Axiom ax-infvn 13139

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 4502) from which one then proves, using full separation, that the wanted set exists (omex 4507). "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 1330	. . . 4 class x
3	2	wind 13124	. . 3 wff Ind x
4		vy	. . . . . . 7 setvar y
5	4	cv 1330	. . . . . 6 class y
6	5	wind 13124	. . . . 5 wff Ind y
7	2, 5	wss 3071	. . . . 5 wff x C_ y
8	6, 7	wi 4	. . . 4 wff (Ind y -> x C_ y )
9	8, 4	wal 1329	. . 3 wff A. y (Ind y -> x C_ y )
10	3, 9	wa 103	. 2 wff (Ind x /\ A. y (Ind y -> x C_ y ) )
11	10, 1	wex 1468	1 wff E. x (Ind x /\ A. y (Ind y -> x C_ y ) )

This axiom is referenced by:  bj-omex  13140