Axiom ax-inf2 4605

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 zfinf 4606 shows it converted to abbreviations. This axiom was derived as theorem axinf2 4604 above, using our version of Infinity ax-inf 4602 and the Axiom of Regularity ax-reg 4573. We will reference ax-inf2 4605 instead of axinf2 4604 so that the ordinary uses of Regularity can be more easily identified.

Assertion

Ref	Expression
ax-inf2	⊢ ∃x(∃y(y ∈ x ⋀ ∀z ¬ z ∈ y) ⋀ ∀y(y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))))

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-inf2

Step	Hyp	Ref	Expression
1		vy	. . . . . . 7 set y
2	1	cv 953	. . . . . 6 class y
3		vx	. . . . . . 7 set x
4	3	cv 953	. . . . . 6 class x
5	2, 4	wcel 956	. . . . 5 wff y ∈ x
6		vz	. . . . . . . . 9 set z
7	6	cv 953	. . . . . . . 8 class z
8	7, 2	wcel 956	. . . . . . 7 wff z ∈ y
9	8	wn 2	. . . . . 6 wff ¬ z ∈ y
10	9, 6	wal 952	. . . . 5 wff ∀z ¬ z ∈ y
11	5, 10	wa 223	. . . 4 wff (y ∈ x ⋀ ∀z ¬ z ∈ y)
12	11, 1	wex 978	. . 3 wff ∃y(y ∈ x ⋀ ∀z ¬ z ∈ y)
13	7, 4	wcel 956	. . . . . . 7 wff z ∈ x
14		vw	. . . . . . . . . . 11 set w
15	14	cv 953	. . . . . . . . . 10 class w
16	15, 7	wcel 956	. . . . . . . . 9 wff w ∈ z
17	15, 2	wcel 956	. . . . . . . . . 10 wff w ∈ y
18	15, 2	wceq 954	. . . . . . . . . 10 wff w = y
19	17, 18	wo 222	. . . . . . . . 9 wff (w ∈ y ⋁ w = y)
20	16, 19	wb 146	. . . . . . . 8 wff (w ∈ z ↔ (w ∈ y ⋁ w = y))
21	20, 14	wal 952	. . . . . . 7 wff ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y))
22	13, 21	wa 223	. . . . . 6 wff (z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))
23	22, 6	wex 978	. . . . 5 wff ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))
24	5, 23	wi 3	. . . 4 wff (y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y))))
25	24, 1	wal 952	. . 3 wff ∀y(y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y))))
26	12, 25	wa 223	. 2 wff (∃y(y ∈ x ⋀ ∀z ¬ z ∈ y) ⋀ ∀y(y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))))
27	26, 3	wex 978	1 wff ∃x(∃y(y ∈ x ⋀ ∀z ¬ z ∈ y) ⋀ ∀y(y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))))

This axiom is referenced by:  zfinf 4606

Copyright terms: Public domain