Axiom ax-infvn 13976

Description: Axiom of infinity in a constructive setting. This asserts the existence of the special set we want (the set of natural numbers), instead of the existence of a set with some properties (ax-iinf 4572) from which one then proves, using full separation, that the wanted set exists (omex 4577). "vn" is for "von Neumann". (Contributed by BJ, 14-Nov-2019.)

Assertion

Ref	Expression
ax-infvn	⊢ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Axiom ax-infvn

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar 𝑥
2	1	cv 1347	. . . 4 class 𝑥
3	2	wind 13961	. . 3 wff Ind 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1347	. . . . . 6 class 𝑦
6	5	wind 13961	. . . . 5 wff Ind 𝑦
7	2, 5	wss 3121	. . . . 5 wff 𝑥 ⊆ 𝑦
8	6, 7	wi 4	. . . 4 wff (Ind 𝑦 → 𝑥 ⊆ 𝑦)
9	8, 4	wal 1346	. . 3 wff ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦)
10	3, 9	wa 103	. 2 wff (Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦))
11	10, 1	wex 1485	1 wff ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦))

This axiom is referenced by:  bj-omex  13977