proposition: Lemma min_axioms' (rho : nat -> V) : rho ⊫ minZFeq'.
proof: Proof. Proof using M_ZF. intros A [<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]]]]; cbn. - now apply set_equiv_equiv. - now apply set_equiv_equiv. - now apply set_equiv_equiv. - intros x x' y y' Hx Hy. now apply set_equiv_elem. - intros x y H1 H2. now apply M_ext. - exists ∅. apply (@M_ZF rho ax_eset). firstorder. - intros x y. exists ({x; y}). apply (@M_ZF rho ax_pair). firstorder. - intros x. exists (⋃ x). apply (@M_ZF rho ax_union). firstorder. - intros x. exists (PP x). apply (@M_ZF rho ax_power). firstorder. - exists ω. split. split. + exists ∅. split. apply (@M_ZF rho ax_eset). firstorder. apply (@M_ZF rho ax_om1). firstorder. + intros x Hx. exists (σ x). split. 2: apply (@M_ZF rho ax_om1); firstorder. intros y. now apply sigma_el. + intros x [H1 H2]. apply (@M_ZF rho ax_om2); cbn. auto 12. split. * destruct H1 as (e & E1 & E2). change (set_elem ∅ x). enough (set_equiv ∅ 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 ZFeq', ZF'. auto 8. * intros d (s & S1 & S2) % H2. change (set_elem (σ d) x). enough (set_equiv (σ d) s) as -> by assumption. apply M_ext; trivial. all: intros y; rewrite sigma_el; trivial; 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 PCPb_to_ZFeq PCPb_to_minZF) Undecidability(Shared.ListAutomation) Morphisms