Detailed syntax breakdown of Definition df-lmi
Step | Hyp | Ref
| Expression |
1 | | clmi 27038 |
. 2
class
lInvG |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3422 |
. . 3
class
V |
4 | | vm |
. . . 4
setvar 𝑚 |
5 | 2 | cv 1538 |
. . . . . 6
class 𝑔 |
6 | | clng 26700 |
. . . . . 6
class
LineG |
7 | 5, 6 | cfv 6418 |
. . . . 5
class
(LineG‘𝑔) |
8 | 7 | crn 5581 |
. . . 4
class ran
(LineG‘𝑔) |
9 | | va |
. . . . 5
setvar 𝑎 |
10 | | cbs 16840 |
. . . . . 6
class
Base |
11 | 5, 10 | cfv 6418 |
. . . . 5
class
(Base‘𝑔) |
12 | 9 | cv 1538 |
. . . . . . . . 9
class 𝑎 |
13 | | vb |
. . . . . . . . . 10
setvar 𝑏 |
14 | 13 | cv 1538 |
. . . . . . . . 9
class 𝑏 |
15 | | cmid 27037 |
. . . . . . . . . 10
class
midG |
16 | 5, 15 | cfv 6418 |
. . . . . . . . 9
class
(midG‘𝑔) |
17 | 12, 14, 16 | co 7255 |
. . . . . . . 8
class (𝑎(midG‘𝑔)𝑏) |
18 | 4 | cv 1538 |
. . . . . . . 8
class 𝑚 |
19 | 17, 18 | wcel 2108 |
. . . . . . 7
wff (𝑎(midG‘𝑔)𝑏) ∈ 𝑚 |
20 | 12, 14, 7 | co 7255 |
. . . . . . . . 9
class (𝑎(LineG‘𝑔)𝑏) |
21 | | cperpg 26960 |
. . . . . . . . . 10
class
⟂G |
22 | 5, 21 | cfv 6418 |
. . . . . . . . 9
class
(⟂G‘𝑔) |
23 | 18, 20, 22 | wbr 5070 |
. . . . . . . 8
wff 𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) |
24 | 9, 13 | weq 1967 |
. . . . . . . 8
wff 𝑎 = 𝑏 |
25 | 23, 24 | wo 843 |
. . . . . . 7
wff (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏) |
26 | 19, 25 | wa 395 |
. . . . . 6
wff ((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)) |
27 | 26, 13, 11 | crio 7211 |
. . . . 5
class
(℩𝑏
∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))) |
28 | 9, 11, 27 | cmpt 5153 |
. . . 4
class (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))) |
29 | 4, 8, 28 | cmpt 5153 |
. . 3
class (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))) |
30 | 2, 3, 29 | cmpt 5153 |
. 2
class (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))))) |
31 | 1, 30 | wceq 1539 |
1
wff lInvG =
(𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))))) |