Step | Hyp | Ref
| Expression |
1 | | cdic 40043 |
. 2
class
DIsoC |
2 | | vk |
. . 3
setvar π |
3 | | cvv 3475 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar π€ |
5 | 2 | cv 1541 |
. . . . 5
class π |
6 | | clh 38855 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6544 |
. . . 4
class
(LHypβπ) |
8 | | vq |
. . . . 5
setvar π |
9 | | vr |
. . . . . . . . 9
setvar π |
10 | 9 | cv 1541 |
. . . . . . . 8
class π |
11 | 4 | cv 1541 |
. . . . . . . 8
class π€ |
12 | | cple 17204 |
. . . . . . . . 9
class
le |
13 | 5, 12 | cfv 6544 |
. . . . . . . 8
class
(leβπ) |
14 | 10, 11, 13 | wbr 5149 |
. . . . . . 7
wff π(leβπ)π€ |
15 | 14 | wn 3 |
. . . . . 6
wff Β¬
π(leβπ)π€ |
16 | | catm 38133 |
. . . . . . 7
class
Atoms |
17 | 5, 16 | cfv 6544 |
. . . . . 6
class
(Atomsβπ) |
18 | 15, 9, 17 | crab 3433 |
. . . . 5
class {π β (Atomsβπ) β£ Β¬ π(leβπ)π€} |
19 | | vf |
. . . . . . . . 9
setvar π |
20 | 19 | cv 1541 |
. . . . . . . 8
class π |
21 | | coc 17205 |
. . . . . . . . . . . . . 14
class
oc |
22 | 5, 21 | cfv 6544 |
. . . . . . . . . . . . 13
class
(ocβπ) |
23 | 11, 22 | cfv 6544 |
. . . . . . . . . . . 12
class
((ocβπ)βπ€) |
24 | | vg |
. . . . . . . . . . . . 13
setvar π |
25 | 24 | cv 1541 |
. . . . . . . . . . . 12
class π |
26 | 23, 25 | cfv 6544 |
. . . . . . . . . . 11
class (πβ((ocβπ)βπ€)) |
27 | 8 | cv 1541 |
. . . . . . . . . . 11
class π |
28 | 26, 27 | wceq 1542 |
. . . . . . . . . 10
wff (πβ((ocβπ)βπ€)) = π |
29 | | cltrn 38972 |
. . . . . . . . . . . 12
class
LTrn |
30 | 5, 29 | cfv 6544 |
. . . . . . . . . . 11
class
(LTrnβπ) |
31 | 11, 30 | cfv 6544 |
. . . . . . . . . 10
class
((LTrnβπ)βπ€) |
32 | 28, 24, 31 | crio 7364 |
. . . . . . . . 9
class
(β©π
β ((LTrnβπ)βπ€)(πβ((ocβπ)βπ€)) = π) |
33 | | vs |
. . . . . . . . . 10
setvar π |
34 | 33 | cv 1541 |
. . . . . . . . 9
class π |
35 | 32, 34 | cfv 6544 |
. . . . . . . 8
class (π β(β©π β ((LTrnβπ)βπ€)(πβ((ocβπ)βπ€)) = π)) |
36 | 20, 35 | wceq 1542 |
. . . . . . 7
wff π = (π β(β©π β ((LTrnβπ)βπ€)(πβ((ocβπ)βπ€)) = π)) |
37 | | ctendo 39623 |
. . . . . . . . . 10
class
TEndo |
38 | 5, 37 | cfv 6544 |
. . . . . . . . 9
class
(TEndoβπ) |
39 | 11, 38 | cfv 6544 |
. . . . . . . 8
class
((TEndoβπ)βπ€) |
40 | 34, 39 | wcel 2107 |
. . . . . . 7
wff π β ((TEndoβπ)βπ€) |
41 | 36, 40 | wa 397 |
. . . . . 6
wff (π = (π β(β©π β ((LTrnβπ)βπ€)(πβ((ocβπ)βπ€)) = π)) β§ π β ((TEndoβπ)βπ€)) |
42 | 41, 19, 33 | copab 5211 |
. . . . 5
class
{β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπ)βπ€)(πβ((ocβπ)βπ€)) = π)) β§ π β ((TEndoβπ)βπ€))} |
43 | 8, 18, 42 | cmpt 5232 |
. . . 4
class (π β {π β (Atomsβπ) β£ Β¬ π(leβπ)π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπ)βπ€)(πβ((ocβπ)βπ€)) = π)) β§ π β ((TEndoβπ)βπ€))}) |
44 | 4, 7, 43 | cmpt 5232 |
. . 3
class (π€ β (LHypβπ) β¦ (π β {π β (Atomsβπ) β£ Β¬ π(leβπ)π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπ)βπ€)(πβ((ocβπ)βπ€)) = π)) β§ π β ((TEndoβπ)βπ€))})) |
45 | 2, 3, 44 | cmpt 5232 |
. 2
class (π β V β¦ (π€ β (LHypβπ) β¦ (π β {π β (Atomsβπ) β£ Β¬ π(leβπ)π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπ)βπ€)(πβ((ocβπ)βπ€)) = π)) β§ π β ((TEndoβπ)βπ€))}))) |
46 | 1, 45 | wceq 1542 |
1
wff DIsoC =
(π β V β¦ (π€ β (LHypβπ) β¦ (π β {π β (Atomsβπ) β£ Β¬ π(leβπ)π€} β¦ {β¨π, π β© β£ (π = (π β(β©π β ((LTrnβπ)βπ€)(πβ((ocβπ)βπ€)) = π)) β§ π β ((TEndoβπ)βπ€))}))) |