Axiom ax-iinf 4572

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	⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Axiom ax-iinf

Step	Hyp	Ref	Expression
1		c0 3414	. . . 4 class ∅
2		vx	. . . . 5 setvar 𝑥
3	2	cv 1347	. . . 4 class 𝑥
4	1, 3	wcel 2141	. . 3 wff ∅ ∈ 𝑥
5		vy	. . . . . 6 setvar 𝑦
6	5, 2	wel 2142	. . . . 5 wff 𝑦 ∈ 𝑥
7	5	cv 1347	. . . . . . 7 class 𝑦
8	7	csuc 4350	. . . . . 6 class suc 𝑦
9	8, 3	wcel 2141	. . . . 5 wff suc 𝑦 ∈ 𝑥
10	6, 9	wi 4	. . . 4 wff (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)
11	10, 5	wal 1346	. . 3 wff ∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)
12	4, 11	wa 103	. 2 wff (∅ ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
13	12, 2	wex 1485	1 wff ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))

This axiom is referenced by:  zfinf2  4573