Detailed syntax breakdown of Definition df-ttg
Step | Hyp | Ref
| Expression |
1 | | cttg 27232 |
. 2
class
toTG |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | vi |
. . . 4
setvar 𝑖 |
5 | | vx |
. . . . 5
setvar 𝑥 |
6 | | vy |
. . . . 5
setvar 𝑦 |
7 | 2 | cv 1538 |
. . . . . 6
class 𝑤 |
8 | | cbs 16910 |
. . . . . 6
class
Base |
9 | 7, 8 | cfv 6435 |
. . . . 5
class
(Base‘𝑤) |
10 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
11 | 10 | cv 1538 |
. . . . . . . . 9
class 𝑧 |
12 | 5 | cv 1538 |
. . . . . . . . 9
class 𝑥 |
13 | | csg 18577 |
. . . . . . . . . 10
class
-g |
14 | 7, 13 | cfv 6435 |
. . . . . . . . 9
class
(-g‘𝑤) |
15 | 11, 12, 14 | co 7277 |
. . . . . . . 8
class (𝑧(-g‘𝑤)𝑥) |
16 | | vk |
. . . . . . . . . 10
setvar 𝑘 |
17 | 16 | cv 1538 |
. . . . . . . . 9
class 𝑘 |
18 | 6 | cv 1538 |
. . . . . . . . . 10
class 𝑦 |
19 | 18, 12, 14 | co 7277 |
. . . . . . . . 9
class (𝑦(-g‘𝑤)𝑥) |
20 | | cvsca 16964 |
. . . . . . . . . 10
class
·𝑠 |
21 | 7, 20 | cfv 6435 |
. . . . . . . . 9
class (
·𝑠 ‘𝑤) |
22 | 17, 19, 21 | co 7277 |
. . . . . . . 8
class (𝑘(
·𝑠 ‘𝑤)(𝑦(-g‘𝑤)𝑥)) |
23 | 15, 22 | wceq 1539 |
. . . . . . 7
wff (𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠
‘𝑤)(𝑦(-g‘𝑤)𝑥)) |
24 | | cc0 10869 |
. . . . . . . 8
class
0 |
25 | | c1 10870 |
. . . . . . . 8
class
1 |
26 | | cicc 13080 |
. . . . . . . 8
class
[,] |
27 | 24, 25, 26 | co 7277 |
. . . . . . 7
class
(0[,]1) |
28 | 23, 16, 27 | wrex 3065 |
. . . . . 6
wff
∃𝑘 ∈
(0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠
‘𝑤)(𝑦(-g‘𝑤)𝑥)) |
29 | 28, 10, 9 | crab 3068 |
. . . . 5
class {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠
‘𝑤)(𝑦(-g‘𝑤)𝑥))} |
30 | 5, 6, 9, 9, 29 | cmpo 7279 |
. . . 4
class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠
‘𝑤)(𝑦(-g‘𝑤)𝑥))}) |
31 | | cnx 16892 |
. . . . . . . 8
class
ndx |
32 | | citv 26792 |
. . . . . . . 8
class
Itv |
33 | 31, 32 | cfv 6435 |
. . . . . . 7
class
(Itv‘ndx) |
34 | 4 | cv 1538 |
. . . . . . 7
class 𝑖 |
35 | 33, 34 | cop 4569 |
. . . . . 6
class
〈(Itv‘ndx), 𝑖〉 |
36 | | csts 16862 |
. . . . . 6
class
sSet |
37 | 7, 35, 36 | co 7277 |
. . . . 5
class (𝑤 sSet 〈(Itv‘ndx),
𝑖〉) |
38 | | clng 26793 |
. . . . . . 7
class
LineG |
39 | 31, 38 | cfv 6435 |
. . . . . 6
class
(LineG‘ndx) |
40 | 12, 18, 34 | co 7277 |
. . . . . . . . . 10
class (𝑥𝑖𝑦) |
41 | 11, 40 | wcel 2106 |
. . . . . . . . 9
wff 𝑧 ∈ (𝑥𝑖𝑦) |
42 | 11, 18, 34 | co 7277 |
. . . . . . . . . 10
class (𝑧𝑖𝑦) |
43 | 12, 42 | wcel 2106 |
. . . . . . . . 9
wff 𝑥 ∈ (𝑧𝑖𝑦) |
44 | 12, 11, 34 | co 7277 |
. . . . . . . . . 10
class (𝑥𝑖𝑧) |
45 | 18, 44 | wcel 2106 |
. . . . . . . . 9
wff 𝑦 ∈ (𝑥𝑖𝑧) |
46 | 41, 43, 45 | w3o 1085 |
. . . . . . . 8
wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) |
47 | 46, 10, 9 | crab 3068 |
. . . . . . 7
class {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} |
48 | 5, 6, 9, 9, 47 | cmpo 7279 |
. . . . . 6
class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) |
49 | 39, 48 | cop 4569 |
. . . . 5
class
〈(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})〉 |
50 | 37, 49, 36 | co 7277 |
. . . 4
class ((𝑤 sSet 〈(Itv‘ndx),
𝑖〉) sSet
〈(LineG‘ndx), (𝑥
∈ (Base‘𝑤),
𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})〉) |
51 | 4, 30, 50 | csb 3833 |
. . 3
class
⦋(𝑥
∈ (Base‘𝑤),
𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠
‘𝑤)(𝑦(-g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet 〈(Itv‘ndx), 𝑖〉) sSet
〈(LineG‘ndx), (𝑥
∈ (Base‘𝑤),
𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})〉) |
52 | 2, 3, 51 | cmpt 5159 |
. 2
class (𝑤 ∈ V ↦
⦋(𝑥 ∈
(Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠
‘𝑤)(𝑦(-g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet 〈(Itv‘ndx), 𝑖〉) sSet
〈(LineG‘ndx), (𝑥
∈ (Base‘𝑤),
𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})〉)) |
53 | 1, 52 | wceq 1539 |
1
wff toTG =
(𝑤 ∈ V ↦
⦋(𝑥 ∈
(Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝑤)𝑥) = (𝑘( ·𝑠
‘𝑤)(𝑦(-g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet 〈(Itv‘ndx), 𝑖〉) sSet
〈(LineG‘ndx), (𝑥
∈ (Base‘𝑤),
𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})〉)) |