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 ∃ y y ∈ x ∧ ∀ z ¬ z ∈ y ∧ ∀ y y ∈ x → ∃ z z ∈ x ∧ ∀ w w ∈ z ↔ w ∈ y ∨ w = y

Proof

Step Hyp Ref Expression
1 peano1 ⊢ ∅ ∈ ω
2 peano2 ⊢ y ∈ ω → suc ⁡ y ∈ ω
3 2 ax-gen ⊢ ∀ y y ∈ ω → suc ⁡ y ∈ ω
4 zfinf ⊢ ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
5 4 inf2 ⊢ ∃ x x ≠ ∅ ∧ 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 = ω → ∀ y y ∈ x → suc ⁡ y ∈ x ↔ ∀ y y ∈ ω → suc ⁡ y ∈ ω
12 7 11 anbi12d ⊢ x = ω → ∅ ∈ x ∧ ∀ y y ∈ x → suc ⁡ y ∈ x ↔ ∅ ∈ ω ∧ ∀ y y ∈ ω → suc ⁡ y ∈ ω
13 6 12 spcev ⊢ ∅ ∈ ω ∧ ∀ y y ∈ ω → suc ⁡ y ∈ ω → ∃ x ∅ ∈ x ∧ ∀ y y ∈ x → suc ⁡ y ∈ x
14 1 3 13 mp2an ⊢ ∃ x ∅ ∈ x ∧ ∀ y y ∈ x → suc ⁡ y ∈ x
15 0el ⊢ ∅ ∈ x ↔ ∃ y ∈ x ∀ z ¬ z ∈ y
16 df-rex ⊢ ∃ y ∈ x ∀ z ¬ z ∈ y ↔ ∃ y y ∈ x ∧ ∀ z ¬ z ∈ y
17 15 16 bitri ⊢ ∅ ∈ x ↔ ∃ y y ∈ x ∧ ∀ z ¬ z ∈ y
18 sucel ⊢ suc ⁡ y ∈ x ↔ ∃ z ∈ x ∀ w w ∈ z ↔ w ∈ y ∨ w = y
19 df-rex ⊢ ∃ z ∈ x ∀ w w ∈ z ↔ w ∈ y ∨ w = y ↔ ∃ z z ∈ x ∧ ∀ w w ∈ z ↔ w ∈ y ∨ w = y
20 18 19 bitri ⊢ suc ⁡ y ∈ x ↔ ∃ z z ∈ x ∧ ∀ w w ∈ z ↔ w ∈ y ∨ w = y
21 20 imbi2i ⊢ y ∈ x → suc ⁡ y ∈ x ↔ y ∈ x → ∃ z z ∈ x ∧ ∀ w w ∈ z ↔ w ∈ y ∨ w = y
22 21 albii ⊢ ∀ y y ∈ x → suc ⁡ y ∈ x ↔ ∀ y y ∈ x → ∃ z z ∈ x ∧ ∀ w w ∈ z ↔ w ∈ y ∨ w = y
23 17 22 anbi12i ⊢ ∅ ∈ x ∧ ∀ y y ∈ x → suc ⁡ y ∈ x ↔ ∃ y y ∈ x ∧ ∀ z ¬ z ∈ y ∧ ∀ y y ∈ x → ∃ z z ∈ x ∧ ∀ w w ∈ z ↔ w ∈ y ∨ w = y
24 23 exbii ⊢ ∃ x ∅ ∈ x ∧ ∀ y y ∈ x → suc ⁡ y ∈ x ↔ ∃ x ∃ y y ∈ x ∧ ∀ z ¬ z ∈ y ∧ ∀ y y ∈ x → ∃ z z ∈ x ∧ ∀ w w ∈ z ↔ w ∈ y ∨ w = y
25 14 24 mpbi ⊢ ∃ x ∃ y y ∈ x ∧ ∀ z ¬ z ∈ y ∧ ∀ y y ∈ x → ∃ z z ∈ x ∧ ∀ w w ∈ z ↔ w ∈ y ∨ w = y