Step | Hyp | Ref
| Expression |
1 | | mgcval.2 |
. . 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.3 |
. . . . . . 7
β’ (π β π β Proset ) |
9 | 3, 4, 5, 6, 7, 1, 8 | mgcval 31896 |
. . . . . 6
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))))) |
10 | 2, 9 | mpbid 231 |
. . . . 5
β’ (π β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
11 | 10 | simplrd 769 |
. . . 4
β’ (π β πΊ:π΅βΆπ΄) |
12 | | mgccole2.1 |
. . . 4
β’ (π β π β π΅) |
13 | 11, 12 | ffvelcdmd 7037 |
. . 3
β’ (π β (πΊβπ) β π΄) |
14 | 3, 5 | prsref 18193 |
. . 3
β’ ((π β Proset β§ (πΊβπ) β π΄) β (πΊβπ) β€ (πΊβπ)) |
15 | 1, 13, 14 | syl2anc 585 |
. 2
β’ (π β (πΊβπ) β€ (πΊβπ)) |
16 | 10 | simprd 497 |
. . . 4
β’ (π β βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))) |
17 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = (πΊβπ) β (πΉβπ₯) = (πΉβ(πΊβπ))) |
18 | 17 | breq1d 5116 |
. . . . . . . 8
β’ (π₯ = (πΊβπ) β ((πΉβπ₯) β² π¦ β (πΉβ(πΊβπ)) β² π¦)) |
19 | | breq1 5109 |
. . . . . . . 8
β’ (π₯ = (πΊβπ) β (π₯ β€ (πΊβπ¦) β (πΊβπ) β€ (πΊβπ¦))) |
20 | 18, 19 | bibi12d 346 |
. . . . . . 7
β’ (π₯ = (πΊβπ) β (((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β ((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦)))) |
21 | 20 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ = (πΊβπ)) β (((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β ((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦)))) |
22 | 21 | ralbidv 3171 |
. . . . 5
β’ ((π β§ π₯ = (πΊβπ)) β (βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β βπ¦ β π΅ ((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦)))) |
23 | 13, 22 | rspcdv 3572 |
. . . 4
β’ (π β (βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β βπ¦ β π΅ ((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦)))) |
24 | 16, 23 | mpd 15 |
. . 3
β’ (π β βπ¦ β π΅ ((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦))) |
25 | | simpr 486 |
. . . . . 6
β’ ((π β§ π¦ = π) β π¦ = π) |
26 | 25 | breq2d 5118 |
. . . . 5
β’ ((π β§ π¦ = π) β ((πΉβ(πΊβπ)) β² π¦ β (πΉβ(πΊβπ)) β² π)) |
27 | | fveq2 6843 |
. . . . . . 7
β’ (π¦ = π β (πΊβπ¦) = (πΊβπ)) |
28 | 27 | adantl 483 |
. . . . . 6
β’ ((π β§ π¦ = π) β (πΊβπ¦) = (πΊβπ)) |
29 | 28 | breq2d 5118 |
. . . . 5
β’ ((π β§ π¦ = π) β ((πΊβπ) β€ (πΊβπ¦) β (πΊβπ) β€ (πΊβπ))) |
30 | 26, 29 | bibi12d 346 |
. . . 4
β’ ((π β§ π¦ = π) β (((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦)) β ((πΉβ(πΊβπ)) β² π β (πΊβπ) β€ (πΊβπ)))) |
31 | 12, 30 | rspcdv 3572 |
. . 3
β’ (π β (βπ¦ β π΅ ((πΉβ(πΊβπ)) β² π¦ β (πΊβπ) β€ (πΊβπ¦)) β ((πΉβ(πΊβπ)) β² π β (πΊβπ) β€ (πΊβπ)))) |
32 | 24, 31 | mpd 15 |
. 2
β’ (π β ((πΉβ(πΊβπ)) β² π β (πΊβπ) β€ (πΊβπ))) |
33 | 15, 32 | mpbird 257 |
1
β’ (π β (πΉβ(πΊβπ)) β² π) |