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

Metamath Proof Explorer

Axiom ax-inf2

Description: A standard version of Axiom of Infinity of ZF set theory. In English, it says: there exists a set that contains the empty set and the successors of all of its members. Theorem zfinf2 shows it converted to abbreviations. This axiom was derived as Theorem axinf2 above, using our version of Infinity ax-inf and the Axiom of Regularity ax-reg . We will reference ax-inf2 instead of axinf2 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf from ax-inf2 is shown by Theorem axinf . (Contributed by NM, 3-Nov-1996)

Ref Expression
Assertion ax-inf2 ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx ⊢ 𝑥
1 vy ⊢ 𝑦
2 1 cv ⊢ 𝑦
3 0 cv ⊢ 𝑥
4 2 3 wcel ⊢ 𝑦 ∈ 𝑥
5 vz ⊢ 𝑧
6 5 cv ⊢ 𝑧
7 6 2 wcel ⊢ 𝑧 ∈ 𝑦
8 7 wn ⊢ ¬ 𝑧 ∈ 𝑦
9 8 5 wal ⊢ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦
10 4 9 wa ⊢ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 )
11 10 1 wex ⊢ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 )
12 6 3 wcel ⊢ 𝑧 ∈ 𝑥
13 vw ⊢ 𝑤
14 13 cv ⊢ 𝑤
15 14 6 wcel ⊢ 𝑤 ∈ 𝑧
16 14 2 wcel ⊢ 𝑤 ∈ 𝑦
17 14 2 wceq ⊢ 𝑤 = 𝑦
18 16 17 wo ⊢ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 )
19 15 18 wb ⊢ ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) )
20 19 13 wal ⊢ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) )
21 12 20 wa ⊢ ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) )
22 21 5 wex ⊢ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) )
23 4 22 wi ⊢ ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
24 23 1 wal ⊢ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
25 11 24 wa ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
26 25 0 wex ⊢ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )