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 32151 |
. . . . 5
β’ ((π β Proset β§ π β Proset ) β (πMGalConnπ) = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |
9 | 2, 3, 8 | syl2anc 584 |
. . . 4
β’ (π β (πMGalConnπ) = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |
10 | 1, 9 | eqtrid 2784 |
. . 3
β’ (π β π» = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |
11 | 10 | breqd 5159 |
. 2
β’ (π β (πΉπ»πΊ β πΉ{β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}πΊ)) |
12 | | fveq1 6890 |
. . . . . . . 8
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
13 | 12 | adantr 481 |
. . . . . . 7
β’ ((π = πΉ β§ π = πΊ) β (πβπ₯) = (πΉβπ₯)) |
14 | 13 | breq1d 5158 |
. . . . . 6
β’ ((π = πΉ β§ π = πΊ) β ((πβπ₯) β² π¦ β (πΉβπ₯) β² π¦)) |
15 | | fveq1 6890 |
. . . . . . . 8
β’ (π = πΊ β (πβπ¦) = (πΊβπ¦)) |
16 | 15 | adantl 482 |
. . . . . . 7
β’ ((π = πΉ β§ π = πΊ) β (πβπ¦) = (πΊβπ¦)) |
17 | 16 | breq2d 5160 |
. . . . . 6
β’ ((π = πΉ β§ π = πΊ) β (π₯ β€ (πβπ¦) β π₯ β€ (πΊβπ¦))) |
18 | 14, 17 | bibi12d 345 |
. . . . 5
β’ ((π = πΉ β§ π = πΊ) β (((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)) β ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
19 | 18 | 2ralbidv 3218 |
. . . 4
β’ ((π = πΉ β§ π = πΊ) β (βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)) β βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
20 | | eqid 2732 |
. . . 4
β’
{β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))} = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))} |
21 | 19, 20 | brab2a 5769 |
. . 3
β’ (πΉ{β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}πΊ β ((πΉ β (π΅ βm π΄) β§ πΊ β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
22 | 5 | fvexi 6905 |
. . . . . 6
β’ π΅ β V |
23 | 4 | fvexi 6905 |
. . . . . 6
β’ π΄ β V |
24 | 22, 23 | elmap 8864 |
. . . . 5
β’ (πΉ β (π΅ βm π΄) β πΉ:π΄βΆπ΅) |
25 | 23, 22 | elmap 8864 |
. . . . 5
β’ (πΊ β (π΄ βm π΅) β πΊ:π΅βΆπ΄) |
26 | 24, 25 | anbi12i 627 |
. . . 4
β’ ((πΉ β (π΅ βm π΄) β§ πΊ β (π΄ βm π΅)) β (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) |
27 | 26 | anbi1i 624 |
. . 3
β’ (((πΉ β (π΅ βm π΄) β§ πΊ β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))) β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦)))) |
28 | 21, 27 | bitr2i 275 |
. 2
β’ (((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))) β πΉ{β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}πΊ) |
29 | 11, 28 | bitr4di 288 |
1
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))))) |