Detailed syntax breakdown of Definition df-od
Step | Hyp | Ref
| Expression |
1 | | cod 18916 |
. 2
class
od |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | 2 | cv 1542 |
. . . . 5
class 𝑔 |
6 | | cbs 16760 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 6380 |
. . . 4
class
(Base‘𝑔) |
8 | | vi |
. . . . 5
setvar 𝑖 |
9 | | vn |
. . . . . . . . 9
setvar 𝑛 |
10 | 9 | cv 1542 |
. . . . . . . 8
class 𝑛 |
11 | 4 | cv 1542 |
. . . . . . . 8
class 𝑥 |
12 | | cmg 18488 |
. . . . . . . . 9
class
.g |
13 | 5, 12 | cfv 6380 |
. . . . . . . 8
class
(.g‘𝑔) |
14 | 10, 11, 13 | co 7213 |
. . . . . . 7
class (𝑛(.g‘𝑔)𝑥) |
15 | | c0g 16944 |
. . . . . . . 8
class
0g |
16 | 5, 15 | cfv 6380 |
. . . . . . 7
class
(0g‘𝑔) |
17 | 14, 16 | wceq 1543 |
. . . . . 6
wff (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔) |
18 | | cn 11830 |
. . . . . 6
class
ℕ |
19 | 17, 9, 18 | crab 3065 |
. . . . 5
class {𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} |
20 | 8 | cv 1542 |
. . . . . . 7
class 𝑖 |
21 | | c0 4237 |
. . . . . . 7
class
∅ |
22 | 20, 21 | wceq 1543 |
. . . . . 6
wff 𝑖 = ∅ |
23 | | cc0 10729 |
. . . . . 6
class
0 |
24 | | cr 10728 |
. . . . . . 7
class
ℝ |
25 | | clt 10867 |
. . . . . . 7
class
< |
26 | 20, 24, 25 | cinf 9057 |
. . . . . 6
class inf(𝑖, ℝ, <
) |
27 | 22, 23, 26 | cif 4439 |
. . . . 5
class if(𝑖 = ∅, 0, inf(𝑖, ℝ, <
)) |
28 | 8, 19, 27 | csb 3811 |
. . . 4
class
⦋{𝑛
∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) |
29 | 4, 7, 28 | cmpt 5135 |
. . 3
class (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |
30 | 2, 3, 29 | cmpt 5135 |
. 2
class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |
31 | 1, 30 | wceq 1543 |
1
wff od = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |