Metamath Proof Explorer

Theorem axinf2

Description: A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf and Regularity ax-reg .

This theorem should not be referenced in any proof. Instead, use ax-inf2 below so that the ordinary uses of Regularity can be more easily identified. (New usage is discouraged.) (Contributed by NM, 3-Nov-1996)

Ref Expression
Assertion axinf2 ⊢∃x∃yy∈x∧∀z¬z∈y∧∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y

Proof

Step Hyp Ref Expression
1 peano1 ⊢∅∈ω
2 peano2 ⊢y∈ω→suc⁡y∈ω
3 2 ax-gen ⊢∀yy∈ω→suc⁡y∈ω
4 zfinf ⊢∃xy∈x∧∀yy∈x→∃zy∈z∧z∈x
5 4 inf2 ⊢∃xx≠∅∧x⊆⋃x
6 5 inf3 ⊢ω∈V
7 eleq2 ⊢x=ω→∅∈x↔∅∈ω
8 eleq2 ⊢x=ω→y∈x↔y∈ω
9 eleq2 ⊢x=ω→suc⁡y∈x↔suc⁡y∈ω
10 8 9 imbi12d ⊢x=ω→y∈x→suc⁡y∈x↔y∈ω→suc⁡y∈ω
11 10 albidv ⊢x=ω→∀yy∈x→suc⁡y∈x↔∀yy∈ω→suc⁡y∈ω
12 7 11 anbi12d ⊢x=ω→∅∈x∧∀yy∈x→suc⁡y∈x↔∅∈ω∧∀yy∈ω→suc⁡y∈ω
13 6 12 spcev ⊢∅∈ω∧∀yy∈ω→suc⁡y∈ω→∃x∅∈x∧∀yy∈x→suc⁡y∈x
14 1 3 13 mp2an ⊢∃x∅∈x∧∀yy∈x→suc⁡y∈x
15 0el ⊢∅∈x↔∃y∈x∀z¬z∈y
16 df-rex ⊢∃y∈x∀z¬z∈y↔∃yy∈x∧∀z¬z∈y
17 15 16 bitri ⊢∅∈x↔∃yy∈x∧∀z¬z∈y
18 sucel ⊢suc⁡y∈x↔∃z∈x∀ww∈z↔w∈y∨w=y
19 df-rex ⊢∃z∈x∀ww∈z↔w∈y∨w=y↔∃zz∈x∧∀ww∈z↔w∈y∨w=y
20 18 19 bitri ⊢suc⁡y∈x↔∃zz∈x∧∀ww∈z↔w∈y∨w=y
21 20 imbi2i ⊢y∈x→suc⁡y∈x↔y∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y
22 21 albii ⊢∀yy∈x→suc⁡y∈x↔∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y
23 17 22 anbi12i ⊢∅∈x∧∀yy∈x→suc⁡y∈x↔∃yy∈x∧∀z¬z∈y∧∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y
24 23 exbii ⊢∃x∅∈x∧∀yy∈x→suc⁡y∈x↔∃x∃yy∈x∧∀z¬z∈y∧∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y
25 14 24 mpbi ⊢∃x∃yy∈x∧∀z¬z∈y∧∀yy∈x→∃zz∈x∧∀ww∈z↔w∈y∨w=y