Detailed syntax breakdown of Definition df-gex
Step | Hyp | Ref
| Expression |
1 | | cgex 19114 |
. 2
class
gEx |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3430 |
. . 3
class
V |
4 | | vi |
. . . 4
setvar 𝑖 |
5 | | vn |
. . . . . . . . 9
setvar 𝑛 |
6 | 5 | cv 1540 |
. . . . . . . 8
class 𝑛 |
7 | | vx |
. . . . . . . . 9
setvar 𝑥 |
8 | 7 | cv 1540 |
. . . . . . . 8
class 𝑥 |
9 | 2 | cv 1540 |
. . . . . . . . 9
class 𝑔 |
10 | | cmg 18681 |
. . . . . . . . 9
class
.g |
11 | 9, 10 | cfv 6430 |
. . . . . . . 8
class
(.g‘𝑔) |
12 | 6, 8, 11 | co 7268 |
. . . . . . 7
class (𝑛(.g‘𝑔)𝑥) |
13 | | c0g 17131 |
. . . . . . . 8
class
0g |
14 | 9, 13 | cfv 6430 |
. . . . . . 7
class
(0g‘𝑔) |
15 | 12, 14 | wceq 1541 |
. . . . . 6
wff (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔) |
16 | | cbs 16893 |
. . . . . . 7
class
Base |
17 | 9, 16 | cfv 6430 |
. . . . . 6
class
(Base‘𝑔) |
18 | 15, 7, 17 | wral 3065 |
. . . . 5
wff
∀𝑥 ∈
(Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔) |
19 | | cn 11956 |
. . . . 5
class
ℕ |
20 | 18, 5, 19 | crab 3069 |
. . . 4
class {𝑛 ∈ ℕ ∣
∀𝑥 ∈
(Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} |
21 | 4 | cv 1540 |
. . . . . 6
class 𝑖 |
22 | | c0 4261 |
. . . . . 6
class
∅ |
23 | 21, 22 | wceq 1541 |
. . . . 5
wff 𝑖 = ∅ |
24 | | cc0 10855 |
. . . . 5
class
0 |
25 | | cr 10854 |
. . . . . 6
class
ℝ |
26 | | clt 10993 |
. . . . . 6
class
< |
27 | 21, 25, 26 | cinf 9161 |
. . . . 5
class inf(𝑖, ℝ, <
) |
28 | 23, 24, 27 | cif 4464 |
. . . 4
class if(𝑖 = ∅, 0, inf(𝑖, ℝ, <
)) |
29 | 4, 20, 28 | csb 3836 |
. . 3
class
⦋{𝑛
∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) |
30 | 2, 3, 29 | cmpt 5161 |
. 2
class (𝑔 ∈ V ↦
⦋{𝑛 ∈
ℕ ∣ ∀𝑥
∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |
31 | 1, 30 | wceq 1541 |
1
wff gEx =
(𝑔 ∈ V ↦
⦋{𝑛 ∈
ℕ ∣ ∀𝑥
∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |