Axiom ax-inf2 9329

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 9330 shows it converted to abbreviations. This axiom was derived as Theorem axinf2 9328 above, using our version of Infinity ax-inf 9326 and the Axiom of Regularity ax-reg 9281. We will reference ax-inf2 9329 instead of axinf2 9328 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 9326 from ax-inf2 9329 is shown by Theorem axinf 9332. (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 2109	. . . . 5 wff 𝑦 ∈ 𝑥
4		vz	. . . . . . . 8 setvar 𝑧
5	4, 1	wel 2109	. . . . . . 7 wff 𝑧 ∈ 𝑦
6	5	wn 3	. . . . . 6 wff ¬ 𝑧 ∈ 𝑦
7	6, 4	wal 1537	. . . . 5 wff ∀𝑧 ¬ 𝑧 ∈ 𝑦
8	3, 7	wa 395	. . . 4 wff (𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦)
9	8, 1	wex 1783	. . 3 wff ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦)
10	4, 2	wel 2109	. . . . . . 7 wff 𝑧 ∈ 𝑥
11		vw	. . . . . . . . . 10 setvar 𝑤
12	11, 4	wel 2109	. . . . . . . . 9 wff 𝑤 ∈ 𝑧
13	11, 1	wel 2109	. . . . . . . . . 10 wff 𝑤 ∈ 𝑦
14	11, 1	weq 1967	. . . . . . . . . 10 wff 𝑤 = 𝑦
15	13, 14	wo 843	. . . . . . . . 9 wff (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)
16	12, 15	wb 205	. . . . . . . 8 wff (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))
17	16, 11	wal 1537	. . . . . . 7 wff ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))
18	10, 17	wa 395	. . . . . 6 wff (𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))
19	18, 4	wex 1783	. . . . 5 wff ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))
20	3, 19	wi 4	. . . 4 wff (𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))
21	20, 1	wal 1537	. . 3 wff ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))
22	9, 21	wa 395	. 2 wff (∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))
23	22, 2	wex 1783	1 wff ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))

This axiom is referenced by:  zfinf2  9330