Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’ (π₯ β ran πΊ β¦ (πΉβπ₯)) = (π₯ β ran πΊ β¦ (πΉβπ₯)) |
2 | | mgcf1o.f |
. . . . . . . 8
β’ (π β πΉπ»πΊ) |
3 | | mgcf1o.a |
. . . . . . . . 9
β’ π΄ = (Baseβπ) |
4 | | mgcf1o.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ) |
5 | | mgcf1o.1 |
. . . . . . . . 9
β’ β€ =
(leβπ) |
6 | | mgcf1o.2 |
. . . . . . . . 9
β’ β² =
(leβπ) |
7 | | mgcf1o.h |
. . . . . . . . 9
β’ π» = (πMGalConnπ) |
8 | | mgcf1o.v |
. . . . . . . . . 10
β’ (π β π β Poset) |
9 | | posprs 18210 |
. . . . . . . . . 10
β’ (π β Poset β π β Proset
) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (π β π β Proset ) |
11 | | mgcf1o.w |
. . . . . . . . . 10
β’ (π β π β Poset) |
12 | | posprs 18210 |
. . . . . . . . . 10
β’ (π β Poset β π β Proset
) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
β’ (π β π β Proset ) |
14 | 3, 4, 5, 6, 7, 10,
13 | dfmgc2 31905 |
. . . . . . . 8
β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))))))) |
15 | 2, 14 | mpbid 231 |
. . . . . . 7
β’ (π β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯)))))) |
16 | 15 | simplld 767 |
. . . . . 6
β’ (π β πΉ:π΄βΆπ΅) |
17 | 16 | ffnd 6670 |
. . . . 5
β’ (π β πΉ Fn π΄) |
18 | 15 | simplrd 769 |
. . . . . . 7
β’ (π β πΊ:π΅βΆπ΄) |
19 | 18 | frnd 6677 |
. . . . . 6
β’ (π β ran πΊ β π΄) |
20 | 19 | sselda 3945 |
. . . . 5
β’ ((π β§ π₯ β ran πΊ) β π₯ β π΄) |
21 | | fnfvelrn 7032 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π₯ β π΄) β (πΉβπ₯) β ran πΉ) |
22 | 17, 20, 21 | syl2an2r 684 |
. . . 4
β’ ((π β§ π₯ β ran πΊ) β (πΉβπ₯) β ran πΉ) |
23 | 18 | ffnd 6670 |
. . . . 5
β’ (π β πΊ Fn π΅) |
24 | 16 | frnd 6677 |
. . . . . 6
β’ (π β ran πΉ β π΅) |
25 | 24 | sselda 3945 |
. . . . 5
β’ ((π β§ π’ β ran πΉ) β π’ β π΅) |
26 | | fnfvelrn 7032 |
. . . . 5
β’ ((πΊ Fn π΅ β§ π’ β π΅) β (πΊβπ’) β ran πΊ) |
27 | 23, 25, 26 | syl2an2r 684 |
. . . 4
β’ ((π β§ π’ β ran πΉ) β (πΊβπ’) β ran πΊ) |
28 | 8 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β π β Poset) |
29 | 11 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β π β Poset) |
30 | 2 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β πΉπ»πΊ) |
31 | | simplr 768 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β π¦ β π΄) |
32 | 7, 3, 4, 5, 6, 28,
29, 30, 31 | mgcf1olem1 31910 |
. . . . . . 7
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β (πΉβ(πΊβ(πΉβπ¦))) = (πΉβπ¦)) |
33 | | simpr 486 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β (πΉβπ¦) = π’) |
34 | 33 | fveq2d 6847 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β (πΊβ(πΉβπ¦)) = (πΊβπ’)) |
35 | | simpllr 775 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β π₯ = (πΊβπ’)) |
36 | 34, 35 | eqtr4d 2776 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β (πΊβ(πΉβπ¦)) = π₯) |
37 | 36 | fveq2d 6847 |
. . . . . . 7
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β (πΉβ(πΊβ(πΉβπ¦))) = (πΉβπ₯)) |
38 | 32, 37, 33 | 3eqtr3rd 2782 |
. . . . . 6
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β§ π¦ β π΄) β§ (πΉβπ¦) = π’) β π’ = (πΉβπ₯)) |
39 | 17 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β πΉ Fn π΄) |
40 | | simplrr 777 |
. . . . . . 7
β’ (((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β π’ β ran πΉ) |
41 | | fvelrnb 6904 |
. . . . . . . 8
β’ (πΉ Fn π΄ β (π’ β ran πΉ β βπ¦ β π΄ (πΉβπ¦) = π’)) |
42 | 41 | biimpa 478 |
. . . . . . 7
β’ ((πΉ Fn π΄ β§ π’ β ran πΉ) β βπ¦ β π΄ (πΉβπ¦) = π’) |
43 | 39, 40, 42 | syl2anc 585 |
. . . . . 6
β’ (((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β βπ¦ β π΄ (πΉβπ¦) = π’) |
44 | 38, 43 | r19.29a 3156 |
. . . . 5
β’ (((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π₯ = (πΊβπ’)) β π’ = (πΉβπ₯)) |
45 | 8 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β π β Poset) |
46 | 11 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β π β Poset) |
47 | 2 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β πΉπ»πΊ) |
48 | | simplr 768 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β π£ β π΅) |
49 | 7, 3, 4, 5, 6, 45,
46, 47, 48 | mgcf1olem2 31911 |
. . . . . . 7
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β (πΊβ(πΉβ(πΊβπ£))) = (πΊβπ£)) |
50 | | simpr 486 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β (πΊβπ£) = π₯) |
51 | 50 | fveq2d 6847 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β (πΉβ(πΊβπ£)) = (πΉβπ₯)) |
52 | | simpllr 775 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β π’ = (πΉβπ₯)) |
53 | 51, 52 | eqtr4d 2776 |
. . . . . . . 8
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β (πΉβ(πΊβπ£)) = π’) |
54 | 53 | fveq2d 6847 |
. . . . . . 7
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β (πΊβ(πΉβ(πΊβπ£))) = (πΊβπ’)) |
55 | 49, 54, 50 | 3eqtr3rd 2782 |
. . . . . 6
β’
(((((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β§ π£ β π΅) β§ (πΊβπ£) = π₯) β π₯ = (πΊβπ’)) |
56 | 23 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β πΊ Fn π΅) |
57 | | simplrl 776 |
. . . . . . 7
β’ (((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β π₯ β ran πΊ) |
58 | | fvelrnb 6904 |
. . . . . . . 8
β’ (πΊ Fn π΅ β (π₯ β ran πΊ β βπ£ β π΅ (πΊβπ£) = π₯)) |
59 | 58 | biimpa 478 |
. . . . . . 7
β’ ((πΊ Fn π΅ β§ π₯ β ran πΊ) β βπ£ β π΅ (πΊβπ£) = π₯) |
60 | 56, 57, 59 | syl2anc 585 |
. . . . . 6
β’ (((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β βπ£ β π΅ (πΊβπ£) = π₯) |
61 | 55, 60 | r19.29a 3156 |
. . . . 5
β’ (((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β§ π’ = (πΉβπ₯)) β π₯ = (πΊβπ’)) |
62 | 44, 61 | impbida 800 |
. . . 4
β’ ((π β§ (π₯ β ran πΊ β§ π’ β ran πΉ)) β (π₯ = (πΊβπ’) β π’ = (πΉβπ₯))) |
63 | 1, 22, 27, 62 | f1o2d 7608 |
. . 3
β’ (π β (π₯ β ran πΊ β¦ (πΉβπ₯)):ran πΊβ1-1-ontoβran
πΉ) |
64 | 16, 19 | feqresmpt 6912 |
. . . 4
β’ (π β (πΉ βΎ ran πΊ) = (π₯ β ran πΊ β¦ (πΉβπ₯))) |
65 | 64 | f1oeq1d 6780 |
. . 3
β’ (π β ((πΉ βΎ ran πΊ):ran πΊβ1-1-ontoβran
πΉ β (π₯ β ran πΊ β¦ (πΉβπ₯)):ran πΊβ1-1-ontoβran
πΉ)) |
66 | 63, 65 | mpbird 257 |
. 2
β’ (π β (πΉ βΎ ran πΊ):ran πΊβ1-1-ontoβran
πΉ) |
67 | | simplll 774 |
. . . . . . 7
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ π₯ β€ π¦) β π) |
68 | 19 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β ran πΊ β π΄) |
69 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β π₯ β ran πΊ) |
70 | 68, 69 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β π₯ β π΄) |
71 | 70 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ π₯ β€ π¦) β π₯ β π΄) |
72 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β π¦ β ran πΊ) |
73 | 68, 72 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β π¦ β π΄) |
74 | 73 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ π₯ β€ π¦) β π¦ β π΄) |
75 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ π₯ β€ π¦) β π₯ β€ π¦) |
76 | 15 | simprld 771 |
. . . . . . . . . . 11
β’ (π β (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£)))) |
77 | 76 | simpld 496 |
. . . . . . . . . 10
β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
78 | 77 | r19.21bi 3233 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
79 | 78 | r19.21bi 3233 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π¦ β π΄) β (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
80 | 79 | imp 408 |
. . . . . . 7
β’ ((((π β§ π₯ β π΄) β§ π¦ β π΄) β§ π₯ β€ π¦) β (πΉβπ₯) β² (πΉβπ¦)) |
81 | 67, 71, 74, 75, 80 | syl1111anc 839 |
. . . . . 6
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ π₯ β€ π¦) β (πΉβπ₯) β² (πΉβπ¦)) |
82 | 69 | fvresd 6863 |
. . . . . . 7
β’ (((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β ((πΉ βΎ ran πΊ)βπ₯) = (πΉβπ₯)) |
83 | 82 | adantr 482 |
. . . . . 6
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ π₯ β€ π¦) β ((πΉ βΎ ran πΊ)βπ₯) = (πΉβπ₯)) |
84 | 72 | fvresd 6863 |
. . . . . . 7
β’ (((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β ((πΉ βΎ ran πΊ)βπ¦) = (πΉβπ¦)) |
85 | 84 | adantr 482 |
. . . . . 6
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ π₯ β€ π¦) β ((πΉ βΎ ran πΊ)βπ¦) = (πΉβπ¦)) |
86 | 81, 83, 85 | 3brtr4d 5138 |
. . . . 5
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ π₯ β€ π¦) β ((πΉ βΎ ran πΊ)βπ₯) β² ((πΉ βΎ ran πΊ)βπ¦)) |
87 | 82, 84 | breq12d 5119 |
. . . . . . 7
β’ (((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β (((πΉ βΎ ran πΊ)βπ₯) β² ((πΉ βΎ ran πΊ)βπ¦) β (πΉβπ₯) β² (πΉβπ¦))) |
88 | 87 | biimpa 478 |
. . . . . 6
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ ((πΉ βΎ ran πΊ)βπ₯) β² ((πΉ βΎ ran πΊ)βπ¦)) β (πΉβπ₯) β² (πΉβπ¦)) |
89 | 11 | ad7antr 737 |
. . . . . . . . . . 11
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β π β Poset) |
90 | 8 | ad7antr 737 |
. . . . . . . . . . 11
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β π β Poset) |
91 | 7, 10, 13, 2 | mgcmnt2d 31907 |
. . . . . . . . . . . 12
β’ (π β πΊ β (πMonotπ)) |
92 | 91 | ad7antr 737 |
. . . . . . . . . . 11
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β πΊ β (πMonotπ)) |
93 | 16 | ad7antr 737 |
. . . . . . . . . . . 12
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β πΉ:π΄βΆπ΅) |
94 | 18 | ad7antr 737 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β πΊ:π΅βΆπ΄) |
95 | | simp-4r 783 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β π’ β π΅) |
96 | 94, 95 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΊβπ’) β π΄) |
97 | 93, 96 | ffvelcdmd 7037 |
. . . . . . . . . . 11
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΉβ(πΊβπ’)) β π΅) |
98 | | simplr 768 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β π£ β π΅) |
99 | 94, 98 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΊβπ£) β π΄) |
100 | 93, 99 | ffvelcdmd 7037 |
. . . . . . . . . . 11
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΉβ(πΊβπ£)) β π΅) |
101 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β (πΉβπ₯) β² (πΉβπ¦)) |
102 | 101 | ad4antr 731 |
. . . . . . . . . . . 12
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΉβπ₯) β² (πΉβπ¦)) |
103 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΊβπ’) = π₯) |
104 | 103 | fveq2d 6847 |
. . . . . . . . . . . 12
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΉβ(πΊβπ’)) = (πΉβπ₯)) |
105 | | simpr 486 |
. . . . . . . . . . . . 13
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΊβπ£) = π¦) |
106 | 105 | fveq2d 6847 |
. . . . . . . . . . . 12
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΉβ(πΊβπ£)) = (πΉβπ¦)) |
107 | 102, 104,
106 | 3brtr4d 5138 |
. . . . . . . . . . 11
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΉβ(πΊβπ’)) β² (πΉβ(πΊβπ£))) |
108 | 4, 3, 6, 5, 89, 90, 92, 97, 100, 107 | ismntd 31893 |
. . . . . . . . . 10
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΊβ(πΉβ(πΊβπ’))) β€ (πΊβ(πΉβ(πΊβπ£)))) |
109 | 2 | ad7antr 737 |
. . . . . . . . . . 11
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β πΉπ»πΊ) |
110 | 7, 3, 4, 5, 6, 90,
89, 109, 95 | mgcf1olem2 31911 |
. . . . . . . . . 10
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΊβ(πΉβ(πΊβπ’))) = (πΊβπ’)) |
111 | 7, 3, 4, 5, 6, 90,
89, 109, 98 | mgcf1olem2 31911 |
. . . . . . . . . 10
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΊβ(πΉβ(πΊβπ£))) = (πΊβπ£)) |
112 | 108, 110,
111 | 3brtr3d 5137 |
. . . . . . . . 9
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β (πΊβπ’) β€ (πΊβπ£)) |
113 | 112, 103,
105 | 3brtr3d 5137 |
. . . . . . . 8
β’
((((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β§ π£ β π΅) β§ (πΊβπ£) = π¦) β π₯ β€ π¦) |
114 | 23 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β πΊ Fn π΅) |
115 | 114 | ad2antrr 725 |
. . . . . . . . 9
β’
((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β πΊ Fn π΅) |
116 | | simp-4r 783 |
. . . . . . . . 9
β’
((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β π¦ β ran πΊ) |
117 | | fvelrnb 6904 |
. . . . . . . . . 10
β’ (πΊ Fn π΅ β (π¦ β ran πΊ β βπ£ β π΅ (πΊβπ£) = π¦)) |
118 | 117 | biimpa 478 |
. . . . . . . . 9
β’ ((πΊ Fn π΅ β§ π¦ β ran πΊ) β βπ£ β π΅ (πΊβπ£) = π¦) |
119 | 115, 116,
118 | syl2anc 585 |
. . . . . . . 8
β’
((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β βπ£ β π΅ (πΊβπ£) = π¦) |
120 | 113, 119 | r19.29a 3156 |
. . . . . . 7
β’
((((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β§ π’ β π΅) β§ (πΊβπ’) = π₯) β π₯ β€ π¦) |
121 | | simpllr 775 |
. . . . . . . 8
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β π₯ β ran πΊ) |
122 | | fvelrnb 6904 |
. . . . . . . . 9
β’ (πΊ Fn π΅ β (π₯ β ran πΊ β βπ’ β π΅ (πΊβπ’) = π₯)) |
123 | 122 | biimpa 478 |
. . . . . . . 8
β’ ((πΊ Fn π΅ β§ π₯ β ran πΊ) β βπ’ β π΅ (πΊβπ’) = π₯) |
124 | 114, 121,
123 | syl2anc 585 |
. . . . . . 7
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β βπ’ β π΅ (πΊβπ’) = π₯) |
125 | 120, 124 | r19.29a 3156 |
. . . . . 6
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ (πΉβπ₯) β² (πΉβπ¦)) β π₯ β€ π¦) |
126 | 88, 125 | syldan 592 |
. . . . 5
β’ ((((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β§ ((πΉ βΎ ran πΊ)βπ₯) β² ((πΉ βΎ ran πΊ)βπ¦)) β π₯ β€ π¦) |
127 | 86, 126 | impbida 800 |
. . . 4
β’ (((π β§ π₯ β ran πΊ) β§ π¦ β ran πΊ) β (π₯ β€ π¦ β ((πΉ βΎ ran πΊ)βπ₯) β² ((πΉ βΎ ran πΊ)βπ¦))) |
128 | 127 | anasss 468 |
. . 3
β’ ((π β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β (π₯ β€ π¦ β ((πΉ βΎ ran πΊ)βπ₯) β² ((πΉ βΎ ran πΊ)βπ¦))) |
129 | 128 | ralrimivva 3194 |
. 2
β’ (π β βπ₯ β ran πΊβπ¦ β ran πΊ(π₯ β€ π¦ β ((πΉ βΎ ran πΊ)βπ₯) β² ((πΉ βΎ ran πΊ)βπ¦))) |
130 | | df-isom 6506 |
. 2
β’ ((πΉ βΎ ran πΊ) Isom β€ , β² (ran πΊ, ran πΉ) β ((πΉ βΎ ran πΊ):ran πΊβ1-1-ontoβran
πΉ β§ βπ₯ β ran πΊβπ¦ β ran πΊ(π₯ β€ π¦ β ((πΉ βΎ ran πΊ)βπ₯) β² ((πΉ βΎ ran πΊ)βπ¦)))) |
131 | 66, 129, 130 | sylanbrc 584 |
1
β’ (π β (πΉ βΎ ran πΊ) Isom β€ , β² (ran πΊ, ran πΉ)) |