Detailed syntax breakdown of Definition df-cgrg
| Step | Hyp | Ref
| Expression |
| 1 | | ccgrg 28518 |
. 2
class
cgrG |
| 2 | | vg |
. . 3
setvar 𝑔 |
| 3 | | cvv 3480 |
. . 3
class
V |
| 4 | | va |
. . . . . . . 8
setvar 𝑎 |
| 5 | 4 | cv 1539 |
. . . . . . 7
class 𝑎 |
| 6 | 2 | cv 1539 |
. . . . . . . . 9
class 𝑔 |
| 7 | | cbs 17247 |
. . . . . . . . 9
class
Base |
| 8 | 6, 7 | cfv 6561 |
. . . . . . . 8
class
(Base‘𝑔) |
| 9 | | cr 11154 |
. . . . . . . 8
class
ℝ |
| 10 | | cpm 8867 |
. . . . . . . 8
class
↑pm |
| 11 | 8, 9, 10 | co 7431 |
. . . . . . 7
class
((Base‘𝑔)
↑pm ℝ) |
| 12 | 5, 11 | wcel 2108 |
. . . . . 6
wff 𝑎 ∈ ((Base‘𝑔) ↑pm
ℝ) |
| 13 | | vb |
. . . . . . . 8
setvar 𝑏 |
| 14 | 13 | cv 1539 |
. . . . . . 7
class 𝑏 |
| 15 | 14, 11 | wcel 2108 |
. . . . . 6
wff 𝑏 ∈ ((Base‘𝑔) ↑pm
ℝ) |
| 16 | 12, 15 | wa 395 |
. . . . 5
wff (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ)
∧ 𝑏 ∈
((Base‘𝑔)
↑pm ℝ)) |
| 17 | 5 | cdm 5685 |
. . . . . . 7
class dom 𝑎 |
| 18 | 14 | cdm 5685 |
. . . . . . 7
class dom 𝑏 |
| 19 | 17, 18 | wceq 1540 |
. . . . . 6
wff dom 𝑎 = dom 𝑏 |
| 20 | | vi |
. . . . . . . . . . . 12
setvar 𝑖 |
| 21 | 20 | cv 1539 |
. . . . . . . . . . 11
class 𝑖 |
| 22 | 21, 5 | cfv 6561 |
. . . . . . . . . 10
class (𝑎‘𝑖) |
| 23 | | vj |
. . . . . . . . . . . 12
setvar 𝑗 |
| 24 | 23 | cv 1539 |
. . . . . . . . . . 11
class 𝑗 |
| 25 | 24, 5 | cfv 6561 |
. . . . . . . . . 10
class (𝑎‘𝑗) |
| 26 | | cds 17306 |
. . . . . . . . . . 11
class
dist |
| 27 | 6, 26 | cfv 6561 |
. . . . . . . . . 10
class
(dist‘𝑔) |
| 28 | 22, 25, 27 | co 7431 |
. . . . . . . . 9
class ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) |
| 29 | 21, 14 | cfv 6561 |
. . . . . . . . . 10
class (𝑏‘𝑖) |
| 30 | 24, 14 | cfv 6561 |
. . . . . . . . . 10
class (𝑏‘𝑗) |
| 31 | 29, 30, 27 | co 7431 |
. . . . . . . . 9
class ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) |
| 32 | 28, 31 | wceq 1540 |
. . . . . . . 8
wff ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) |
| 33 | 32, 23, 17 | wral 3061 |
. . . . . . 7
wff
∀𝑗 ∈ dom
𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) |
| 34 | 33, 20, 17 | wral 3061 |
. . . . . 6
wff
∀𝑖 ∈ dom
𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) |
| 35 | 19, 34 | wa 395 |
. . . . 5
wff (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))) |
| 36 | 16, 35 | wa 395 |
. . . 4
wff ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ)
∧ 𝑏 ∈
((Base‘𝑔)
↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)))) |
| 37 | 36, 4, 13 | copab 5205 |
. . 3
class
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ)
∧ 𝑏 ∈
((Base‘𝑔)
↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))} |
| 38 | 2, 3, 37 | cmpt 5225 |
. 2
class (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ))
∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))}) |
| 39 | 1, 38 | wceq 1540 |
1
wff cgrG =
(𝑔 ∈ V ↦
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ)
∧ 𝑏 ∈
((Base‘𝑔)
↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))}) |