Step | Hyp | Ref
| Expression |
1 | | dfmgc2lem.1 |
. . 3
β’ (π β πΉ:π΄βΆπ΅) |
2 | | dfmgc2lem.2 |
. . 3
β’ (π β πΊ:π΅βΆπ΄) |
3 | 1, 2 | jca 513 |
. 2
β’ (π β (πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄)) |
4 | | mgcval.2 |
. . . . . . 7
β’ (π β π β Proset ) |
5 | 4 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β π β Proset ) |
6 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β π§ β π΄) |
7 | 6 | adantr 482 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β π§ β π΄) |
8 | 2 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β πΊ:π΅βΆπ΄) |
9 | 1 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β πΉ:π΄βΆπ΅) |
10 | 9, 7 | ffvelcdmd 7037 |
. . . . . . 7
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β (πΉβπ§) β π΅) |
11 | 8, 10 | ffvelcdmd 7037 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β (πΊβ(πΉβπ§)) β π΄) |
12 | 2 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β πΊ:π΅βΆπ΄) |
13 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β π€ β π΅) |
14 | 12, 13 | ffvelcdmd 7037 |
. . . . . . 7
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β (πΊβπ€) β π΄) |
15 | 14 | adantr 482 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β (πΊβπ€) β π΄) |
16 | | dfmgc2lem.5 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β π₯ β€ (πΊβ(πΉβπ₯))) |
17 | 16 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) |
18 | 17 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))) |
19 | | simpr 486 |
. . . . . . . . 9
β’
(((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β§ π₯ = π§) β π₯ = π§) |
20 | 19 | fveq2d 6847 |
. . . . . . . . . 10
β’
(((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β§ π₯ = π§) β (πΉβπ₯) = (πΉβπ§)) |
21 | 20 | fveq2d 6847 |
. . . . . . . . 9
β’
(((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β§ π₯ = π§) β (πΊβ(πΉβπ₯)) = (πΊβ(πΉβπ§))) |
22 | 19, 21 | breq12d 5119 |
. . . . . . . 8
β’
(((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β§ π₯ = π§) β (π₯ β€ (πΊβ(πΉβπ₯)) β π§ β€ (πΊβ(πΉβπ§)))) |
23 | 7, 22 | rspcdv 3572 |
. . . . . . 7
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β (βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯)) β π§ β€ (πΊβ(πΉβπ§)))) |
24 | 18, 23 | mpd 15 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β π§ β€ (πΊβ(πΉβπ§))) |
25 | | dfmgc2lem.4 |
. . . . . . . . 9
β’ (π β βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) |
26 | 25 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) |
27 | | breq1 5109 |
. . . . . . . . . 10
β’ (π’ = (πΉβπ§) β (π’ β² π£ β (πΉβπ§) β² π£)) |
28 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π’ = (πΉβπ§) β (πΊβπ’) = (πΊβ(πΉβπ§))) |
29 | 28 | breq1d 5116 |
. . . . . . . . . 10
β’ (π’ = (πΉβπ§) β ((πΊβπ’) β€ (πΊβπ£) β (πΊβ(πΉβπ§)) β€ (πΊβπ£))) |
30 | 27, 29 | imbi12d 345 |
. . . . . . . . 9
β’ (π’ = (πΉβπ§) β ((π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)) β ((πΉβπ§) β² π£ β (πΊβ(πΉβπ§)) β€ (πΊβπ£)))) |
31 | | breq2 5110 |
. . . . . . . . . 10
β’ (π£ = π€ β ((πΉβπ§) β² π£ β (πΉβπ§) β² π€)) |
32 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π£ = π€ β (πΊβπ£) = (πΊβπ€)) |
33 | 32 | breq2d 5118 |
. . . . . . . . . 10
β’ (π£ = π€ β ((πΊβ(πΉβπ§)) β€ (πΊβπ£) β (πΊβ(πΉβπ§)) β€ (πΊβπ€))) |
34 | 31, 33 | imbi12d 345 |
. . . . . . . . 9
β’ (π£ = π€ β (((πΉβπ§) β² π£ β (πΊβ(πΉβπ§)) β€ (πΊβπ£)) β ((πΉβπ§) β² π€ β (πΊβ(πΉβπ§)) β€ (πΊβπ€)))) |
35 | 1 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β (πΉβπ§) β π΅) |
36 | 35 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β (πΉβπ§) β π΅) |
37 | | eqidd 2734 |
. . . . . . . . 9
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π’ = (πΉβπ§)) β π΅ = π΅) |
38 | 30, 34, 36, 37, 13 | rspc2vd 3907 |
. . . . . . . 8
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β (βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)) β ((πΉβπ§) β² π€ β (πΊβ(πΉβπ§)) β€ (πΊβπ€)))) |
39 | 26, 38 | mpd 15 |
. . . . . . 7
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β ((πΉβπ§) β² π€ β (πΊβ(πΉβπ§)) β€ (πΊβπ€))) |
40 | 39 | imp 408 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β (πΊβ(πΉβπ§)) β€ (πΊβπ€)) |
41 | | mgcoval.1 |
. . . . . . 7
β’ π΄ = (Baseβπ) |
42 | | mgcoval.3 |
. . . . . . 7
β’ β€ =
(leβπ) |
43 | 41, 42 | prstr 18194 |
. . . . . 6
β’ ((π β Proset β§ (π§ β π΄ β§ (πΊβ(πΉβπ§)) β π΄ β§ (πΊβπ€) β π΄) β§ (π§ β€ (πΊβ(πΉβπ§)) β§ (πΊβ(πΉβπ§)) β€ (πΊβπ€))) β π§ β€ (πΊβπ€)) |
44 | 5, 7, 11, 15, 24, 40, 43 | syl132anc 1389 |
. . . . 5
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ (πΉβπ§) β² π€) β π§ β€ (πΊβπ€)) |
45 | | mgcval.3 |
. . . . . . 7
β’ (π β π β Proset ) |
46 | 45 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β π β Proset ) |
47 | 35 | ad2antrr 725 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β (πΉβπ§) β π΅) |
48 | 1 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β πΉ:π΄βΆπ΅) |
49 | 14 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β (πΊβπ€) β π΄) |
50 | 48, 49 | ffvelcdmd 7037 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β (πΉβ(πΊβπ€)) β π΅) |
51 | | simplr 768 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β π€ β π΅) |
52 | | dfmgc2lem.3 |
. . . . . . . . 9
β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
53 | 52 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
54 | | breq1 5109 |
. . . . . . . . . 10
β’ (π₯ = π§ β (π₯ β€ π¦ β π§ β€ π¦)) |
55 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
56 | 55 | breq1d 5116 |
. . . . . . . . . 10
β’ (π₯ = π§ β ((πΉβπ₯) β² (πΉβπ¦) β (πΉβπ§) β² (πΉβπ¦))) |
57 | 54, 56 | imbi12d 345 |
. . . . . . . . 9
β’ (π₯ = π§ β ((π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β (π§ β€ π¦ β (πΉβπ§) β² (πΉβπ¦)))) |
58 | | breq2 5110 |
. . . . . . . . . 10
β’ (π¦ = (πΊβπ€) β (π§ β€ π¦ β π§ β€ (πΊβπ€))) |
59 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π¦ = (πΊβπ€) β (πΉβπ¦) = (πΉβ(πΊβπ€))) |
60 | 59 | breq2d 5118 |
. . . . . . . . . 10
β’ (π¦ = (πΊβπ€) β ((πΉβπ§) β² (πΉβπ¦) β (πΉβπ§) β² (πΉβ(πΊβπ€)))) |
61 | 58, 60 | imbi12d 345 |
. . . . . . . . 9
β’ (π¦ = (πΊβπ€) β ((π§ β€ π¦ β (πΉβπ§) β² (πΉβπ¦)) β (π§ β€ (πΊβπ€) β (πΉβπ§) β² (πΉβ(πΊβπ€))))) |
62 | | eqidd 2734 |
. . . . . . . . 9
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π₯ = π§) β π΄ = π΄) |
63 | 57, 61, 6, 62, 14 | rspc2vd 3907 |
. . . . . . . 8
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β (π§ β€ (πΊβπ€) β (πΉβπ§) β² (πΉβ(πΊβπ€))))) |
64 | 53, 63 | mpd 15 |
. . . . . . 7
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β (π§ β€ (πΊβπ€) β (πΉβπ§) β² (πΉβ(πΊβπ€)))) |
65 | 64 | imp 408 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β (πΉβπ§) β² (πΉβ(πΊβπ€))) |
66 | | dfmgc2lem.6 |
. . . . . . . . 9
β’ ((π β§ π’ β π΅) β (πΉβ(πΊβπ’)) β² π’) |
67 | 66 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) |
68 | 67 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’) |
69 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β§ π’ = π€) β π’ = π€) |
70 | 69 | fveq2d 6847 |
. . . . . . . . . 10
β’
(((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β§ π’ = π€) β (πΊβπ’) = (πΊβπ€)) |
71 | 70 | fveq2d 6847 |
. . . . . . . . 9
β’
(((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β§ π’ = π€) β (πΉβ(πΊβπ’)) = (πΉβ(πΊβπ€))) |
72 | 71, 69 | breq12d 5119 |
. . . . . . . 8
β’
(((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β§ π’ = π€) β ((πΉβ(πΊβπ’)) β² π’ β (πΉβ(πΊβπ€)) β² π€)) |
73 | 51, 72 | rspcdv 3572 |
. . . . . . 7
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β (πΉβ(πΊβπ€)) β² π€)) |
74 | 68, 73 | mpd 15 |
. . . . . 6
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β (πΉβ(πΊβπ€)) β² π€) |
75 | | mgcoval.2 |
. . . . . . 7
β’ π΅ = (Baseβπ) |
76 | | mgcoval.4 |
. . . . . . 7
β’ β² =
(leβπ) |
77 | 75, 76 | prstr 18194 |
. . . . . 6
β’ ((π β Proset β§ ((πΉβπ§) β π΅ β§ (πΉβ(πΊβπ€)) β π΅ β§ π€ β π΅) β§ ((πΉβπ§) β² (πΉβ(πΊβπ€)) β§ (πΉβ(πΊβπ€)) β² π€)) β (πΉβπ§) β² π€) |
78 | 46, 47, 50, 51, 65, 74, 77 | syl132anc 1389 |
. . . . 5
β’ ((((π β§ π§ β π΄) β§ π€ β π΅) β§ π§ β€ (πΊβπ€)) β (πΉβπ§) β² π€) |
79 | 44, 78 | impbida 800 |
. . . 4
β’ (((π β§ π§ β π΄) β§ π€ β π΅) β ((πΉβπ§) β² π€ β π§ β€ (πΊβπ€))) |
80 | 79 | anasss 468 |
. . 3
β’ ((π β§ (π§ β π΄ β§ π€ β π΅)) β ((πΉβπ§) β² π€ β π§ β€ (πΊβπ€))) |
81 | 80 | ralrimivva 3194 |
. 2
β’ (π β βπ§ β π΄ βπ€ β π΅ ((πΉβπ§) β² π€ β π§ β€ (πΊβπ€))) |
82 | | mgcval.1 |
. . 3
β’ π» = (πMGalConnπ) |
83 | 41, 75, 42, 76, 82, 4, 45 | mgcval 31896 |
. 2
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ§ β π΄ βπ€ β π΅ ((πΉβπ§) β² π€ β π§ β€ (πΊβπ€))))) |
84 | 3, 81, 83 | mpbir2and 712 |
1
β’ (π β πΉπ»πΊ) |