proposition: Lemma min_axioms' (rho : nat -> V) : rho ⊫ minZF'.
proof: Proof. Proof using VIEQ M_ZF. intros A [<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]; cbn. - apply (@M_ZF rho ax_ext). cbn. tauto. - exists ∅. apply (@M_ZF rho ax_eset). cbn. tauto. - intros x y. exists ({x; y}). apply (@M_ZF rho ax_pair). cbn. tauto. - intros x. exists (⋃ x). apply (@M_ZF rho ax_union). cbn. tauto. - intros x. exists (PP x). apply (@M_ZF rho ax_power). cbn. tauto. - exists ω. split. split. + exists ∅. split. apply (@M_ZF rho ax_eset). cbn. tauto. apply (@M_ZF rho ax_om1). cbn. tauto. + intros x Hx. exists (σ x). split. 2: apply (@M_ZF rho ax_om1); cbn; tauto. intros y. rewrite !VIEQ. now apply sigma_el. + intros x [H1 H2]. apply (@M_ZF rho ax_om2); cbn. tauto. split. * destruct H1 as (e & E1 & E2). enough (∅ = e) as -> by assumption. apply M_ext; trivial. all: intros y Hy; exfalso; try now apply E1 in Hy. apply (@M_ZF rho ax_eset) in Hy; trivial. unfold ZF'. cbn. tauto. * intros d (s & S1 & S2) % H2. enough (σ d = s) as -> by assumption. apply M_ext; trivial. all: intros y; rewrite sigma_el; trivial. all: rewrite <- !VIEQ; apply S1. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets(minZF ZF) Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability(Shared.ListAutomation)