Step | Hyp | Ref
| Expression |
1 | | mgcf1o.w |
. 2
β’ (π β π β Poset) |
2 | | mgcf1o.f |
. . . . 5
β’ (π β πΉπ»πΊ) |
3 | | mgcf1o.a |
. . . . . 6
β’ π΄ = (Baseβπ) |
4 | | mgcf1o.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
5 | | mgcf1o.1 |
. . . . . 6
β’ β€ =
(leβπ) |
6 | | mgcf1o.2 |
. . . . . 6
β’ β² =
(leβπ) |
7 | | mgcf1o.h |
. . . . . 6
β’ π» = (πMGalConnπ) |
8 | | mgcf1o.v |
. . . . . . 7
β’ (π β π β Poset) |
9 | | posprs 18281 |
. . . . . . 7
β’ (π β Poset β π β Proset
) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (π β π β Proset ) |
11 | | posprs 18281 |
. . . . . . 7
β’ (π β Poset β π β Proset
) |
12 | 1, 11 | syl 17 |
. . . . . 6
β’ (π β π β Proset ) |
13 | 3, 4, 5, 6, 7, 10,
12 | dfmgc2 32671 |
. . . . 5
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))))))) |
14 | 2, 13 | mpbid 231 |
. . . 4
β’ (π β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯)))))) |
15 | 14 | simplld 765 |
. . 3
β’ (π β πΉ:π΄βΆπ΅) |
16 | 14 | simplrd 767 |
. . . 4
β’ (π β πΊ:π΅βΆπ΄) |
17 | | mgcf1olem1.1 |
. . . . 5
β’ (π β π β π΄) |
18 | 15, 17 | ffvelcdmd 7081 |
. . . 4
β’ (π β (πΉβπ) β π΅) |
19 | 16, 18 | ffvelcdmd 7081 |
. . 3
β’ (π β (πΊβ(πΉβπ)) β π΄) |
20 | 15, 19 | ffvelcdmd 7081 |
. 2
β’ (π β (πΉβ(πΊβ(πΉβπ))) β π΅) |
21 | 3, 4, 5, 6, 7, 10,
12, 2, 18 | mgccole2 32666 |
. 2
β’ (π β (πΉβ(πΊβ(πΉβπ))) β² (πΉβπ)) |
22 | 3, 4, 5, 6, 7, 10,
12, 2, 17 | mgccole1 32665 |
. . 3
β’ (π β π β€ (πΊβ(πΉβπ))) |
23 | 3, 4, 5, 6, 7, 10,
12, 2, 17, 19, 22 | mgcmnt1 32667 |
. 2
β’ (π β (πΉβπ) β² (πΉβ(πΊβ(πΉβπ)))) |
24 | 4, 6 | posasymb 18284 |
. . 3
β’ ((π β Poset β§ (πΉβ(πΊβ(πΉβπ))) β π΅ β§ (πΉβπ) β π΅) β (((πΉβ(πΊβ(πΉβπ))) β² (πΉβπ) β§ (πΉβπ) β² (πΉβ(πΊβ(πΉβπ)))) β (πΉβ(πΊβ(πΉβπ))) = (πΉβπ))) |
25 | 24 | biimpa 476 |
. 2
β’ (((π β Poset β§ (πΉβ(πΊβ(πΉβπ))) β π΅ β§ (πΉβπ) β π΅) β§ ((πΉβ(πΊβ(πΉβπ))) β² (πΉβπ) β§ (πΉβπ) β² (πΉβ(πΊβ(πΉβπ))))) β (πΉβ(πΊβ(πΉβπ))) = (πΉβπ)) |
26 | 1, 20, 18, 21, 23, 25 | syl32anc 1375 |
1
β’ (π β (πΉβ(πΊβ(πΉβπ))) = (πΉβπ)) |