Axiom ax-inf2 5540

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 5541 shows it converted to abbreviations. This axiom was derived as theorem axinf2 5539 above, using our version of Infinity ax-inf 5537 and the Axiom of Regularity ax-reg 5505. We will reference ax-inf2 5540 instead of axinf2 5539 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 5537 from ax-inf2 5540 is shown by theorem axinf 5543.

Assertion

Ref	Expression
ax-inf2	|- E.x(E.y(y e. x /\ A.z -. z e. y) /\ A.y(y e. x -> E.z(z e. x /\ A.w(w e. z <-> (w e. 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 1135	. . . . . 6 class y
3		vx	. . . . . . 7 set x
4	3	cv 1135	. . . . . 6 class x
5	2, 4	wcel 1138	. . . . 5 wff y e. x
6		vz	. . . . . . . . 9 set z
7	6	cv 1135	. . . . . . . 8 class z
8	7, 2	wcel 1138	. . . . . . 7 wff z e. y
9	8	wn 2	. . . . . 6 wff -. z e. y
10	9, 6	wal 1134	. . . . 5 wff A.z -. z e. y
11	5, 10	wa 239	. . . 4 wff (y e. x /\ A.z -. z e. y)
12	11, 1	wex 1164	. . 3 wff E.y(y e. x /\ A.z -. z e. y)
13	7, 4	wcel 1138	. . . . . . 7 wff z e. x
14		vw	. . . . . . . . . . 11 set w
15	14	cv 1135	. . . . . . . . . 10 class w
16	15, 7	wcel 1138	. . . . . . . . 9 wff w e. z
17	15, 2	wcel 1138	. . . . . . . . . 10 wff w e. y
18	15, 2	wceq 1136	. . . . . . . . . 10 wff w = y
19	17, 18	wo 238	. . . . . . . . 9 wff (w e. y \/ w = y)
20	16, 19	wb 162	. . . . . . . 8 wff (w e. z <-> (w e. y \/ w = y))
21	20, 14	wal 1134	. . . . . . 7 wff A.w(w e. z <-> (w e. y \/ w = y))
22	13, 21	wa 239	. . . . . 6 wff (z e. x /\ A.w(w e. z <-> (w e. y \/ w = y)))
23	22, 6	wex 1164	. . . . 5 wff E.z(z e. x /\ A.w(w e. z <-> (w e. y \/ w = y)))
24	5, 23	wi 3	. . . 4 wff (y e. x -> E.z(z e. x /\ A.w(w e. z <-> (w e. y \/ w = y))))
25	24, 1	wal 1134	. . 3 wff A.y(y e. x -> E.z(z e. x /\ A.w(w e. z <-> (w e. y \/ w = y))))
26	12, 25	wa 239	. 2 wff (E.y(y e. x /\ A.z -. z e. y) /\ A.y(y e. x -> E.z(z e. x /\ A.w(w e. z <-> (w e. y \/ w = y)))))
27	26, 3	wex 1164	1 wff E.x(E.y(y e. x /\ A.z -. z e. y) /\ A.y(y e. x -> E.z(z e. x /\ A.w(w e. z <-> (w e. y \/ w = y)))))

This axiom is referenced by:  zfinf2 5541

Copyright terms: Public domain