Metamath Proof Explorer

Theorem zfinf2

Description: A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of BellMachover p. 472. (See ax-inf2 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993)

Ref Expression
Assertion zfinf2 ⊢∃x∅∈x∧∀y∈xsuc⁡y∈x

Proof

Step Hyp Ref Expression
1 ax-inf2 ⊢∃x∃yy∈x∧∀z¬z∈y∧∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y
2 0el ⊢∅∈x↔∃y∈x∀z¬z∈y
3 df-rex ⊢∃y∈x∀z¬z∈y↔∃yy∈x∧∀z¬z∈y
4 2 3 bitri ⊢∅∈x↔∃yy∈x∧∀z¬z∈y
5 sucel ⊢suc⁡y∈x↔∃z∈x∀ww∈z↔w∈y∨w=y
6 df-rex ⊢∃z∈x∀ww∈z↔w∈y∨w=y↔∃zz∈x∧∀ww∈z↔w∈y∨w=y
7 5 6 bitri ⊢suc⁡y∈x↔∃zz∈x∧∀ww∈z↔w∈y∨w=y
8 7 ralbii ⊢∀y∈xsuc⁡y∈x↔∀y∈x∃zz∈x∧∀ww∈z↔w∈y∨w=y
9 df-ral ⊢∀y∈x∃zz∈x∧∀ww∈z↔w∈y∨w=y↔∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y
10 8 9 bitri ⊢∀y∈xsuc⁡y∈x↔∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y
11 4 10 anbi12i ⊢∅∈x∧∀y∈xsuc⁡y∈x↔∃yy∈x∧∀z¬z∈y∧∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y
12 11 exbii ⊢∃x∅∈x∧∀y∈xsuc⁡y∈x↔∃x∃yy∈x∧∀z¬z∈y∧∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y
13 1 12 mpbir ⊢∃x∅∈x∧∀y∈xsuc⁡y∈x