Step | Hyp | Ref
| Expression |
1 | | cocaN 39585 |
. 2
class
ocA |
2 | | vk |
. . 3
setvar π |
3 | | cvv 3446 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar π€ |
5 | 2 | cv 1541 |
. . . . 5
class π |
6 | | clh 38450 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6497 |
. . . 4
class
(LHypβπ) |
8 | | vx |
. . . . 5
setvar π₯ |
9 | 4 | cv 1541 |
. . . . . . 7
class π€ |
10 | | cltrn 38567 |
. . . . . . . 8
class
LTrn |
11 | 5, 10 | cfv 6497 |
. . . . . . 7
class
(LTrnβπ) |
12 | 9, 11 | cfv 6497 |
. . . . . 6
class
((LTrnβπ)βπ€) |
13 | 12 | cpw 4561 |
. . . . 5
class π«
((LTrnβπ)βπ€) |
14 | 8 | cv 1541 |
. . . . . . . . . . . . 13
class π₯ |
15 | | vz |
. . . . . . . . . . . . . 14
setvar π§ |
16 | 15 | cv 1541 |
. . . . . . . . . . . . 13
class π§ |
17 | 14, 16 | wss 3911 |
. . . . . . . . . . . 12
wff π₯ β π§ |
18 | | cdia 39494 |
. . . . . . . . . . . . . . 15
class
DIsoA |
19 | 5, 18 | cfv 6497 |
. . . . . . . . . . . . . 14
class
(DIsoAβπ) |
20 | 9, 19 | cfv 6497 |
. . . . . . . . . . . . 13
class
((DIsoAβπ)βπ€) |
21 | 20 | crn 5635 |
. . . . . . . . . . . 12
class ran
((DIsoAβπ)βπ€) |
22 | 17, 15, 21 | crab 3408 |
. . . . . . . . . . 11
class {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§} |
23 | 22 | cint 4908 |
. . . . . . . . . 10
class β© {π§
β ran ((DIsoAβπ)βπ€) β£ π₯ β π§} |
24 | 20 | ccnv 5633 |
. . . . . . . . . 10
class β‘((DIsoAβπ)βπ€) |
25 | 23, 24 | cfv 6497 |
. . . . . . . . 9
class (β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}) |
26 | | coc 17142 |
. . . . . . . . . 10
class
oc |
27 | 5, 26 | cfv 6497 |
. . . . . . . . 9
class
(ocβπ) |
28 | 25, 27 | cfv 6497 |
. . . . . . . 8
class
((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§})) |
29 | 9, 27 | cfv 6497 |
. . . . . . . 8
class
((ocβπ)βπ€) |
30 | | cjn 18201 |
. . . . . . . . 9
class
join |
31 | 5, 30 | cfv 6497 |
. . . . . . . 8
class
(joinβπ) |
32 | 28, 29, 31 | co 7358 |
. . . . . . 7
class
(((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€)) |
33 | | cmee 18202 |
. . . . . . . 8
class
meet |
34 | 5, 33 | cfv 6497 |
. . . . . . 7
class
(meetβπ) |
35 | 32, 9, 34 | co 7358 |
. . . . . 6
class
((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€) |
36 | 35, 20 | cfv 6497 |
. . . . 5
class
(((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€)) |
37 | 8, 13, 36 | cmpt 5189 |
. . . 4
class (π₯ β π«
((LTrnβπ)βπ€) β¦ (((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€))) |
38 | 4, 7, 37 | cmpt 5189 |
. . 3
class (π€ β (LHypβπ) β¦ (π₯ β π« ((LTrnβπ)βπ€) β¦ (((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€)))) |
39 | 2, 3, 38 | cmpt 5189 |
. 2
class (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π« ((LTrnβπ)βπ€) β¦ (((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€))))) |
40 | 1, 39 | wceq 1542 |
1
wff ocA =
(π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π« ((LTrnβπ)βπ€) β¦ (((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€))))) |