Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mgcf1o Structured version   Visualization version   GIF version

Theorem mgcf1o 31912
Description: Given a Galois connection, exhibit an order isomorphism. (Contributed by Thierry Arnoux, 26-Jul-2024.)
Hypotheses
Ref Expression
mgcf1o.h 𝐻 = (𝑉MGalConnπ‘Š)
mgcf1o.a 𝐴 = (Baseβ€˜π‘‰)
mgcf1o.b 𝐡 = (Baseβ€˜π‘Š)
mgcf1o.1 ≀ = (leβ€˜π‘‰)
mgcf1o.2 ≲ = (leβ€˜π‘Š)
mgcf1o.v (πœ‘ β†’ 𝑉 ∈ Poset)
mgcf1o.w (πœ‘ β†’ π‘Š ∈ Poset)
mgcf1o.f (πœ‘ β†’ 𝐹𝐻𝐺)
Assertion
Ref Expression
mgcf1o (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺) Isom ≀ , ≲ (ran 𝐺, ran 𝐹))

Proof of Theorem mgcf1o
Dummy variables 𝑒 𝑣 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef 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 )
108, 9syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝑉 ∈ Proset )
11 mgcf1o.w . . . . . . . . . 10 (πœ‘ β†’ π‘Š ∈ Poset)
12 posprs 18210 . . . . . . . . . 10 (π‘Š ∈ Poset β†’ π‘Š ∈ Proset )
1311, 12syl 17 . . . . . . . . 9 (πœ‘ β†’ π‘Š ∈ Proset )
143, 4, 5, 6, 7, 10, 13dfmgc2 31905 . . . . . . . 8 (πœ‘ β†’ (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴) ∧ ((βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))) ∧ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)))))))
152, 14mpbid 231 . . . . . . 7 (πœ‘ β†’ ((𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴) ∧ ((βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))) ∧ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))))))
1615simplld 767 . . . . . 6 (πœ‘ β†’ 𝐹:𝐴⟢𝐡)
1716ffnd 6670 . . . . 5 (πœ‘ β†’ 𝐹 Fn 𝐴)
1815simplrd 769 . . . . . . 7 (πœ‘ β†’ 𝐺:𝐡⟢𝐴)
1918frnd 6677 . . . . . 6 (πœ‘ β†’ ran 𝐺 βŠ† 𝐴)
2019sselda 3945 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ ran 𝐺) β†’ π‘₯ ∈ 𝐴)
21 fnfvelrn 7032 . . . . 5 ((𝐹 Fn 𝐴 ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) ∈ ran 𝐹)
2217, 20, 21syl2an2r 684 . . . 4 ((πœ‘ ∧ π‘₯ ∈ ran 𝐺) β†’ (πΉβ€˜π‘₯) ∈ ran 𝐹)
2318ffnd 6670 . . . . 5 (πœ‘ β†’ 𝐺 Fn 𝐡)
2416frnd 6677 . . . . . 6 (πœ‘ β†’ ran 𝐹 βŠ† 𝐡)
2524sselda 3945 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ 𝑒 ∈ 𝐡)
26 fnfvelrn 7032 . . . . 5 ((𝐺 Fn 𝐡 ∧ 𝑒 ∈ 𝐡) β†’ (πΊβ€˜π‘’) ∈ ran 𝐺)
2723, 25, 26syl2an2r 684 . . . 4 ((πœ‘ ∧ 𝑒 ∈ ran 𝐹) β†’ (πΊβ€˜π‘’) ∈ ran 𝐺)
288ad4antr 731 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ 𝑉 ∈ Poset)
2911ad4antr 731 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ π‘Š ∈ Poset)
302ad4antr 731 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ 𝐹𝐻𝐺)
31 simplr 768 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ 𝑦 ∈ 𝐴)
327, 3, 4, 5, 6, 28, 29, 30, 31mgcf1olem1 31910 . . . . . . 7 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ (πΉβ€˜(πΊβ€˜(πΉβ€˜π‘¦))) = (πΉβ€˜π‘¦))
33 simpr 486 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ (πΉβ€˜π‘¦) = 𝑒)
3433fveq2d 6847 . . . . . . . . 9 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ (πΊβ€˜(πΉβ€˜π‘¦)) = (πΊβ€˜π‘’))
35 simpllr 775 . . . . . . . . 9 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ π‘₯ = (πΊβ€˜π‘’))
3634, 35eqtr4d 2776 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ (πΊβ€˜(πΉβ€˜π‘¦)) = π‘₯)
3736fveq2d 6847 . . . . . . 7 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ (πΉβ€˜(πΊβ€˜(πΉβ€˜π‘¦))) = (πΉβ€˜π‘₯))
3832, 37, 333eqtr3rd 2782 . . . . . 6 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) ∧ 𝑦 ∈ 𝐴) ∧ (πΉβ€˜π‘¦) = 𝑒) β†’ 𝑒 = (πΉβ€˜π‘₯))
3917ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) β†’ 𝐹 Fn 𝐴)
40 simplrr 777 . . . . . . 7 (((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) β†’ 𝑒 ∈ ran 𝐹)
41 fvelrnb 6904 . . . . . . . 8 (𝐹 Fn 𝐴 β†’ (𝑒 ∈ ran 𝐹 ↔ βˆƒπ‘¦ ∈ 𝐴 (πΉβ€˜π‘¦) = 𝑒))
4241biimpa 478 . . . . . . 7 ((𝐹 Fn 𝐴 ∧ 𝑒 ∈ ran 𝐹) β†’ βˆƒπ‘¦ ∈ 𝐴 (πΉβ€˜π‘¦) = 𝑒)
4339, 40, 42syl2anc 585 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) β†’ βˆƒπ‘¦ ∈ 𝐴 (πΉβ€˜π‘¦) = 𝑒)
4438, 43r19.29a 3156 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ π‘₯ = (πΊβ€˜π‘’)) β†’ 𝑒 = (πΉβ€˜π‘₯))
458ad4antr 731 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ 𝑉 ∈ Poset)
4611ad4antr 731 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ π‘Š ∈ Poset)
472ad4antr 731 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ 𝐹𝐻𝐺)
48 simplr 768 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ 𝑣 ∈ 𝐡)
497, 3, 4, 5, 6, 45, 46, 47, 48mgcf1olem2 31911 . . . . . . 7 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ (πΊβ€˜(πΉβ€˜(πΊβ€˜π‘£))) = (πΊβ€˜π‘£))
50 simpr 486 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ (πΊβ€˜π‘£) = π‘₯)
5150fveq2d 6847 . . . . . . . . 9 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ (πΉβ€˜(πΊβ€˜π‘£)) = (πΉβ€˜π‘₯))
52 simpllr 775 . . . . . . . . 9 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ 𝑒 = (πΉβ€˜π‘₯))
5351, 52eqtr4d 2776 . . . . . . . 8 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ (πΉβ€˜(πΊβ€˜π‘£)) = 𝑒)
5453fveq2d 6847 . . . . . . 7 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ (πΊβ€˜(πΉβ€˜(πΊβ€˜π‘£))) = (πΊβ€˜π‘’))
5549, 54, 503eqtr3rd 2782 . . . . . 6 (((((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = π‘₯) β†’ π‘₯ = (πΊβ€˜π‘’))
5623ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) β†’ 𝐺 Fn 𝐡)
57 simplrl 776 . . . . . . 7 (((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) β†’ π‘₯ ∈ ran 𝐺)
58 fvelrnb 6904 . . . . . . . 8 (𝐺 Fn 𝐡 β†’ (π‘₯ ∈ ran 𝐺 ↔ βˆƒπ‘£ ∈ 𝐡 (πΊβ€˜π‘£) = π‘₯))
5958biimpa 478 . . . . . . 7 ((𝐺 Fn 𝐡 ∧ π‘₯ ∈ ran 𝐺) β†’ βˆƒπ‘£ ∈ 𝐡 (πΊβ€˜π‘£) = π‘₯)
6056, 57, 59syl2anc 585 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) β†’ βˆƒπ‘£ ∈ 𝐡 (πΊβ€˜π‘£) = π‘₯)
6155, 60r19.29a 3156 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) ∧ 𝑒 = (πΉβ€˜π‘₯)) β†’ π‘₯ = (πΊβ€˜π‘’))
6244, 61impbida 800 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑒 ∈ ran 𝐹)) β†’ (π‘₯ = (πΊβ€˜π‘’) ↔ 𝑒 = (πΉβ€˜π‘₯)))
631, 22, 27, 62f1o2d 7608 . . 3 (πœ‘ β†’ (π‘₯ ∈ ran 𝐺 ↦ (πΉβ€˜π‘₯)):ran 𝐺–1-1-ontoβ†’ran 𝐹)
6416, 19feqresmpt 6912 . . . 4 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺) = (π‘₯ ∈ ran 𝐺 ↦ (πΉβ€˜π‘₯)))
6564f1oeq1d 6780 . . 3 (πœ‘ β†’ ((𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹 ↔ (π‘₯ ∈ ran 𝐺 ↦ (πΉβ€˜π‘₯)):ran 𝐺–1-1-ontoβ†’ran 𝐹))
6663, 65mpbird 257 . 2 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺):ran 𝐺–1-1-ontoβ†’ran 𝐹)
67 simplll 774 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ π‘₯ ≀ 𝑦) β†’ πœ‘)
6819ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) β†’ ran 𝐺 βŠ† 𝐴)
69 simplr 768 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) β†’ π‘₯ ∈ ran 𝐺)
7068, 69sseldd 3946 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) β†’ π‘₯ ∈ 𝐴)
7170adantr 482 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ π‘₯ ≀ 𝑦) β†’ π‘₯ ∈ 𝐴)
72 simpr 486 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) β†’ 𝑦 ∈ ran 𝐺)
7368, 72sseldd 3946 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) β†’ 𝑦 ∈ 𝐴)
7473adantr 482 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ π‘₯ ≀ 𝑦) β†’ 𝑦 ∈ 𝐴)
75 simpr 486 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ π‘₯ ≀ 𝑦) β†’ π‘₯ ≀ 𝑦)
7615simprld 771 . . . . . . . . . . 11 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))))
7776simpld 496 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)))
7877r19.21bi 3233 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)))
7978r19.21bi 3233 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)))
8079imp 408 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ π‘₯ ≀ 𝑦) β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦))
8167, 71, 74, 75, 80syl1111anc 839 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ π‘₯ ≀ 𝑦) β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦))
8269fvresd 6863 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘₯) = (πΉβ€˜π‘₯))
8382adantr 482 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ π‘₯ ≀ 𝑦) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘₯) = (πΉβ€˜π‘₯))
8472fvresd 6863 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘¦) = (πΉβ€˜π‘¦))
8584adantr 482 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ π‘₯ ≀ 𝑦) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘¦) = (πΉβ€˜π‘¦))
8681, 83, 853brtr4d 5138 . . . . 5 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ π‘₯ ≀ 𝑦) β†’ ((𝐹 β†Ύ ran 𝐺)β€˜π‘₯) ≲ ((𝐹 β†Ύ ran 𝐺)β€˜π‘¦))
8782, 84breq12d 5119 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) β†’ (((𝐹 β†Ύ ran 𝐺)β€˜π‘₯) ≲ ((𝐹 β†Ύ ran 𝐺)β€˜π‘¦) ↔ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)))
8887biimpa 478 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘₯) ≲ ((𝐹 β†Ύ ran 𝐺)β€˜π‘¦)) β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦))
8911ad7antr 737 . . . . . . . . . . 11 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ π‘Š ∈ Poset)
908ad7antr 737 . . . . . . . . . . 11 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ 𝑉 ∈ Poset)
917, 10, 13, 2mgcmnt2d 31907 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐺 ∈ (π‘ŠMonot𝑉))
9291ad7antr 737 . . . . . . . . . . 11 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ 𝐺 ∈ (π‘ŠMonot𝑉))
9316ad7antr 737 . . . . . . . . . . . 12 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ 𝐹:𝐴⟢𝐡)
9418ad7antr 737 . . . . . . . . . . . . 13 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ 𝐺:𝐡⟢𝐴)
95 simp-4r 783 . . . . . . . . . . . . 13 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ 𝑒 ∈ 𝐡)
9694, 95ffvelcdmd 7037 . . . . . . . . . . . 12 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΊβ€˜π‘’) ∈ 𝐴)
9793, 96ffvelcdmd 7037 . . . . . . . . . . 11 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΉβ€˜(πΊβ€˜π‘’)) ∈ 𝐡)
98 simplr 768 . . . . . . . . . . . . 13 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ 𝑣 ∈ 𝐡)
9994, 98ffvelcdmd 7037 . . . . . . . . . . . 12 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΊβ€˜π‘£) ∈ 𝐴)
10093, 99ffvelcdmd 7037 . . . . . . . . . . 11 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΉβ€˜(πΊβ€˜π‘£)) ∈ 𝐡)
101 simpr 486 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦))
102101ad4antr 731 . . . . . . . . . . . 12 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦))
103 simpllr 775 . . . . . . . . . . . . 13 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΊβ€˜π‘’) = π‘₯)
104103fveq2d 6847 . . . . . . . . . . . 12 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΉβ€˜(πΊβ€˜π‘’)) = (πΉβ€˜π‘₯))
105 simpr 486 . . . . . . . . . . . . 13 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΊβ€˜π‘£) = 𝑦)
106105fveq2d 6847 . . . . . . . . . . . 12 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΉβ€˜(πΊβ€˜π‘£)) = (πΉβ€˜π‘¦))
107102, 104, 1063brtr4d 5138 . . . . . . . . . . 11 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΉβ€˜(πΊβ€˜π‘’)) ≲ (πΉβ€˜(πΊβ€˜π‘£)))
1084, 3, 6, 5, 89, 90, 92, 97, 100, 107ismntd 31893 . . . . . . . . . 10 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΊβ€˜(πΉβ€˜(πΊβ€˜π‘’))) ≀ (πΊβ€˜(πΉβ€˜(πΊβ€˜π‘£))))
1092ad7antr 737 . . . . . . . . . . 11 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ 𝐹𝐻𝐺)
1107, 3, 4, 5, 6, 90, 89, 109, 95mgcf1olem2 31911 . . . . . . . . . 10 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΊβ€˜(πΉβ€˜(πΊβ€˜π‘’))) = (πΊβ€˜π‘’))
1117, 3, 4, 5, 6, 90, 89, 109, 98mgcf1olem2 31911 . . . . . . . . . 10 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΊβ€˜(πΉβ€˜(πΊβ€˜π‘£))) = (πΊβ€˜π‘£))
112108, 110, 1113brtr3d 5137 . . . . . . . . 9 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))
113112, 103, 1053brtr3d 5137 . . . . . . . 8 ((((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) ∧ 𝑣 ∈ 𝐡) ∧ (πΊβ€˜π‘£) = 𝑦) β†’ π‘₯ ≀ 𝑦)
11423ad3antrrr 729 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) β†’ 𝐺 Fn 𝐡)
115114ad2antrr 725 . . . . . . . . 9 ((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) β†’ 𝐺 Fn 𝐡)
116 simp-4r 783 . . . . . . . . 9 ((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) β†’ 𝑦 ∈ ran 𝐺)
117 fvelrnb 6904 . . . . . . . . . 10 (𝐺 Fn 𝐡 β†’ (𝑦 ∈ ran 𝐺 ↔ βˆƒπ‘£ ∈ 𝐡 (πΊβ€˜π‘£) = 𝑦))
118117biimpa 478 . . . . . . . . 9 ((𝐺 Fn 𝐡 ∧ 𝑦 ∈ ran 𝐺) β†’ βˆƒπ‘£ ∈ 𝐡 (πΊβ€˜π‘£) = 𝑦)
119115, 116, 118syl2anc 585 . . . . . . . 8 ((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) β†’ βˆƒπ‘£ ∈ 𝐡 (πΊβ€˜π‘£) = 𝑦)
120113, 119r19.29a 3156 . . . . . . 7 ((((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ 𝑒 ∈ 𝐡) ∧ (πΊβ€˜π‘’) = π‘₯) β†’ π‘₯ ≀ 𝑦)
121 simpllr 775 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) β†’ π‘₯ ∈ ran 𝐺)
122 fvelrnb 6904 . . . . . . . . 9 (𝐺 Fn 𝐡 β†’ (π‘₯ ∈ ran 𝐺 ↔ βˆƒπ‘’ ∈ 𝐡 (πΊβ€˜π‘’) = π‘₯))
123122biimpa 478 . . . . . . . 8 ((𝐺 Fn 𝐡 ∧ π‘₯ ∈ ran 𝐺) β†’ βˆƒπ‘’ ∈ 𝐡 (πΊβ€˜π‘’) = π‘₯)
124114, 121, 123syl2anc 585 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) β†’ βˆƒπ‘’ ∈ 𝐡 (πΊβ€˜π‘’) = π‘₯)
125120, 124r19.29a 3156 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) β†’ π‘₯ ≀ 𝑦)
12688, 125syldan 592 . . . . 5 ((((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) ∧ ((𝐹 β†Ύ ran 𝐺)β€˜π‘₯) ≲ ((𝐹 β†Ύ ran 𝐺)β€˜π‘¦)) β†’ π‘₯ ≀ 𝑦)
12786, 126impbida 800 . . . 4 (((πœ‘ ∧ π‘₯ ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐺) β†’ (π‘₯ ≀ 𝑦 ↔ ((𝐹 β†Ύ ran 𝐺)β€˜π‘₯) ≲ ((𝐹 β†Ύ ran 𝐺)β€˜π‘¦)))
128127anasss 468 . . 3 ((πœ‘ ∧ (π‘₯ ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺)) β†’ (π‘₯ ≀ 𝑦 ↔ ((𝐹 β†Ύ ran 𝐺)β€˜π‘₯) ≲ ((𝐹 β†Ύ ran 𝐺)β€˜π‘¦)))
129128ralrimivva 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 𝐺)β€˜π‘¦))))
13166, 129, 130sylanbrc 584 1 (πœ‘ β†’ (𝐹 β†Ύ ran 𝐺) Isom ≀ , ≲ (ran 𝐺, ran 𝐹))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  βˆƒwrex 3070   βŠ† wss 3911   class class class wbr 5106   ↦ cmpt 5189  ran crn 5635   β†Ύ cres 5636   Fn wfn 6492  βŸΆwf 6493  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497   Isom wiso 6498  (class class class)co 7358  Basecbs 17088  lecple 17145   Proset cproset 18187  Posetcpo 18201  Monotcmnt 31887  MGalConncmgc 31888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8770  df-proset 18189  df-poset 18207  df-mnt 31889  df-mgc 31890
This theorem is referenced by:  nsgqusf1o  32242
  Copyright terms: Public domain W3C validator