Axiom ax-inf2 9643

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 9644 shows it converted to abbreviations. This axiom was derived as Theorem axinf2 9642 above, using our version of Infinity ax-inf 9640 and the Axiom of Regularity ax-reg 9587. We will reference ax-inf2 9643 instead of axinf2 9642 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 9640 from ax-inf2 9643 is shown by Theorem axinf 9646. (Contributed by NM, 3-Nov-1996.)

Assertion

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

Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Detailed syntax breakdown of Axiom ax-inf2

Step	Hyp	Ref	Expression
1		vy	. . . . . 6 setvar 𝑦
2		vx	. . . . . 6 setvar 𝑥
3	1, 2	wel 2146	. . . . 5 wff 𝑦 ∈ 𝑥
4		vz	. . . . . . . 8 setvar 𝑧
5	4, 1	wel 2146	. . . . . . 7 wff 𝑧 ∈ 𝑦
6	5	wn 3	. . . . . 6 wff ¬ 𝑧 ∈ 𝑦
7	6, 4	wal 1568	. . . . 5 wff ∀𝑧 ¬ 𝑧 ∈ 𝑦
8	3, 7	wa 401	. . . 4 wff (𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦)
9	8, 1	wex 1812	. . 3 wff ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦)
10	4, 2	wel 2146	. . . . . . 7 wff 𝑧 ∈ 𝑥
11		vw	. . . . . . . . . 10 setvar 𝑤
12	11, 4	wel 2146	. . . . . . . . 9 wff 𝑤 ∈ 𝑧
13	11, 1	wel 2146	. . . . . . . . . 10 wff 𝑤 ∈ 𝑦
14	11, 1	weq 1995	. . . . . . . . . 10 wff 𝑤 = 𝑦
15	13, 14	wo 861	. . . . . . . . 9 wff (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)
16	12, 15	wb 209	. . . . . . . 8 wff (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))
17	16, 11	wal 1568	. . . . . . 7 wff ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))
18	10, 17	wa 401	. . . . . 6 wff (𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))
19	18, 4	wex 1812	. . . . 5 wff ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))
20	3, 19	wi 4	. . . 4 wff (𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))
21	20, 1	wal 1568	. . 3 wff ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))
22	9, 21	wa 401	. 2 wff (∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))
23	22, 2	wex 1812	1 wff ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))

This axiom is used by:  zfinf2  9644  axnulALT3  35734  axprALT2  35735