Step | Hyp | Ref
| Expression |
1 | | mgcval.3 |
. . 3
β’ (π β π β Proset ) |
2 | | mgccole.1 |
. . . . . 6
β’ (π β πΉπ»πΊ) |
3 | | mgcoval.1 |
. . . . . . 7
β’ π΄ = (Baseβπ) |
4 | | mgcoval.2 |
. . . . . . 7
β’ π΅ = (Baseβπ) |
5 | | mgcoval.3 |
. . . . . . 7
β’ β€ =
(leβπ) |
6 | | mgcoval.4 |
. . . . . . 7
β’ β² =
(leβπ) |
7 | | mgcval.1 |
. . . . . . 7
β’ π» = (πMGalConnπ) |
8 | | mgcval.2 |
. . . . . . 7
β’ (π β π β Proset ) |
9 | 3, 4, 5, 6, 7, 8, 1 | mgcval 31896 |
. . . . . 6
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))))) |
10 | 2, 9 | mpbid 231 |
. . . . 5
β’ (π β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
11 | 10 | simplld 767 |
. . . 4
β’ (π β πΉ:π΄βΆπ΅) |
12 | 10 | simplrd 769 |
. . . . 5
β’ (π β πΊ:π΅βΆπ΄) |
13 | | mgcmnt2.1 |
. . . . 5
β’ (π β π β π΅) |
14 | 12, 13 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πΊβπ) β π΄) |
15 | 11, 14 | ffvelcdmd 7037 |
. . 3
β’ (π β (πΉβ(πΊβπ)) β π΅) |
16 | | mgcmnt2.2 |
. . 3
β’ (π β π β π΅) |
17 | 3, 4, 5, 6, 7, 8, 1, 2, 13 | mgccole2 31900 |
. . 3
β’ (π β (πΉβ(πΊβπ)) β² π) |
18 | | mgcmnt2.3 |
. . 3
β’ (π β π β² π) |
19 | 4, 6 | prstr 18194 |
. . 3
β’ ((π β Proset β§ ((πΉβ(πΊβπ)) β π΅ β§ π β π΅ β§ π β π΅) β§ ((πΉβ(πΊβπ)) β² π β§ π β² π)) β (πΉβ(πΊβπ)) β² π) |
20 | 1, 15, 13, 16, 17, 18, 19 | syl132anc 1389 |
. 2
β’ (π β (πΉβ(πΊβπ)) β² π) |
21 | | breq2 5110 |
. . . 4
β’ (π¦ = π β ((πΉβ(πΊβπ)) β² π¦ β (πΉβ(πΊβπ)) β² π)) |
22 | | fveq2 6843 |
. . . . 5
β’ (π¦ = π β (πΊβπ¦) = (πΊβπ)) |
23 | 22 | breq2d 5118 |
. . . 4
β’ (π¦ = π β ((πΊβπ) β€ (πΊβπ¦) β (πΊβπ) β€ (πΊβπ))) |
24 | 21, 23 | bibi12d 346 |
. . 3
β’ (π¦ = π β (((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦)) β ((πΉβ(πΊβπ)) β² π β (πΊβπ) β€ (πΊβπ)))) |
25 | | fveq2 6843 |
. . . . . . 7
β’ (π₯ = (πΊβπ) β (πΉβπ₯) = (πΉβ(πΊβπ))) |
26 | 25 | breq1d 5116 |
. . . . . 6
β’ (π₯ = (πΊβπ) β ((πΉβπ₯) β² π¦ β (πΉβ(πΊβπ)) β² π¦)) |
27 | | breq1 5109 |
. . . . . 6
β’ (π₯ = (πΊβπ) β (π₯ β€ (πΊβπ¦) β (πΊβπ) β€ (πΊβπ¦))) |
28 | 26, 27 | bibi12d 346 |
. . . . 5
β’ (π₯ = (πΊβπ) β (((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β ((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦)))) |
29 | 28 | ralbidv 3171 |
. . . 4
β’ (π₯ = (πΊβπ) β (βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β βπ¦ β π΅ ((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦)))) |
30 | 10 | simprd 497 |
. . . 4
β’ (π β βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))) |
31 | 29, 30, 14 | rspcdva 3581 |
. . 3
β’ (π β βπ¦ β π΅ ((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦))) |
32 | 24, 31, 16 | rspcdva 3581 |
. 2
β’ (π β ((πΉβ(πΊβπ)) β² π β (πΊβπ) β€ (πΊβπ))) |
33 | 20, 32 | mpbid 231 |
1
β’ (π β (πΊβπ) β€ (πΊβπ)) |