Axiom ax-inf2 13163

Description: Another axiom of infinity in a constructive setting (see ax-infvn 13128). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-inf2	⊢ ∃𝑎∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Axiom ax-inf2

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar 𝑥
2		va	. . . . 5 setvar 𝑎
3	1, 2	wel 1481	. . . 4 wff 𝑥 ∈ 𝑎
4	1	cv 1330	. . . . . 6 class 𝑥
5		c0 3358	. . . . . 6 class ∅
6	4, 5	wceq 1331	. . . . 5 wff 𝑥 = ∅
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1330	. . . . . . . 8 class 𝑦
9	8	csuc 4282	. . . . . . 7 class suc 𝑦
10	4, 9	wceq 1331	. . . . . 6 wff 𝑥 = suc 𝑦
11	2	cv 1330	. . . . . 6 class 𝑎
12	10, 7, 11	wrex 2415	. . . . 5 wff ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦
13	6, 12	wo 697	. . . 4 wff (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦)
14	3, 13	wb 104	. . 3 wff (𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))
15	14, 1	wal 1329	. 2 wff ∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))
16	15, 2	wex 1468	1 wff ∃𝑎∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))

This axiom is referenced by:  bj-omex2  13164  bj-nn0sucALT  13165