Axiom ax-inf 1079

Description: Axiom of Infinity. An axiom of Zermelo-Fraenkel set theory. This axiom is the gateway to "Cantor's paradise" (an expression coined by Hilbert). The axiom asserts that an infinite set exists, or more specifically, "there exists a non-empty set that is a subset of its union." Our version is not common the literature, but a proof that it implies the more standard version is given by inf3 3471. Its advantage is that when expanded to primitives, it uses fewer symbols than the standard version. Our version is a slight variant of the Axiom of Infinity in [FreydScedrov] p. 283, proved here as inf1 3458. Variants of the standard version are zfinf 3474 (which is Axiom Inf of [BellMachover] p. 472) and omex 3475 (Axiom 7 of [TakeutiZaring] p. 43). The standard version essentially states that there exists a set containing all the natural numbers. Theorem inf0 3457 shows the reverse derivation of our axiom from a standard one. Theorem inf5 3472 shows a very short way to state this axiom.

Assertion

Ref	Expression
ax-inf	|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))

Distinct variable group(s):   x,y,z,w

Detailed syntax breakdown of Axiom ax-inf

Step	Hyp	Ref	Expression
1		vx	. . . 4 set x
2		vy	. . . 4 set y
3	1, 2	wel 803	. . 3 wff x e. y
4		vz	. . . . . 6 set z
5	4, 2	wel 803	. . . . 5 wff z e. y
6		vw	. . . . . . . 8 set w
7	4, 6	wel 803	. . . . . . 7 wff z e. w
8	6, 2	wel 803	. . . . . . 7 wff w e. y
9	7, 8	wa 196	. . . . . 6 wff (z e. w /\ w e. y)
10	9, 6	wex 678	. . . . 5 wff E.w(z e. w /\ w e. y)
11	5, 10	wi 2	. . . 4 wff (z e. y -> E.w(z e. w /\ w e. y))
12	11, 4	wal 672	. . 3 wff A.z(z e. y -> E.w(z e. w /\ w e. y))
13	3, 12	wa 196	. 2 wff (x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
14	13, 2	wex 678	1 wff E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))

This axiom is referenced by:  axinf 1084

metamath.org