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 | | mgccole1.2 |
. . . 4
β’ (π β π β π΄) |
13 | 11, 12 | ffvelcdmd 7037 |
. . 3
β’ (π β (πΉβπ) β π΅) |
14 | 4, 6 | prsref 18193 |
. . 3
β’ ((π β Proset β§ (πΉβπ) β π΅) β (πΉβπ) β² (πΉβπ)) |
15 | 1, 13, 14 | syl2anc 585 |
. 2
β’ (π β (πΉβπ) β² (πΉβπ)) |
16 | | fveq2 6843 |
. . . . . . 7
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
17 | 16 | breq1d 5116 |
. . . . . 6
β’ (π₯ = π β ((πΉβπ₯) β² π¦ β (πΉβπ) β² π¦)) |
18 | | breq1 5109 |
. . . . . 6
β’ (π₯ = π β (π₯ β€ (πΊβπ¦) β π β€ (πΊβπ¦))) |
19 | 17, 18 | bibi12d 346 |
. . . . 5
β’ (π₯ = π β (((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β ((πΉβπ) β² π¦ β π β€ (πΊβπ¦)))) |
20 | 19 | ralbidv 3171 |
. . . 4
β’ (π₯ = π β (βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β βπ¦ β π΅ ((πΉβπ) β² π¦ β π β€ (πΊβπ¦)))) |
21 | 10 | simprd 497 |
. . . 4
β’ (π β βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))) |
22 | 20, 21, 12 | rspcdva 3581 |
. . 3
β’ (π β βπ¦ β π΅ ((πΉβπ) β² π¦ β π β€ (πΊβπ¦))) |
23 | | simpr 486 |
. . . . . 6
β’ ((π β§ π¦ = (πΉβπ)) β π¦ = (πΉβπ)) |
24 | 23 | breq2d 5118 |
. . . . 5
β’ ((π β§ π¦ = (πΉβπ)) β ((πΉβπ) β² π¦ β (πΉβπ) β² (πΉβπ))) |
25 | 23 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π¦ = (πΉβπ)) β (πΊβπ¦) = (πΊβ(πΉβπ))) |
26 | 25 | breq2d 5118 |
. . . . 5
β’ ((π β§ π¦ = (πΉβπ)) β (π β€ (πΊβπ¦) β π β€ (πΊβ(πΉβπ)))) |
27 | 24, 26 | bibi12d 346 |
. . . 4
β’ ((π β§ π¦ = (πΉβπ)) β (((πΉβπ) β² π¦ β π β€ (πΊβπ¦)) β ((πΉβπ) β² (πΉβπ) β π β€ (πΊβ(πΉβπ))))) |
28 | 13, 27 | rspcdv 3572 |
. . 3
β’ (π β (βπ¦ β π΅ ((πΉβπ) β² π¦ β π β€ (πΊβπ¦)) β ((πΉβπ) β² (πΉβπ) β π β€ (πΊβ(πΉβπ))))) |
29 | 22, 28 | mpd 15 |
. 2
β’ (π β ((πΉβπ) β² (πΉβπ) β π β€ (πΊβ(πΉβπ)))) |
30 | 15, 29 | mpbid 231 |
1
β’ (π β π β€ (πΊβ(πΉβπ))) |