Step | Hyp | Ref
| Expression |
1 | | cmgc 31888 |
. 2
class
MGalConn |
2 | | vv |
. . 3
setvar π£ |
3 | | vw |
. . 3
setvar π€ |
4 | | cvv 3444 |
. . 3
class
V |
5 | | va |
. . . 4
setvar π |
6 | 2 | cv 1541 |
. . . . 5
class π£ |
7 | | cbs 17088 |
. . . . 5
class
Base |
8 | 6, 7 | cfv 6497 |
. . . 4
class
(Baseβπ£) |
9 | | vb |
. . . . 5
setvar π |
10 | 3 | cv 1541 |
. . . . . 6
class π€ |
11 | 10, 7 | cfv 6497 |
. . . . 5
class
(Baseβπ€) |
12 | | vf |
. . . . . . . . . 10
setvar π |
13 | 12 | cv 1541 |
. . . . . . . . 9
class π |
14 | 9 | cv 1541 |
. . . . . . . . . 10
class π |
15 | 5 | cv 1541 |
. . . . . . . . . 10
class π |
16 | | cmap 8768 |
. . . . . . . . . 10
class
βm |
17 | 14, 15, 16 | co 7358 |
. . . . . . . . 9
class (π βm π) |
18 | 13, 17 | wcel 2107 |
. . . . . . . 8
wff π β (π βm π) |
19 | | vg |
. . . . . . . . . 10
setvar π |
20 | 19 | cv 1541 |
. . . . . . . . 9
class π |
21 | 15, 14, 16 | co 7358 |
. . . . . . . . 9
class (π βm π) |
22 | 20, 21 | wcel 2107 |
. . . . . . . 8
wff π β (π βm π) |
23 | 18, 22 | wa 397 |
. . . . . . 7
wff (π β (π βm π) β§ π β (π βm π)) |
24 | | vx |
. . . . . . . . . . . . 13
setvar π₯ |
25 | 24 | cv 1541 |
. . . . . . . . . . . 12
class π₯ |
26 | 25, 13 | cfv 6497 |
. . . . . . . . . . 11
class (πβπ₯) |
27 | | vy |
. . . . . . . . . . . 12
setvar π¦ |
28 | 27 | cv 1541 |
. . . . . . . . . . 11
class π¦ |
29 | | cple 17145 |
. . . . . . . . . . . 12
class
le |
30 | 10, 29 | cfv 6497 |
. . . . . . . . . . 11
class
(leβπ€) |
31 | 26, 28, 30 | wbr 5106 |
. . . . . . . . . 10
wff (πβπ₯)(leβπ€)π¦ |
32 | 28, 20 | cfv 6497 |
. . . . . . . . . . 11
class (πβπ¦) |
33 | 6, 29 | cfv 6497 |
. . . . . . . . . . 11
class
(leβπ£) |
34 | 25, 32, 33 | wbr 5106 |
. . . . . . . . . 10
wff π₯(leβπ£)(πβπ¦) |
35 | 31, 34 | wb 205 |
. . . . . . . . 9
wff ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)) |
36 | 35, 27, 14 | wral 3061 |
. . . . . . . 8
wff
βπ¦ β
π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)) |
37 | 36, 24, 15 | wral 3061 |
. . . . . . 7
wff
βπ₯ β
π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)) |
38 | 23, 37 | wa 397 |
. . . . . 6
wff ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦))) |
39 | 38, 12, 19 | copab 5168 |
. . . . 5
class
{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))} |
40 | 9, 11, 39 | csb 3856 |
. . . 4
class
β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))} |
41 | 5, 8, 40 | csb 3856 |
. . 3
class
β¦(Baseβπ£) / πβ¦β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))} |
42 | 2, 3, 4, 4, 41 | cmpo 7360 |
. 2
class (π£ β V, π€ β V β¦
β¦(Baseβπ£) / πβ¦β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))}) |
43 | 1, 42 | wceq 1542 |
1
wff MGalConn =
(π£ β V, π€ β V β¦
β¦(Baseβπ£) / πβ¦β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))}) |