Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > ax-infvn | Unicode version |
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 4570) from which one then proves, using full separation, that the wanted set exists (omex 4575). "vn" is for "von Neumann". (Contributed by BJ, 14-Nov-2019.) |
Ref | Expression |
---|---|
ax-infvn | Ind Ind |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . . . 5 | |
2 | 1 | cv 1347 | . . . 4 |
3 | 2 | wind 13883 | . . 3 Ind |
4 | vy | . . . . . . 7 | |
5 | 4 | cv 1347 | . . . . . 6 |
6 | 5 | wind 13883 | . . . . 5 Ind |
7 | 2, 5 | wss 3121 | . . . . 5 |
8 | 6, 7 | wi 4 | . . . 4 Ind |
9 | 8, 4 | wal 1346 | . . 3 Ind |
10 | 3, 9 | wa 103 | . 2 Ind Ind |
11 | 10, 1 | wex 1485 | 1 Ind Ind |
Colors of variables: wff set class |
This axiom is referenced by: bj-omex 13899 |
Copyright terms: Public domain | W3C validator |