Step | Hyp | Ref
| Expression |
1 | | mgcval.2 |
. . 3
β’ (π β π β Proset ) |
2 | | mgcmnt1.1 |
. . 3
β’ (π β π β π΄) |
3 | | mgcmnt1.2 |
. . 3
β’ (π β π β π΄) |
4 | | mgccole.1 |
. . . . . 6
β’ (π β πΉπ»πΊ) |
5 | | mgcoval.1 |
. . . . . . 7
β’ π΄ = (Baseβπ) |
6 | | mgcoval.2 |
. . . . . . 7
β’ π΅ = (Baseβπ) |
7 | | mgcoval.3 |
. . . . . . 7
β’ β€ =
(leβπ) |
8 | | mgcoval.4 |
. . . . . . 7
β’ β² =
(leβπ) |
9 | | mgcval.1 |
. . . . . . 7
β’ π» = (πMGalConnπ) |
10 | | mgcval.3 |
. . . . . . 7
β’ (π β π β Proset ) |
11 | 5, 6, 7, 8, 9, 1, 10 | mgcval 31896 |
. . . . . 6
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))))) |
12 | 4, 11 | mpbid 231 |
. . . . 5
β’ (π β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
13 | 12 | simplrd 769 |
. . . 4
β’ (π β πΊ:π΅βΆπ΄) |
14 | 12 | simplld 767 |
. . . . 5
β’ (π β πΉ:π΄βΆπ΅) |
15 | 14, 3 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πΉβπ) β π΅) |
16 | 13, 15 | ffvelcdmd 7037 |
. . 3
β’ (π β (πΊβ(πΉβπ)) β π΄) |
17 | | mgcmnt1.3 |
. . 3
β’ (π β π β€ π) |
18 | 5, 6, 7, 8, 9, 1, 10, 4, 3 | mgccole1 31899 |
. . 3
β’ (π β π β€ (πΊβ(πΉβπ))) |
19 | 5, 7 | prstr 18194 |
. . 3
β’ ((π β Proset β§ (π β π΄ β§ π β π΄ β§ (πΊβ(πΉβπ)) β π΄) β§ (π β€ π β§ π β€ (πΊβ(πΉβπ)))) β π β€ (πΊβ(πΉβπ))) |
20 | 1, 2, 3, 16, 17, 18, 19 | syl132anc 1389 |
. 2
β’ (π β π β€ (πΊβ(πΉβπ))) |
21 | 12 | simprd 497 |
. . . 4
β’ (π β βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))) |
22 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
23 | 22 | breq1d 5116 |
. . . . . . . 8
β’ (π₯ = π β ((πΉβπ₯) β² π¦ β (πΉβπ) β² π¦)) |
24 | | breq1 5109 |
. . . . . . . 8
β’ (π₯ = π β (π₯ β€ (πΊβπ¦) β π β€ (πΊβπ¦))) |
25 | 23, 24 | bibi12d 346 |
. . . . . . 7
β’ (π₯ = π β (((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β ((πΉβπ) β² π¦ β π β€ (πΊβπ¦)))) |
26 | 25 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ = π) β (((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β ((πΉβπ) β² π¦ β π β€ (πΊβπ¦)))) |
27 | 26 | ralbidv 3171 |
. . . . 5
β’ ((π β§ π₯ = π) β (βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β βπ¦ β π΅ ((πΉβπ) β² π¦ β π β€ (πΊβπ¦)))) |
28 | 2, 27 | rspcdv 3572 |
. . . 4
β’ (π β (βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)) β βπ¦ β π΅ ((πΉβπ) β² π¦ β π β€ (πΊβπ¦)))) |
29 | 21, 28 | mpd 15 |
. . 3
β’ (π β βπ¦ β π΅ ((πΉβπ) β² π¦ β π β€ (πΊβπ¦))) |
30 | | simpr 486 |
. . . . . 6
β’ ((π β§ π¦ = (πΉβπ)) β π¦ = (πΉβπ)) |
31 | 30 | breq2d 5118 |
. . . . 5
β’ ((π β§ π¦ = (πΉβπ)) β ((πΉβπ) β² π¦ β (πΉβπ) β² (πΉβπ))) |
32 | 30 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π¦ = (πΉβπ)) β (πΊβπ¦) = (πΊβ(πΉβπ))) |
33 | 32 | breq2d 5118 |
. . . . 5
β’ ((π β§ π¦ = (πΉβπ)) β (π β€ (πΊβπ¦) β π β€ (πΊβ(πΉβπ)))) |
34 | 31, 33 | bibi12d 346 |
. . . 4
β’ ((π β§ π¦ = (πΉβπ)) β (((πΉβπ) β² π¦ β π β€ (πΊβπ¦)) β ((πΉβπ) β² (πΉβπ) β π β€ (πΊβ(πΉβπ))))) |
35 | 15, 34 | rspcdv 3572 |
. . 3
β’ (π β (βπ¦ β π΅ ((πΉβπ) β² π¦ β π β€ (πΊβπ¦)) β ((πΉβπ) β² (πΉβπ) β π β€ (πΊβ(πΉβπ))))) |
36 | 29, 35 | mpd 15 |
. 2
β’ (π β ((πΉβπ) β² (πΉβπ) β π β€ (πΊβ(πΉβπ)))) |
37 | 20, 36 | mpbird 257 |
1
β’ (π β (πΉβπ) β² (πΉβπ)) |