Step | Hyp | Ref
| Expression |
1 | | mgcval.1 |
. . . 4
β’ π» = (πMGalConnπ) |
2 | | mgcval.2 |
. . . . 5
β’ (π β π β Proset ) |
3 | | mgcval.3 |
. . . . 5
β’ (π β π β Proset ) |
4 | | mgcoval.1 |
. . . . . 6
β’ π΄ = (Baseβπ) |
5 | | mgcoval.2 |
. . . . . 6
β’ π΅ = (Baseβπ) |
6 | | mgcoval.3 |
. . . . . 6
β’ β€ =
(leβπ) |
7 | | mgcoval.4 |
. . . . . 6
β’ β² =
(leβπ) |
8 | 4, 5, 6, 7 | mgcoval 31895 |
. . . . 5
β’ ((π β Proset β§ π β Proset ) β (πMGalConnπ) = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |
9 | 2, 3, 8 | syl2anc 585 |
. . . 4
β’ (π β (πMGalConnπ) = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |
10 | 1, 9 | eqtrid 2785 |
. . 3
β’ (π β π» = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |
11 | 10 | breqd 5117 |
. 2
β’ (π β (πΉπ»πΊ β πΉ{β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}πΊ)) |
12 | | fveq1 6842 |
. . . . . . . 8
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ ((π = πΉ β§ π = πΊ) β (πβπ₯) = (πΉβπ₯)) |
14 | 13 | breq1d 5116 |
. . . . . 6
β’ ((π = πΉ β§ π = πΊ) β ((πβπ₯) β² π¦ β (πΉβπ₯) β² π¦)) |
15 | | fveq1 6842 |
. . . . . . . 8
β’ (π = πΊ β (πβπ¦) = (πΊβπ¦)) |
16 | 15 | adantl 483 |
. . . . . . 7
β’ ((π = πΉ β§ π = πΊ) β (πβπ¦) = (πΊβπ¦)) |
17 | 16 | breq2d 5118 |
. . . . . 6
β’ ((π = πΉ β§ π = πΊ) β (π₯ β€ (πβπ¦) β π₯ β€ (πΊβπ¦))) |
18 | 14, 17 | bibi12d 346 |
. . . . 5
β’ ((π = πΉ β§ π = πΊ) β (((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)) β ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
19 | 18 | 2ralbidv 3209 |
. . . 4
β’ ((π = πΉ β§ π = πΊ) β (βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)) β βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
20 | | eqid 2733 |
. . . 4
β’
{β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))} = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))} |
21 | 19, 20 | brab2a 5726 |
. . 3
β’ (πΉ{β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}πΊ β ((πΉ β (π΅ βm π΄) β§ πΊ β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
22 | 5 | fvexi 6857 |
. . . . . 6
β’ π΅ β V |
23 | 4 | fvexi 6857 |
. . . . . 6
β’ π΄ β V |
24 | 22, 23 | elmap 8812 |
. . . . 5
β’ (πΉ β (π΅ βm π΄) β πΉ:π΄βΆπ΅) |
25 | 23, 22 | elmap 8812 |
. . . . 5
β’ (πΊ β (π΄ βm π΅) β πΊ:π΅βΆπ΄) |
26 | 24, 25 | anbi12i 628 |
. . . 4
β’ ((πΉ β (π΅ βm π΄) β§ πΊ β (π΄ βm π΅)) β (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) |
27 | 26 | anbi1i 625 |
. . 3
β’ (((πΉ β (π΅ βm π΄) β§ πΊ β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))) β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
28 | 21, 27 | bitr2i 276 |
. 2
β’ (((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))) β πΉ{β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}πΊ) |
29 | 11, 28 | bitr4di 289 |
1
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))))) |