Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > ax-infvn | GIF 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 4560) from which one then proves, using full separation, that the wanted set exists (omex 4565). "vn" is for "von Neumann". (Contributed by BJ, 14-Nov-2019.) |
Ref | Expression |
---|---|
ax-infvn | ⊢ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . . . 5 setvar 𝑥 | |
2 | 1 | cv 1341 | . . . 4 class 𝑥 |
3 | 2 | wind 13670 | . . 3 wff Ind 𝑥 |
4 | vy | . . . . . . 7 setvar 𝑦 | |
5 | 4 | cv 1341 | . . . . . 6 class 𝑦 |
6 | 5 | wind 13670 | . . . . 5 wff Ind 𝑦 |
7 | 2, 5 | wss 3112 | . . . . 5 wff 𝑥 ⊆ 𝑦 |
8 | 6, 7 | wi 4 | . . . 4 wff (Ind 𝑦 → 𝑥 ⊆ 𝑦) |
9 | 8, 4 | wal 1340 | . . 3 wff ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦) |
10 | 3, 9 | wa 103 | . 2 wff (Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦)) |
11 | 10, 1 | wex 1479 | 1 wff ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦)) |
Colors of variables: wff set class |
This axiom is referenced by: bj-omex 13686 |
Copyright terms: Public domain | W3C validator |