Detailed syntax breakdown of Definition df-od
| Step | Hyp | Ref
| Expression |
| 1 | | cod 19542 |
. 2
class
od |
| 2 | | vg |
. . 3
setvar 𝑔 |
| 3 | | cvv 3480 |
. . 3
class
V |
| 4 | | vx |
. . . 4
setvar 𝑥 |
| 5 | 2 | cv 1539 |
. . . . 5
class 𝑔 |
| 6 | | cbs 17247 |
. . . . 5
class
Base |
| 7 | 5, 6 | cfv 6561 |
. . . 4
class
(Base‘𝑔) |
| 8 | | vi |
. . . . 5
setvar 𝑖 |
| 9 | | vn |
. . . . . . . . 9
setvar 𝑛 |
| 10 | 9 | cv 1539 |
. . . . . . . 8
class 𝑛 |
| 11 | 4 | cv 1539 |
. . . . . . . 8
class 𝑥 |
| 12 | | cmg 19085 |
. . . . . . . . 9
class
.g |
| 13 | 5, 12 | cfv 6561 |
. . . . . . . 8
class
(.g‘𝑔) |
| 14 | 10, 11, 13 | co 7431 |
. . . . . . 7
class (𝑛(.g‘𝑔)𝑥) |
| 15 | | c0g 17484 |
. . . . . . . 8
class
0g |
| 16 | 5, 15 | cfv 6561 |
. . . . . . 7
class
(0g‘𝑔) |
| 17 | 14, 16 | wceq 1540 |
. . . . . 6
wff (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔) |
| 18 | | cn 12266 |
. . . . . 6
class
ℕ |
| 19 | 17, 9, 18 | crab 3436 |
. . . . 5
class {𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} |
| 20 | 8 | cv 1539 |
. . . . . . 7
class 𝑖 |
| 21 | | c0 4333 |
. . . . . . 7
class
∅ |
| 22 | 20, 21 | wceq 1540 |
. . . . . 6
wff 𝑖 = ∅ |
| 23 | | cc0 11155 |
. . . . . 6
class
0 |
| 24 | | cr 11154 |
. . . . . . 7
class
ℝ |
| 25 | | clt 11295 |
. . . . . . 7
class
< |
| 26 | 20, 24, 25 | cinf 9481 |
. . . . . 6
class inf(𝑖, ℝ, <
) |
| 27 | 22, 23, 26 | cif 4525 |
. . . . 5
class if(𝑖 = ∅, 0, inf(𝑖, ℝ, <
)) |
| 28 | 8, 19, 27 | csb 3899 |
. . . 4
class
⦋{𝑛
∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) |
| 29 | 4, 7, 28 | cmpt 5225 |
. . 3
class (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |
| 30 | 2, 3, 29 | cmpt 5225 |
. 2
class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |
| 31 | 1, 30 | wceq 1540 |
1
wff od = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |