Step | Hyp | Ref
| Expression |
1 | | ctendo 39926 |
. 2
class
TEndo |
2 | | vk |
. . 3
setvar π |
3 | | cvv 3472 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar π€ |
5 | 2 | cv 1538 |
. . . . 5
class π |
6 | | clh 39158 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6542 |
. . . 4
class
(LHypβπ) |
8 | 4 | cv 1538 |
. . . . . . . 8
class π€ |
9 | | cltrn 39275 |
. . . . . . . . 9
class
LTrn |
10 | 5, 9 | cfv 6542 |
. . . . . . . 8
class
(LTrnβπ) |
11 | 8, 10 | cfv 6542 |
. . . . . . 7
class
((LTrnβπ)βπ€) |
12 | | vf |
. . . . . . . 8
setvar π |
13 | 12 | cv 1538 |
. . . . . . 7
class π |
14 | 11, 11, 13 | wf 6538 |
. . . . . 6
wff π:((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) |
15 | | vx |
. . . . . . . . . . . 12
setvar π₯ |
16 | 15 | cv 1538 |
. . . . . . . . . . 11
class π₯ |
17 | | vy |
. . . . . . . . . . . 12
setvar π¦ |
18 | 17 | cv 1538 |
. . . . . . . . . . 11
class π¦ |
19 | 16, 18 | ccom 5679 |
. . . . . . . . . 10
class (π₯ β π¦) |
20 | 19, 13 | cfv 6542 |
. . . . . . . . 9
class (πβ(π₯ β π¦)) |
21 | 16, 13 | cfv 6542 |
. . . . . . . . . 10
class (πβπ₯) |
22 | 18, 13 | cfv 6542 |
. . . . . . . . . 10
class (πβπ¦) |
23 | 21, 22 | ccom 5679 |
. . . . . . . . 9
class ((πβπ₯) β (πβπ¦)) |
24 | 20, 23 | wceq 1539 |
. . . . . . . 8
wff (πβ(π₯ β π¦)) = ((πβπ₯) β (πβπ¦)) |
25 | 24, 17, 11 | wral 3059 |
. . . . . . 7
wff
βπ¦ β
((LTrnβπ)βπ€)(πβ(π₯ β π¦)) = ((πβπ₯) β (πβπ¦)) |
26 | 25, 15, 11 | wral 3059 |
. . . . . 6
wff
βπ₯ β
((LTrnβπ)βπ€)βπ¦ β ((LTrnβπ)βπ€)(πβ(π₯ β π¦)) = ((πβπ₯) β (πβπ¦)) |
27 | | ctrl 39332 |
. . . . . . . . . . 11
class
trL |
28 | 5, 27 | cfv 6542 |
. . . . . . . . . 10
class
(trLβπ) |
29 | 8, 28 | cfv 6542 |
. . . . . . . . 9
class
((trLβπ)βπ€) |
30 | 21, 29 | cfv 6542 |
. . . . . . . 8
class
(((trLβπ)βπ€)β(πβπ₯)) |
31 | 16, 29 | cfv 6542 |
. . . . . . . 8
class
(((trLβπ)βπ€)βπ₯) |
32 | | cple 17208 |
. . . . . . . . 9
class
le |
33 | 5, 32 | cfv 6542 |
. . . . . . . 8
class
(leβπ) |
34 | 30, 31, 33 | wbr 5147 |
. . . . . . 7
wff
(((trLβπ)βπ€)β(πβπ₯))(leβπ)(((trLβπ)βπ€)βπ₯) |
35 | 34, 15, 11 | wral 3059 |
. . . . . 6
wff
βπ₯ β
((LTrnβπ)βπ€)(((trLβπ)βπ€)β(πβπ₯))(leβπ)(((trLβπ)βπ€)βπ₯) |
36 | 14, 26, 35 | w3a 1085 |
. . . . 5
wff (π:((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ₯ β ((LTrnβπ)βπ€)βπ¦ β ((LTrnβπ)βπ€)(πβ(π₯ β π¦)) = ((πβπ₯) β (πβπ¦)) β§ βπ₯ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(πβπ₯))(leβπ)(((trLβπ)βπ€)βπ₯)) |
37 | 36, 12 | cab 2707 |
. . . 4
class {π β£ (π:((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ₯ β ((LTrnβπ)βπ€)βπ¦ β ((LTrnβπ)βπ€)(πβ(π₯ β π¦)) = ((πβπ₯) β (πβπ¦)) β§ βπ₯ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(πβπ₯))(leβπ)(((trLβπ)βπ€)βπ₯))} |
38 | 4, 7, 37 | cmpt 5230 |
. . 3
class (π€ β (LHypβπ) β¦ {π β£ (π:((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ₯ β ((LTrnβπ)βπ€)βπ¦ β ((LTrnβπ)βπ€)(πβ(π₯ β π¦)) = ((πβπ₯) β (πβπ¦)) β§ βπ₯ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(πβπ₯))(leβπ)(((trLβπ)βπ€)βπ₯))}) |
39 | 2, 3, 38 | cmpt 5230 |
. 2
class (π β V β¦ (π€ β (LHypβπ) β¦ {π β£ (π:((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ₯ β ((LTrnβπ)βπ€)βπ¦ β ((LTrnβπ)βπ€)(πβ(π₯ β π¦)) = ((πβπ₯) β (πβπ¦)) β§ βπ₯ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(πβπ₯))(leβπ)(((trLβπ)βπ€)βπ₯))})) |
40 | 1, 39 | wceq 1539 |
1
wff TEndo =
(π β V β¦ (π€ β (LHypβπ) β¦ {π β£ (π:((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ₯ β ((LTrnβπ)βπ€)βπ¦ β ((LTrnβπ)βπ€)(πβ(π₯ β π¦)) = ((πβπ₯) β (πβπ¦)) β§ βπ₯ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(πβπ₯))(leβπ)(((trLβπ)βπ€)βπ₯))})) |