Axiom ax-infvn 15587

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 4624) from which one then proves, using full separation, that the wanted set exists (omex 4629). "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 1363	. . . 4 class 𝑥
3	2	wind 15572	. . 3 wff Ind 𝑥
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1363	. . . . . 6 class 𝑦
6	5	wind 15572	. . . . 5 wff Ind 𝑦
7	2, 5	wss 3157	. . . . 5 wff 𝑥 ⊆ 𝑦
8	6, 7	wi 4	. . . 4 wff (Ind 𝑦 → 𝑥 ⊆ 𝑦)
9	8, 4	wal 1362	. . 3 wff ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦)
10	3, 9	wa 104	. 2 wff (Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦))
11	10, 1	wex 1506	1 wff ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦))

This axiom is referenced by:  bj-omex  15588