Axiom ax-inf2 5964

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

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 1585	. . . . . 6 class y
3		vx	. . . . . . 7 set x
4	3	cv 1585	. . . . . 6 class x
5	2, 4	wcel 1588	. . . . 5 wff y e. x
6		vz	. . . . . . . . 9 set z
7	6	cv 1585	. . . . . . . 8 class z
8	7, 2	wcel 1588	. . . . . . 7 wff z e. y
9	8	wn 2	. . . . . 6 wff -. z e. y
10	9, 6	wal 1584	. . . . 5 wff A.z -. z e. y
11	5, 10	wa 337	. . . 4 wff (y e. x /\ A.z -. z e. y)
12	11, 1	wex 1615	. . 3 wff E.y(y e. x /\ A.z -. z e. y)
13	7, 4	wcel 1588	. . . . . . 7 wff z e. x
14		vw	. . . . . . . . . . 11 set w
15	14	cv 1585	. . . . . . . . . 10 class w
16	15, 7	wcel 1588	. . . . . . . . 9 wff w e. z
17	15, 2	wcel 1588	. . . . . . . . . 10 wff w e. y
18	15, 2	wceq 1586	. . . . . . . . . 10 wff w = y
19	17, 18	wo 336	. . . . . . . . 9 wff (w e. y \/ w = y)
20	16, 19	wb 219	. . . . . . . 8 wff (w e. z <-> (w e. y \/ w = y))
21	20, 14	wal 1584	. . . . . . 7 wff A.w(w e. z <-> (w e. y \/ w = y))
22	13, 21	wa 337	. . . . . 6 wff (z e. x /\ A.w(w e. z <-> (w e. y \/ w = y)))
23	22, 6	wex 1615	. . . . 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 1584	. . 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 337	. 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 1615	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 5965

Copyright terms: Public domain