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	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Axiom ax-infvn

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar x
2	1	cv 1363	. . . 4 class x
3	2	wind 15572	. . 3 wff Ind x
4		vy	. . . . . . 7 setvar y
5	4	cv 1363	. . . . . 6 class y
6	5	wind 15572	. . . . 5 wff Ind y
7	2, 5	wss 3157	. . . . 5 wff x C_ y
8	6, 7	wi 4	. . . 4 wff (Ind y -> x C_ y )
9	8, 4	wal 1362	. . 3 wff A. y (Ind y -> x C_ y )
10	3, 9	wa 104	. 2 wff (Ind x /\ A. y (Ind y -> x C_ y ) )
11	10, 1	wex 1506	1 wff E. x (Ind x /\ A. y (Ind y -> x C_ y ) )

This axiom is referenced by:  bj-omex  15588