Step | Hyp | Ref
| Expression |
1 | | cttg 28121 |
. 2
class
toTG |
2 | | vw |
. . 3
setvar π€ |
3 | | cvv 3474 |
. . 3
class
V |
4 | | vi |
. . . 4
setvar π |
5 | | vx |
. . . . 5
setvar π₯ |
6 | | vy |
. . . . 5
setvar π¦ |
7 | 2 | cv 1540 |
. . . . . 6
class π€ |
8 | | cbs 17143 |
. . . . . 6
class
Base |
9 | 7, 8 | cfv 6543 |
. . . . 5
class
(Baseβπ€) |
10 | | vz |
. . . . . . . . . 10
setvar π§ |
11 | 10 | cv 1540 |
. . . . . . . . 9
class π§ |
12 | 5 | cv 1540 |
. . . . . . . . 9
class π₯ |
13 | | csg 18820 |
. . . . . . . . . 10
class
-g |
14 | 7, 13 | cfv 6543 |
. . . . . . . . 9
class
(-gβπ€) |
15 | 11, 12, 14 | co 7408 |
. . . . . . . 8
class (π§(-gβπ€)π₯) |
16 | | vk |
. . . . . . . . . 10
setvar π |
17 | 16 | cv 1540 |
. . . . . . . . 9
class π |
18 | 6 | cv 1540 |
. . . . . . . . . 10
class π¦ |
19 | 18, 12, 14 | co 7408 |
. . . . . . . . 9
class (π¦(-gβπ€)π₯) |
20 | | cvsca 17200 |
. . . . . . . . . 10
class
Β·π |
21 | 7, 20 | cfv 6543 |
. . . . . . . . 9
class (
Β·π βπ€) |
22 | 17, 19, 21 | co 7408 |
. . . . . . . 8
class (π(
Β·π βπ€)(π¦(-gβπ€)π₯)) |
23 | 15, 22 | wceq 1541 |
. . . . . . 7
wff (π§(-gβπ€)π₯) = (π( Β·π
βπ€)(π¦(-gβπ€)π₯)) |
24 | | cc0 11109 |
. . . . . . . 8
class
0 |
25 | | c1 11110 |
. . . . . . . 8
class
1 |
26 | | cicc 13326 |
. . . . . . . 8
class
[,] |
27 | 24, 25, 26 | co 7408 |
. . . . . . 7
class
(0[,]1) |
28 | 23, 16, 27 | wrex 3070 |
. . . . . 6
wff
βπ β
(0[,]1)(π§(-gβπ€)π₯) = (π( Β·π
βπ€)(π¦(-gβπ€)π₯)) |
29 | 28, 10, 9 | crab 3432 |
. . . . 5
class {π§ β (Baseβπ€) β£ βπ β (0[,]1)(π§(-gβπ€)π₯) = (π( Β·π
βπ€)(π¦(-gβπ€)π₯))} |
30 | 5, 6, 9, 9, 29 | cmpo 7410 |
. . . 4
class (π₯ β (Baseβπ€), π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ βπ β (0[,]1)(π§(-gβπ€)π₯) = (π( Β·π
βπ€)(π¦(-gβπ€)π₯))}) |
31 | | cnx 17125 |
. . . . . . . 8
class
ndx |
32 | | citv 27681 |
. . . . . . . 8
class
Itv |
33 | 31, 32 | cfv 6543 |
. . . . . . 7
class
(Itvβndx) |
34 | 4 | cv 1540 |
. . . . . . 7
class π |
35 | 33, 34 | cop 4634 |
. . . . . 6
class
β¨(Itvβndx), πβ© |
36 | | csts 17095 |
. . . . . 6
class
sSet |
37 | 7, 35, 36 | co 7408 |
. . . . 5
class (π€ sSet β¨(Itvβndx),
πβ©) |
38 | | clng 27682 |
. . . . . . 7
class
LineG |
39 | 31, 38 | cfv 6543 |
. . . . . 6
class
(LineGβndx) |
40 | 12, 18, 34 | co 7408 |
. . . . . . . . . 10
class (π₯ππ¦) |
41 | 11, 40 | wcel 2106 |
. . . . . . . . 9
wff π§ β (π₯ππ¦) |
42 | 11, 18, 34 | co 7408 |
. . . . . . . . . 10
class (π§ππ¦) |
43 | 12, 42 | wcel 2106 |
. . . . . . . . 9
wff π₯ β (π§ππ¦) |
44 | 12, 11, 34 | co 7408 |
. . . . . . . . . 10
class (π₯ππ§) |
45 | 18, 44 | wcel 2106 |
. . . . . . . . 9
wff π¦ β (π₯ππ§) |
46 | 41, 43, 45 | w3o 1086 |
. . . . . . . 8
wff (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) |
47 | 46, 10, 9 | crab 3432 |
. . . . . . 7
class {π§ β (Baseβπ€) β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))} |
48 | 5, 6, 9, 9, 47 | cmpo 7410 |
. . . . . 6
class (π₯ β (Baseβπ€), π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))}) |
49 | 39, 48 | cop 4634 |
. . . . 5
class
β¨(LineGβndx), (π₯ β (Baseβπ€), π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})β© |
50 | 37, 49, 36 | co 7408 |
. . . 4
class ((π€ sSet β¨(Itvβndx),
πβ©) sSet
β¨(LineGβndx), (π₯
β (Baseβπ€),
π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})β©) |
51 | 4, 30, 50 | csb 3893 |
. . 3
class
β¦(π₯
β (Baseβπ€),
π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ βπ β (0[,]1)(π§(-gβπ€)π₯) = (π( Β·π
βπ€)(π¦(-gβπ€)π₯))}) / πβ¦((π€ sSet β¨(Itvβndx), πβ©) sSet
β¨(LineGβndx), (π₯
β (Baseβπ€),
π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})β©) |
52 | 2, 3, 51 | cmpt 5231 |
. 2
class (π€ β V β¦
β¦(π₯ β
(Baseβπ€), π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ βπ β (0[,]1)(π§(-gβπ€)π₯) = (π( Β·π
βπ€)(π¦(-gβπ€)π₯))}) / πβ¦((π€ sSet β¨(Itvβndx), πβ©) sSet
β¨(LineGβndx), (π₯
β (Baseβπ€),
π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})β©)) |
53 | 1, 52 | wceq 1541 |
1
wff toTG =
(π€ β V β¦
β¦(π₯ β
(Baseβπ€), π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ βπ β (0[,]1)(π§(-gβπ€)π₯) = (π( Β·π
βπ€)(π¦(-gβπ€)π₯))}) / πβ¦((π€ sSet β¨(Itvβndx), πβ©) sSet
β¨(LineGβndx), (π₯
β (Baseβπ€),
π¦ β (Baseβπ€) β¦ {π§ β (Baseβπ€) β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})β©)) |