Step | Hyp | Ref
| Expression |
1 | | ancom 462 |
. . . 4
β’ ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β (πΊ:(Baseβπ)βΆ(Baseβπ) β§ πΉ:(Baseβπ)βΆ(Baseβπ))) |
2 | 1 | a1i 11 |
. . 3
β’ ((π β Proset β§ π β Proset ) β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β (πΊ:(Baseβπ)βΆ(Baseβπ) β§ πΉ:(Baseβπ)βΆ(Baseβπ)))) |
3 | | ralcom 3271 |
. . . 4
β’
(βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((πΉβπ₯)(leβπ)π¦ β π₯(leβπ)(πΊβπ¦)) β βπ¦ β (Baseβπ)βπ₯ β (Baseβπ)((πΉβπ₯)(leβπ)π¦ β π₯(leβπ)(πΊβπ¦))) |
4 | | bicom 221 |
. . . . . . 7
β’ (((πΉβπ₯)(leβπ)π¦ β π₯(leβπ)(πΊβπ¦)) β (π₯(leβπ)(πΊβπ¦) β (πΉβπ₯)(leβπ)π¦)) |
5 | | fvex 6856 |
. . . . . . . . . . 11
β’ (πΊβπ¦) β V |
6 | | vex 3448 |
. . . . . . . . . . 11
β’ π₯ β V |
7 | 5, 6 | brcnv 5839 |
. . . . . . . . . 10
β’ ((πΊβπ¦)β‘(leβπ)π₯ β π₯(leβπ)(πΊβπ¦)) |
8 | 7 | bicomi 223 |
. . . . . . . . 9
β’ (π₯(leβπ)(πΊβπ¦) β (πΊβπ¦)β‘(leβπ)π₯) |
9 | 8 | a1i 11 |
. . . . . . . 8
β’ ((((π β Proset β§ π β Proset ) β§ π¦ β (Baseβπ)) β§ π₯ β (Baseβπ)) β (π₯(leβπ)(πΊβπ¦) β (πΊβπ¦)β‘(leβπ)π₯)) |
10 | | vex 3448 |
. . . . . . . . . . 11
β’ π¦ β V |
11 | | fvex 6856 |
. . . . . . . . . . 11
β’ (πΉβπ₯) β V |
12 | 10, 11 | brcnv 5839 |
. . . . . . . . . 10
β’ (π¦β‘(leβπ)(πΉβπ₯) β (πΉβπ₯)(leβπ)π¦) |
13 | 12 | bicomi 223 |
. . . . . . . . 9
β’ ((πΉβπ₯)(leβπ)π¦ β π¦β‘(leβπ)(πΉβπ₯)) |
14 | 13 | a1i 11 |
. . . . . . . 8
β’ ((((π β Proset β§ π β Proset ) β§ π¦ β (Baseβπ)) β§ π₯ β (Baseβπ)) β ((πΉβπ₯)(leβπ)π¦ β π¦β‘(leβπ)(πΉβπ₯))) |
15 | 9, 14 | bibi12d 346 |
. . . . . . 7
β’ ((((π β Proset β§ π β Proset ) β§ π¦ β (Baseβπ)) β§ π₯ β (Baseβπ)) β ((π₯(leβπ)(πΊβπ¦) β (πΉβπ₯)(leβπ)π¦) β ((πΊβπ¦)β‘(leβπ)π₯ β π¦β‘(leβπ)(πΉβπ₯)))) |
16 | 4, 15 | bitrid 283 |
. . . . . 6
β’ ((((π β Proset β§ π β Proset ) β§ π¦ β (Baseβπ)) β§ π₯ β (Baseβπ)) β (((πΉβπ₯)(leβπ)π¦ β π₯(leβπ)(πΊβπ¦)) β ((πΊβπ¦)β‘(leβπ)π₯ β π¦β‘(leβπ)(πΉβπ₯)))) |
17 | 16 | ralbidva 3169 |
. . . . 5
β’ (((π β Proset β§ π β Proset ) β§ π¦ β (Baseβπ)) β (βπ₯ β (Baseβπ)((πΉβπ₯)(leβπ)π¦ β π₯(leβπ)(πΊβπ¦)) β βπ₯ β (Baseβπ)((πΊβπ¦)β‘(leβπ)π₯ β π¦β‘(leβπ)(πΉβπ₯)))) |
18 | 17 | ralbidva 3169 |
. . . 4
β’ ((π β Proset β§ π β Proset ) β
(βπ¦ β
(Baseβπ)βπ₯ β (Baseβπ)((πΉβπ₯)(leβπ)π¦ β π₯(leβπ)(πΊβπ¦)) β βπ¦ β (Baseβπ)βπ₯ β (Baseβπ)((πΊβπ¦)β‘(leβπ)π₯ β π¦β‘(leβπ)(πΉβπ₯)))) |
19 | 3, 18 | bitrid 283 |
. . 3
β’ ((π β Proset β§ π β Proset ) β
(βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((πΉβπ₯)(leβπ)π¦ β π₯(leβπ)(πΊβπ¦)) β βπ¦ β (Baseβπ)βπ₯ β (Baseβπ)((πΊβπ¦)β‘(leβπ)π₯ β π¦β‘(leβπ)(πΉβπ₯)))) |
20 | 2, 19 | anbi12d 632 |
. 2
β’ ((π β Proset β§ π β Proset ) β (((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((πΉβπ₯)(leβπ)π¦ β π₯(leβπ)(πΊβπ¦))) β ((πΊ:(Baseβπ)βΆ(Baseβπ) β§ πΉ:(Baseβπ)βΆ(Baseβπ)) β§ βπ¦ β (Baseβπ)βπ₯ β (Baseβπ)((πΊβπ¦)β‘(leβπ)π₯ β π¦β‘(leβπ)(πΉβπ₯))))) |
21 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
22 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
23 | | eqid 2733 |
. . 3
β’
(leβπ) =
(leβπ) |
24 | | eqid 2733 |
. . 3
β’
(leβπ) =
(leβπ) |
25 | | mgccnv.1 |
. . 3
β’ π» = (πMGalConnπ) |
26 | | simpl 484 |
. . 3
β’ ((π β Proset β§ π β Proset ) β π β Proset
) |
27 | | simpr 486 |
. . 3
β’ ((π β Proset β§ π β Proset ) β π β Proset
) |
28 | 21, 22, 23, 24, 25, 26, 27 | mgcval 31896 |
. 2
β’ ((π β Proset β§ π β Proset ) β (πΉπ»πΊ β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((πΉβπ₯)(leβπ)π¦ β π₯(leβπ)(πΊβπ¦))))) |
29 | | eqid 2733 |
. . . 4
β’
(ODualβπ) =
(ODualβπ) |
30 | 29, 22 | odubas 18185 |
. . 3
β’
(Baseβπ) =
(Baseβ(ODualβπ)) |
31 | | eqid 2733 |
. . . 4
β’
(ODualβπ) =
(ODualβπ) |
32 | 31, 21 | odubas 18185 |
. . 3
β’
(Baseβπ) =
(Baseβ(ODualβπ)) |
33 | 29, 24 | oduleval 18183 |
. . 3
β’ β‘(leβπ) = (leβ(ODualβπ)) |
34 | 31, 23 | oduleval 18183 |
. . 3
β’ β‘(leβπ) = (leβ(ODualβπ)) |
35 | | mgccnv.2 |
. . 3
β’ π = ((ODualβπ)MGalConn(ODualβπ)) |
36 | 29 | oduprs 31873 |
. . . 4
β’ (π β Proset β
(ODualβπ) β
Proset ) |
37 | 27, 36 | syl 17 |
. . 3
β’ ((π β Proset β§ π β Proset ) β
(ODualβπ) β
Proset ) |
38 | 31 | oduprs 31873 |
. . . 4
β’ (π β Proset β
(ODualβπ) β
Proset ) |
39 | 26, 38 | syl 17 |
. . 3
β’ ((π β Proset β§ π β Proset ) β
(ODualβπ) β
Proset ) |
40 | 30, 32, 33, 34, 35, 37, 39 | mgcval 31896 |
. 2
β’ ((π β Proset β§ π β Proset ) β (πΊππΉ β ((πΊ:(Baseβπ)βΆ(Baseβπ) β§ πΉ:(Baseβπ)βΆ(Baseβπ)) β§ βπ¦ β (Baseβπ)βπ₯ β (Baseβπ)((πΊβπ¦)β‘(leβπ)π₯ β π¦β‘(leβπ)(πΉβπ₯))))) |
41 | 20, 28, 40 | 3bitr4d 311 |
1
β’ ((π β Proset β§ π β Proset ) β (πΉπ»πΊ β πΊππΉ)) |