Step | Hyp | Ref
| Expression |
1 | | mgcmntd.3 |
. 2
β’ (π β π β Proset ) |
2 | | mgcmntd.2 |
. 2
β’ (π β π β Proset ) |
3 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
4 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
5 | | eqid 2733 |
. . 3
β’
(leβπ) =
(leβπ) |
6 | | eqid 2733 |
. . 3
β’
(leβπ) =
(leβπ) |
7 | | mgcmntd.1 |
. . 3
β’ π» = (πMGalConnπ) |
8 | | mgcmntd.4 |
. . 3
β’ (π β πΉπ»πΊ) |
9 | 3, 4, 5, 6, 7, 2, 1, 8 | mgcf2 31898 |
. 2
β’ (π β πΊ:(Baseβπ)βΆ(Baseβπ)) |
10 | 3, 4, 5, 6, 7, 2, 1 | dfmgc2 31905 |
. . . . 5
β’ (π β (πΉπ»πΊ β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πΉβπ₯)(leβπ)(πΉβπ¦)) β§ βπ’ β (Baseβπ)βπ£ β (Baseβπ)(π’(leβπ)π£ β (πΊβπ’)(leβπ)(πΊβπ£))) β§ (βπ’ β (Baseβπ)(πΉβ(πΊβπ’))(leβπ)π’ β§ βπ₯ β (Baseβπ)π₯(leβπ)(πΊβ(πΉβπ₯))))))) |
11 | 8, 10 | mpbid 231 |
. . . 4
β’ (π β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πΉβπ₯)(leβπ)(πΉβπ¦)) β§ βπ’ β (Baseβπ)βπ£ β (Baseβπ)(π’(leβπ)π£ β (πΊβπ’)(leβπ)(πΊβπ£))) β§ (βπ’ β (Baseβπ)(πΉβ(πΊβπ’))(leβπ)π’ β§ βπ₯ β (Baseβπ)π₯(leβπ)(πΊβ(πΉβπ₯)))))) |
12 | 11 | simprld 771 |
. . 3
β’ (π β (βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πΉβπ₯)(leβπ)(πΉβπ¦)) β§ βπ’ β (Baseβπ)βπ£ β (Baseβπ)(π’(leβπ)π£ β (πΊβπ’)(leβπ)(πΊβπ£)))) |
13 | 12 | simprd 497 |
. 2
β’ (π β βπ’ β (Baseβπ)βπ£ β (Baseβπ)(π’(leβπ)π£ β (πΊβπ’)(leβπ)(πΊβπ£))) |
14 | 4, 3, 6, 5 | ismnt 31892 |
. . 3
β’ ((π β Proset β§ π β Proset ) β (πΊ β (πMonotπ) β (πΊ:(Baseβπ)βΆ(Baseβπ) β§ βπ’ β (Baseβπ)βπ£ β (Baseβπ)(π’(leβπ)π£ β (πΊβπ’)(leβπ)(πΊβπ£))))) |
15 | 14 | biimpar 479 |
. 2
β’ (((π β Proset β§ π β Proset ) β§ (πΊ:(Baseβπ)βΆ(Baseβπ) β§ βπ’ β (Baseβπ)βπ£ β (Baseβπ)(π’(leβπ)π£ β (πΊβπ’)(leβπ)(πΊβπ£)))) β πΊ β (πMonotπ)) |
16 | 1, 2, 9, 13, 15 | syl22anc 838 |
1
β’ (π β πΊ β (πMonotπ)) |