Detailed syntax breakdown of Definition df-mir
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cmir 26917 |
. 2
class
pInvG |
| 2 | | vg |
. . 3
setvar 𝑔 |
| 3 | | cvv 3422 |
. . 3
class
V |
| 4 | | vm |
. . . 4
setvar 𝑚 |
| 5 | 2 | cv 1538 |
. . . . 5
class 𝑔 |
| 6 | | cbs 16840 |
. . . . 5
class
Base |
| 7 | 5, 6 | cfv 6418 |
. . . 4
class
(Base‘𝑔) |
| 8 | | va |
. . . . 5
setvar 𝑎 |
| 9 | 4 | cv 1538 |
. . . . . . . . 9
class 𝑚 |
| 10 | | vb |
. . . . . . . . . 10
setvar 𝑏 |
| 11 | 10 | cv 1538 |
. . . . . . . . 9
class 𝑏 |
| 12 | | cds 16897 |
. . . . . . . . . 10
class
dist |
| 13 | 5, 12 | cfv 6418 |
. . . . . . . . 9
class
(dist‘𝑔) |
| 14 | 9, 11, 13 | co 7255 |
. . . . . . . 8
class (𝑚(dist‘𝑔)𝑏) |
| 15 | 8 | cv 1538 |
. . . . . . . . 9
class 𝑎 |
| 16 | 9, 15, 13 | co 7255 |
. . . . . . . 8
class (𝑚(dist‘𝑔)𝑎) |
| 17 | 14, 16 | wceq 1539 |
. . . . . . 7
wff (𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) |
| 18 | | citv 26699 |
. . . . . . . . . 10
class
Itv |
| 19 | 5, 18 | cfv 6418 |
. . . . . . . . 9
class
(Itv‘𝑔) |
| 20 | 11, 15, 19 | co 7255 |
. . . . . . . 8
class (𝑏(Itv‘𝑔)𝑎) |
| 21 | 9, 20 | wcel 2108 |
. . . . . . 7
wff 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎) |
| 22 | 17, 21 | wa 395 |
. . . . . 6
wff ((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)) |
| 23 | 22, 10, 7 | crio 7211 |
. . . . 5
class
(℩𝑏
∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))) |
| 24 | 8, 7, 23 | cmpt 5153 |
. . . 4
class (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)))) |
| 25 | 4, 7, 24 | cmpt 5153 |
. . 3
class (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))) |
| 26 | 2, 3, 25 | cmpt 5153 |
. 2
class (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)))))) |
| 27 | 1, 26 | wceq 1539 |
1
wff pInvG =
(𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)))))) |
