This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 )

Proof

Step Hyp Ref Expression
1 ax-inf2 ⊢ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
2 0el ⊢ ( ∅ ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 )
3 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) )
4 2 3 bitri ⊢ ( ∅ ∈ 𝑥 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) )
5 sucel ⊢ ( suc 𝑦 ∈ 𝑥 ↔ ∃ 𝑧 ∈ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) )
6 df-rex ⊢ ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
7 5 6 bitri ⊢ ( suc 𝑦 ∈ 𝑥 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
8 7 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
9 df-ral ⊢ ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
10 8 9 bitri ⊢ ( ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
11 4 10 anbi12i ⊢ ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ) ↔ ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) )
12 11 exbii ⊢ ( ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) )
13 1 12 mpbir ⊢ ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 )