Axiom ax-inf2 14011

Description: Another axiom of infinity in a constructive setting (see ax-infvn 13976). (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 2142	. . . 4 wff 𝑥 ∈ 𝑎
4	1	cv 1347	. . . . . 6 class 𝑥
5		c0 3414	. . . . . 6 class ∅
6	4, 5	wceq 1348	. . . . 5 wff 𝑥 = ∅
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1347	. . . . . . . 8 class 𝑦
9	8	csuc 4350	. . . . . . 7 class suc 𝑦
10	4, 9	wceq 1348	. . . . . 6 wff 𝑥 = suc 𝑦
11	2	cv 1347	. . . . . 6 class 𝑎
12	10, 7, 11	wrex 2449	. . . . 5 wff ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦
13	6, 12	wo 703	. . . 4 wff (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦)
14	3, 13	wb 104	. . 3 wff (𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))
15	14, 1	wal 1346	. 2 wff ∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))
16	15, 2	wex 1485	1 wff ∃𝑎∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))

This axiom is referenced by:  bj-omex2  14012  bj-nn0sucALT  14013