Step | Hyp | Ref
| Expression |
1 | | mgcmntco.3 |
. . . . 5
β’ (π β π β Proset ) |
2 | 1 | ad2antrr 725 |
. . . 4
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β π β Proset ) |
3 | | mgcval.2 |
. . . . . . 7
β’ (π β π β Proset ) |
4 | | mgcmntco.4 |
. . . . . . 7
β’ (π β πΎ β (πMonotπ)) |
5 | | mgcoval.1 |
. . . . . . . 8
β’ π΄ = (Baseβπ) |
6 | | mgcmntco.1 |
. . . . . . . 8
β’ πΆ = (Baseβπ) |
7 | 5, 6 | mntf 31894 |
. . . . . . 7
β’ ((π β Proset β§ π β Proset β§ πΎ β (πMonotπ)) β πΎ:π΄βΆπΆ) |
8 | 3, 1, 4, 7 | syl3anc 1372 |
. . . . . 6
β’ (π β πΎ:π΄βΆπΆ) |
9 | 8 | ad2antrr 725 |
. . . . 5
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β πΎ:π΄βΆπΆ) |
10 | | mgcoval.2 |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
11 | | mgcoval.3 |
. . . . . . . 8
β’ β€ =
(leβπ) |
12 | | mgcoval.4 |
. . . . . . . 8
β’ β² =
(leβπ) |
13 | | mgcval.1 |
. . . . . . . 8
β’ π» = (πMGalConnπ) |
14 | | mgcval.3 |
. . . . . . . 8
β’ (π β π β Proset ) |
15 | | mgccole.1 |
. . . . . . . 8
β’ (π β πΉπ»πΊ) |
16 | 5, 10, 11, 12, 13, 3, 14, 15 | mgcf2 31898 |
. . . . . . 7
β’ (π β πΊ:π΅βΆπ΄) |
17 | 16 | adantr 482 |
. . . . . 6
β’ ((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β πΊ:π΅βΆπ΄) |
18 | 17 | ffvelcdmda 7036 |
. . . . 5
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β (πΊβπ¦) β π΄) |
19 | 9, 18 | ffvelcdmd 7037 |
. . . 4
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β (πΎβ(πΊβπ¦)) β πΆ) |
20 | | mgcmntco.5 |
. . . . . . 7
β’ (π β πΏ β (πMonotπ)) |
21 | 10, 6 | mntf 31894 |
. . . . . . 7
β’ ((π β Proset β§ π β Proset β§ πΏ β (πMonotπ)) β πΏ:π΅βΆπΆ) |
22 | 14, 1, 20, 21 | syl3anc 1372 |
. . . . . 6
β’ (π β πΏ:π΅βΆπΆ) |
23 | 22 | ad2antrr 725 |
. . . . 5
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β πΏ:π΅βΆπΆ) |
24 | 5, 10, 11, 12, 13, 3, 14, 15 | mgcf1 31897 |
. . . . . . 7
β’ (π β πΉ:π΄βΆπ΅) |
25 | 24 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β πΉ:π΄βΆπ΅) |
26 | 25, 18 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β (πΉβ(πΊβπ¦)) β π΅) |
27 | 23, 26 | ffvelcdmd 7037 |
. . . 4
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β (πΏβ(πΉβ(πΊβπ¦))) β πΆ) |
28 | 22 | adantr 482 |
. . . . 5
β’ ((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β πΏ:π΅βΆπΆ) |
29 | 28 | ffvelcdmda 7036 |
. . . 4
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β (πΏβπ¦) β πΆ) |
30 | 16 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π¦ β π΅) β (πΊβπ¦) β π΄) |
31 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = (πΊβπ¦) β (πΎβπ₯) = (πΎβ(πΊβπ¦))) |
32 | | 2fveq3 6848 |
. . . . . . . . 9
β’ (π₯ = (πΊβπ¦) β (πΏβ(πΉβπ₯)) = (πΏβ(πΉβ(πΊβπ¦)))) |
33 | 31, 32 | breq12d 5119 |
. . . . . . . 8
β’ (π₯ = (πΊβπ¦) β ((πΎβπ₯) < (πΏβ(πΉβπ₯)) β (πΎβ(πΊβπ¦)) < (πΏβ(πΉβ(πΊβπ¦))))) |
34 | 33 | adantl 483 |
. . . . . . 7
β’ (((π β§ π¦ β π΅) β§ π₯ = (πΊβπ¦)) β ((πΎβπ₯) < (πΏβ(πΉβπ₯)) β (πΎβ(πΊβπ¦)) < (πΏβ(πΉβ(πΊβπ¦))))) |
35 | 30, 34 | rspcdv 3572 |
. . . . . 6
β’ ((π β§ π¦ β π΅) β (βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯)) β (πΎβ(πΊβπ¦)) < (πΏβ(πΉβ(πΊβπ¦))))) |
36 | 35 | imp 408 |
. . . . 5
β’ (((π β§ π¦ β π΅) β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β (πΎβ(πΊβπ¦)) < (πΏβ(πΉβ(πΊβπ¦)))) |
37 | 36 | an32s 651 |
. . . 4
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β (πΎβ(πΊβπ¦)) < (πΏβ(πΉβ(πΊβπ¦)))) |
38 | | mgcmntco.2 |
. . . . 5
β’ < =
(leβπ) |
39 | 14 | ad2antrr 725 |
. . . . 5
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β π β Proset ) |
40 | 20 | ad2antrr 725 |
. . . . 5
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β πΏ β (πMonotπ)) |
41 | | simpr 486 |
. . . . 5
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β π¦ β π΅) |
42 | 3 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β π β Proset ) |
43 | 15 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β πΉπ»πΊ) |
44 | 5, 10, 11, 12, 13, 42, 39, 43, 41 | mgccole2 31900 |
. . . . 5
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β (πΉβ(πΊβπ¦)) β² π¦) |
45 | 10, 6, 12, 38, 39, 2, 40, 26, 41, 44 | ismntd 31893 |
. . . 4
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β (πΏβ(πΉβ(πΊβπ¦))) < (πΏβπ¦)) |
46 | 6, 38 | prstr 18194 |
. . . 4
β’ ((π β Proset β§ ((πΎβ(πΊβπ¦)) β πΆ β§ (πΏβ(πΉβ(πΊβπ¦))) β πΆ β§ (πΏβπ¦) β πΆ) β§ ((πΎβ(πΊβπ¦)) < (πΏβ(πΉβ(πΊβπ¦))) β§ (πΏβ(πΉβ(πΊβπ¦))) < (πΏβπ¦))) β (πΎβ(πΊβπ¦)) < (πΏβπ¦)) |
47 | 2, 19, 27, 29, 37, 45, 46 | syl132anc 1389 |
. . 3
β’ (((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β§ π¦ β π΅) β (πΎβ(πΊβπ¦)) < (πΏβπ¦)) |
48 | 47 | ralrimiva 3140 |
. 2
β’ ((π β§ βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) β βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) |
49 | 1 | ad2antrr 725 |
. . . 4
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β π β Proset ) |
50 | 8 | ad2antrr 725 |
. . . . 5
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β πΎ:π΄βΆπΆ) |
51 | | simpr 486 |
. . . . 5
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β π₯ β π΄) |
52 | 50, 51 | ffvelcdmd 7037 |
. . . 4
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β (πΎβπ₯) β πΆ) |
53 | 16 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β πΊ:π΅βΆπ΄) |
54 | 24 | adantr 482 |
. . . . . . 7
β’ ((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β πΉ:π΄βΆπ΅) |
55 | 54 | ffvelcdmda 7036 |
. . . . . 6
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β (πΉβπ₯) β π΅) |
56 | 53, 55 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β (πΊβ(πΉβπ₯)) β π΄) |
57 | 50, 56 | ffvelcdmd 7037 |
. . . 4
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β (πΎβ(πΊβ(πΉβπ₯))) β πΆ) |
58 | 22 | ad2antrr 725 |
. . . . 5
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β πΏ:π΅βΆπΆ) |
59 | 58, 55 | ffvelcdmd 7037 |
. . . 4
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β (πΏβ(πΉβπ₯)) β πΆ) |
60 | 3 | ad2antrr 725 |
. . . . 5
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β π β Proset ) |
61 | 4 | ad2antrr 725 |
. . . . 5
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β πΎ β (πMonotπ)) |
62 | 14 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β π β Proset ) |
63 | 15 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β πΉπ»πΊ) |
64 | 5, 10, 11, 12, 13, 60, 62, 63, 51 | mgccole1 31899 |
. . . . 5
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β π₯ β€ (πΊβ(πΉβπ₯))) |
65 | 5, 6, 11, 38, 60, 49, 61, 51, 56, 64 | ismntd 31893 |
. . . 4
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β (πΎβπ₯) < (πΎβ(πΊβ(πΉβπ₯)))) |
66 | 24 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β π΅) |
67 | | 2fveq3 6848 |
. . . . . . . . 9
β’ (π¦ = (πΉβπ₯) β (πΎβ(πΊβπ¦)) = (πΎβ(πΊβ(πΉβπ₯)))) |
68 | | fveq2 6843 |
. . . . . . . . 9
β’ (π¦ = (πΉβπ₯) β (πΏβπ¦) = (πΏβ(πΉβπ₯))) |
69 | 67, 68 | breq12d 5119 |
. . . . . . . 8
β’ (π¦ = (πΉβπ₯) β ((πΎβ(πΊβπ¦)) < (πΏβπ¦) β (πΎβ(πΊβ(πΉβπ₯))) < (πΏβ(πΉβπ₯)))) |
70 | 69 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π¦ = (πΉβπ₯)) β ((πΎβ(πΊβπ¦)) < (πΏβπ¦) β (πΎβ(πΊβ(πΉβπ₯))) < (πΏβ(πΉβπ₯)))) |
71 | 66, 70 | rspcdv 3572 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦) β (πΎβ(πΊβ(πΉβπ₯))) < (πΏβ(πΉβπ₯)))) |
72 | 71 | imp 408 |
. . . . 5
β’ (((π β§ π₯ β π΄) β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β (πΎβ(πΊβ(πΉβπ₯))) < (πΏβ(πΉβπ₯))) |
73 | 72 | an32s 651 |
. . . 4
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β (πΎβ(πΊβ(πΉβπ₯))) < (πΏβ(πΉβπ₯))) |
74 | 6, 38 | prstr 18194 |
. . . 4
β’ ((π β Proset β§ ((πΎβπ₯) β πΆ β§ (πΎβ(πΊβ(πΉβπ₯))) β πΆ β§ (πΏβ(πΉβπ₯)) β πΆ) β§ ((πΎβπ₯) < (πΎβ(πΊβ(πΉβπ₯))) β§ (πΎβ(πΊβ(πΉβπ₯))) < (πΏβ(πΉβπ₯)))) β (πΎβπ₯) < (πΏβ(πΉβπ₯))) |
75 | 49, 52, 57, 59, 65, 73, 74 | syl132anc 1389 |
. . 3
β’ (((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β§ π₯ β π΄) β (πΎβπ₯) < (πΏβ(πΉβπ₯))) |
76 | 75 | ralrimiva 3140 |
. 2
β’ ((π β§ βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦)) β βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯))) |
77 | 48, 76 | impbida 800 |
1
β’ (π β (βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯)) β βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦))) |