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 ∈ x suc ⁡ y ∈ x

Proof

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