Detailed syntax breakdown of Definition df-gex
Step | Hyp | Ref
| Expression |
1 | | cgex 19133 |
. 2
class
gEx |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3432 |
. . 3
class
V |
4 | | vi |
. . . 4
setvar 𝑖 |
5 | | vn |
. . . . . . . . 9
setvar 𝑛 |
6 | 5 | cv 1538 |
. . . . . . . 8
class 𝑛 |
7 | | vx |
. . . . . . . . 9
setvar 𝑥 |
8 | 7 | cv 1538 |
. . . . . . . 8
class 𝑥 |
9 | 2 | cv 1538 |
. . . . . . . . 9
class 𝑔 |
10 | | cmg 18700 |
. . . . . . . . 9
class
.g |
11 | 9, 10 | cfv 6433 |
. . . . . . . 8
class
(.g‘𝑔) |
12 | 6, 8, 11 | co 7275 |
. . . . . . 7
class (𝑛(.g‘𝑔)𝑥) |
13 | | c0g 17150 |
. . . . . . . 8
class
0g |
14 | 9, 13 | cfv 6433 |
. . . . . . 7
class
(0g‘𝑔) |
15 | 12, 14 | wceq 1539 |
. . . . . 6
wff (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔) |
16 | | cbs 16912 |
. . . . . . 7
class
Base |
17 | 9, 16 | cfv 6433 |
. . . . . 6
class
(Base‘𝑔) |
18 | 15, 7, 17 | wral 3064 |
. . . . 5
wff
∀𝑥 ∈
(Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔) |
19 | | cn 11973 |
. . . . 5
class
ℕ |
20 | 18, 5, 19 | crab 3068 |
. . . 4
class {𝑛 ∈ ℕ ∣
∀𝑥 ∈
(Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} |
21 | 4 | cv 1538 |
. . . . . 6
class 𝑖 |
22 | | c0 4256 |
. . . . . 6
class
∅ |
23 | 21, 22 | wceq 1539 |
. . . . 5
wff 𝑖 = ∅ |
24 | | cc0 10871 |
. . . . 5
class
0 |
25 | | cr 10870 |
. . . . . 6
class
ℝ |
26 | | clt 11009 |
. . . . . 6
class
< |
27 | 21, 25, 26 | cinf 9200 |
. . . . 5
class inf(𝑖, ℝ, <
) |
28 | 23, 24, 27 | cif 4459 |
. . . 4
class if(𝑖 = ∅, 0, inf(𝑖, ℝ, <
)) |
29 | 4, 20, 28 | csb 3832 |
. . 3
class
⦋{𝑛
∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) |
30 | 2, 3, 29 | cmpt 5157 |
. 2
class (𝑔 ∈ V ↦
⦋{𝑛 ∈
ℕ ∣ ∀𝑥
∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |
31 | 1, 30 | wceq 1539 |
1
wff gEx =
(𝑔 ∈ V ↦
⦋{𝑛 ∈
ℕ ∣ ∀𝑥
∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |