Axiom ax-iinf 4624

Description: Axiom of Infinity. Axiom 5 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by Jim Kingdon, 16-Nov-2018.)

Assertion

Ref	Expression
ax-iinf	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Axiom ax-iinf

Step	Hyp	Ref	Expression
1		c0 3450	. . . 4 class (/)
2		vx	. . . . 5 setvar x
3	2	cv 1363	. . . 4 class x
4	1, 3	wcel 2167	. . 3 wff (/) e. x
5		vy	. . . . . 6 setvar y
6	5, 2	wel 2168	. . . . 5 wff y e. x
7	5	cv 1363	. . . . . . 7 class y
8	7	csuc 4400	. . . . . 6 class suc y
9	8, 3	wcel 2167	. . . . 5 wff suc y e. x
10	6, 9	wi 4	. . . 4 wff ( y e. x -> suc y e. x )
11	10, 5	wal 1362	. . 3 wff A. y ( y e. x -> suc y e. x )
12	4, 11	wa 104	. 2 wff ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
13	12, 2	wex 1506	1 wff E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )

This axiom is referenced by:  zfinf2  4625