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

Theorem dfmgc2 31905
Description: Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.)
Hypotheses
Ref Expression
mgcoval.1 𝐴 = (Baseβ€˜π‘‰)
mgcoval.2 𝐡 = (Baseβ€˜π‘Š)
mgcoval.3 ≀ = (leβ€˜π‘‰)
mgcoval.4 ≲ = (leβ€˜π‘Š)
mgcval.1 𝐻 = (𝑉MGalConnπ‘Š)
mgcval.2 (πœ‘ β†’ 𝑉 ∈ Proset )
mgcval.3 (πœ‘ β†’ π‘Š ∈ Proset )
Assertion
Ref Expression
dfmgc2 (πœ‘ β†’ (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴) ∧ ((βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))) ∧ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)))))))
Distinct variable groups:   𝑣, ≀   𝑣, ≲   𝑣,𝐴,π‘₯,𝑦   𝑣,𝐡,π‘₯,𝑦   𝑣,𝑉,π‘₯,𝑦   𝑣,π‘Š,π‘₯,𝑦   π‘₯,𝐹,𝑦   π‘₯,𝐺,𝑦   𝑒, ≀ ,𝑣   π‘₯, ≀ ,𝑦   𝑒, ≲   π‘₯, ≲ ,𝑦   𝑒,𝐡   𝑒,𝐹,𝑣   𝑒,𝐺,𝑣   𝑒,𝐻,𝑣   π‘₯,𝐻,𝑦   πœ‘,𝑒,𝑣   πœ‘,π‘₯,𝑦
Allowed substitution hints:   𝐴(𝑒)   𝑉(𝑒)   π‘Š(𝑒)

Proof of Theorem dfmgc2
Dummy variables 𝑖 𝑗 π‘š 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mgcoval.1 . . . . 5 𝐴 = (Baseβ€˜π‘‰)
2 mgcoval.2 . . . . 5 𝐡 = (Baseβ€˜π‘Š)
3 mgcoval.3 . . . . 5 ≀ = (leβ€˜π‘‰)
4 mgcoval.4 . . . . 5 ≲ = (leβ€˜π‘Š)
5 mgcval.1 . . . . 5 𝐻 = (𝑉MGalConnπ‘Š)
6 mgcval.2 . . . . 5 (πœ‘ β†’ 𝑉 ∈ Proset )
7 mgcval.3 . . . . 5 (πœ‘ β†’ π‘Š ∈ Proset )
81, 2, 3, 4, 5, 6, 7mgcval 31896 . . . 4 (πœ‘ β†’ (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴) ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘₯) ≲ 𝑦 ↔ π‘₯ ≀ (πΊβ€˜π‘¦)))))
98simprbda 500 . . 3 ((πœ‘ ∧ 𝐹𝐻𝐺) β†’ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴))
106ad4antr 731 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ π‘₯ ≀ 𝑦) β†’ 𝑉 ∈ Proset )
117ad4antr 731 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ π‘₯ ≀ 𝑦) β†’ π‘Š ∈ Proset )
12 simp-4r 783 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ π‘₯ ≀ 𝑦) β†’ 𝐹𝐻𝐺)
13 simpllr 775 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ π‘₯ ≀ 𝑦) β†’ π‘₯ ∈ 𝐴)
14 simplr 768 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ π‘₯ ≀ 𝑦) β†’ 𝑦 ∈ 𝐴)
15 simpr 486 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ π‘₯ ≀ 𝑦) β†’ π‘₯ ≀ 𝑦)
161, 2, 3, 4, 5, 10, 11, 12, 13, 14, 15mgcmnt1 31901 . . . . . . . 8 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ π‘₯ ≀ 𝑦) β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦))
1716ex 414 . . . . . . 7 ((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) β†’ (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)))
1817anasss 468 . . . . . 6 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)))
1918ralrimivva 3194 . . . . 5 ((πœ‘ ∧ 𝐹𝐻𝐺) β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)))
206ad4antr 731 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ≲ 𝑣) β†’ 𝑉 ∈ Proset )
217ad4antr 731 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ≲ 𝑣) β†’ π‘Š ∈ Proset )
22 simp-4r 783 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ≲ 𝑣) β†’ 𝐹𝐻𝐺)
23 simpllr 775 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ≲ 𝑣) β†’ 𝑒 ∈ 𝐡)
24 simplr 768 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ≲ 𝑣) β†’ 𝑣 ∈ 𝐡)
25 simpr 486 . . . . . . . . 9 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ≲ 𝑣) β†’ 𝑒 ≲ 𝑣)
261, 2, 3, 4, 5, 20, 21, 22, 23, 24, 25mgcmnt2 31902 . . . . . . . 8 (((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ≲ 𝑣) β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))
2726ex 414 . . . . . . 7 ((((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) ∧ 𝑣 ∈ 𝐡) β†’ (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))
2827anasss 468 . . . . . 6 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ (𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡)) β†’ (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))
2928ralrimivva 3194 . . . . 5 ((πœ‘ ∧ 𝐹𝐻𝐺) β†’ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))
3019, 29jca 513 . . . 4 ((πœ‘ ∧ 𝐹𝐻𝐺) β†’ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))))
316ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) β†’ 𝑉 ∈ Proset )
327ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) β†’ π‘Š ∈ Proset )
33 simplr 768 . . . . . . 7 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) β†’ 𝐹𝐻𝐺)
34 simpr 486 . . . . . . 7 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) β†’ 𝑒 ∈ 𝐡)
351, 2, 3, 4, 5, 31, 32, 33, 34mgccole2 31900 . . . . . 6 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ 𝑒 ∈ 𝐡) β†’ (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒)
3635ralrimiva 3140 . . . . 5 ((πœ‘ ∧ 𝐹𝐻𝐺) β†’ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒)
376ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) β†’ 𝑉 ∈ Proset )
387ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) β†’ π‘Š ∈ Proset )
39 simplr 768 . . . . . . 7 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) β†’ 𝐹𝐻𝐺)
40 simpr 486 . . . . . . 7 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝐴)
411, 2, 3, 4, 5, 37, 38, 39, 40mgccole1 31899 . . . . . 6 (((πœ‘ ∧ 𝐹𝐻𝐺) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)))
4241ralrimiva 3140 . . . . 5 ((πœ‘ ∧ 𝐹𝐻𝐺) β†’ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)))
4336, 42jca 513 . . . 4 ((πœ‘ ∧ 𝐹𝐻𝐺) β†’ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))))
4430, 43jca 513 . . 3 ((πœ‘ ∧ 𝐹𝐻𝐺) β†’ ((βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))) ∧ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)))))
459, 44jca 513 . 2 ((πœ‘ ∧ 𝐹𝐻𝐺) β†’ ((𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴) ∧ ((βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))) ∧ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))))))
466ad4antr 731 . . . . . 6 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ 𝑉 ∈ Proset )
477ad4antr 731 . . . . . 6 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ π‘Š ∈ Proset )
48 simp-4r 783 . . . . . . 7 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴))
4948simpld 496 . . . . . 6 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ 𝐹:𝐴⟢𝐡)
5048simprd 497 . . . . . 6 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ 𝐺:𝐡⟢𝐴)
51 simpllr 775 . . . . . . . 8 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))))
5251simpld 496 . . . . . . 7 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)))
53 breq1 5109 . . . . . . . . 9 (π‘₯ = π‘š β†’ (π‘₯ ≀ 𝑦 ↔ π‘š ≀ 𝑦))
54 fveq2 6843 . . . . . . . . . 10 (π‘₯ = π‘š β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘š))
5554breq1d 5116 . . . . . . . . 9 (π‘₯ = π‘š β†’ ((πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦) ↔ (πΉβ€˜π‘š) ≲ (πΉβ€˜π‘¦)))
5653, 55imbi12d 345 . . . . . . . 8 (π‘₯ = π‘š β†’ ((π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ↔ (π‘š ≀ 𝑦 β†’ (πΉβ€˜π‘š) ≲ (πΉβ€˜π‘¦))))
57 breq2 5110 . . . . . . . . 9 (𝑦 = 𝑛 β†’ (π‘š ≀ 𝑦 ↔ π‘š ≀ 𝑛))
58 fveq2 6843 . . . . . . . . . 10 (𝑦 = 𝑛 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘›))
5958breq2d 5118 . . . . . . . . 9 (𝑦 = 𝑛 β†’ ((πΉβ€˜π‘š) ≲ (πΉβ€˜π‘¦) ↔ (πΉβ€˜π‘š) ≲ (πΉβ€˜π‘›)))
6057, 59imbi12d 345 . . . . . . . 8 (𝑦 = 𝑛 β†’ ((π‘š ≀ 𝑦 β†’ (πΉβ€˜π‘š) ≲ (πΉβ€˜π‘¦)) ↔ (π‘š ≀ 𝑛 β†’ (πΉβ€˜π‘š) ≲ (πΉβ€˜π‘›))))
6156, 60cbvral2vw 3226 . . . . . . 7 (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ↔ βˆ€π‘š ∈ 𝐴 βˆ€π‘› ∈ 𝐴 (π‘š ≀ 𝑛 β†’ (πΉβ€˜π‘š) ≲ (πΉβ€˜π‘›)))
6252, 61sylib 217 . . . . . 6 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ βˆ€π‘š ∈ 𝐴 βˆ€π‘› ∈ 𝐴 (π‘š ≀ 𝑛 β†’ (πΉβ€˜π‘š) ≲ (πΉβ€˜π‘›)))
6351simprd 497 . . . . . . 7 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))
64 breq1 5109 . . . . . . . . 9 (𝑒 = 𝑖 β†’ (𝑒 ≲ 𝑣 ↔ 𝑖 ≲ 𝑣))
65 fveq2 6843 . . . . . . . . . 10 (𝑒 = 𝑖 β†’ (πΊβ€˜π‘’) = (πΊβ€˜π‘–))
6665breq1d 5116 . . . . . . . . 9 (𝑒 = 𝑖 β†’ ((πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£) ↔ (πΊβ€˜π‘–) ≀ (πΊβ€˜π‘£)))
6764, 66imbi12d 345 . . . . . . . 8 (𝑒 = 𝑖 β†’ ((𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)) ↔ (𝑖 ≲ 𝑣 β†’ (πΊβ€˜π‘–) ≀ (πΊβ€˜π‘£))))
68 breq2 5110 . . . . . . . . 9 (𝑣 = 𝑗 β†’ (𝑖 ≲ 𝑣 ↔ 𝑖 ≲ 𝑗))
69 fveq2 6843 . . . . . . . . . 10 (𝑣 = 𝑗 β†’ (πΊβ€˜π‘£) = (πΊβ€˜π‘—))
7069breq2d 5118 . . . . . . . . 9 (𝑣 = 𝑗 β†’ ((πΊβ€˜π‘–) ≀ (πΊβ€˜π‘£) ↔ (πΊβ€˜π‘–) ≀ (πΊβ€˜π‘—)))
7168, 70imbi12d 345 . . . . . . . 8 (𝑣 = 𝑗 β†’ ((𝑖 ≲ 𝑣 β†’ (πΊβ€˜π‘–) ≀ (πΊβ€˜π‘£)) ↔ (𝑖 ≲ 𝑗 β†’ (πΊβ€˜π‘–) ≀ (πΊβ€˜π‘—))))
7267, 71cbvral2vw 3226 . . . . . . 7 (βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)) ↔ βˆ€π‘– ∈ 𝐡 βˆ€π‘— ∈ 𝐡 (𝑖 ≲ 𝑗 β†’ (πΊβ€˜π‘–) ≀ (πΊβ€˜π‘—)))
7363, 72sylib 217 . . . . . 6 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ βˆ€π‘– ∈ 𝐡 βˆ€π‘— ∈ 𝐡 (𝑖 ≲ 𝑗 β†’ (πΊβ€˜π‘–) ≀ (πΊβ€˜π‘—)))
74 id 22 . . . . . . . 8 (π‘₯ = π‘š β†’ π‘₯ = π‘š)
75 2fveq3 6848 . . . . . . . 8 (π‘₯ = π‘š β†’ (πΊβ€˜(πΉβ€˜π‘₯)) = (πΊβ€˜(πΉβ€˜π‘š)))
7674, 75breq12d 5119 . . . . . . 7 (π‘₯ = π‘š β†’ (π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)) ↔ π‘š ≀ (πΊβ€˜(πΉβ€˜π‘š))))
77 simplr 768 . . . . . . 7 ((((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) ∧ π‘š ∈ 𝐴) β†’ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)))
78 simpr 486 . . . . . . 7 ((((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) ∧ π‘š ∈ 𝐴) β†’ π‘š ∈ 𝐴)
7976, 77, 78rspcdva 3581 . . . . . 6 ((((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) ∧ π‘š ∈ 𝐴) β†’ π‘š ≀ (πΊβ€˜(πΉβ€˜π‘š)))
80 2fveq3 6848 . . . . . . . 8 (𝑒 = 𝑖 β†’ (πΉβ€˜(πΊβ€˜π‘’)) = (πΉβ€˜(πΊβ€˜π‘–)))
81 id 22 . . . . . . . 8 (𝑒 = 𝑖 β†’ 𝑒 = 𝑖)
8280, 81breq12d 5119 . . . . . . 7 (𝑒 = 𝑖 β†’ ((πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ↔ (πΉβ€˜(πΊβ€˜π‘–)) ≲ 𝑖))
83 simpllr 775 . . . . . . 7 ((((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) ∧ 𝑖 ∈ 𝐡) β†’ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒)
84 simpr 486 . . . . . . 7 ((((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) ∧ 𝑖 ∈ 𝐡) β†’ 𝑖 ∈ 𝐡)
8582, 83, 84rspcdva 3581 . . . . . 6 ((((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) ∧ 𝑖 ∈ 𝐡) β†’ (πΉβ€˜(πΊβ€˜π‘–)) ≲ 𝑖)
861, 2, 3, 4, 5, 46, 47, 49, 50, 62, 73, 79, 85dfmgc2lem 31904 . . . . 5 (((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒) ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))) β†’ 𝐹𝐻𝐺)
8786anasss 468 . . . 4 ((((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£)))) ∧ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)))) β†’ 𝐹𝐻𝐺)
8887anasss 468 . . 3 (((πœ‘ ∧ (𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴)) ∧ ((βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))) ∧ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯))))) β†’ 𝐹𝐻𝐺)
8988anasss 468 . 2 ((πœ‘ ∧ ((𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴) ∧ ((βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))) ∧ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)))))) β†’ 𝐹𝐻𝐺)
9045, 89impbida 800 1 (πœ‘ β†’ (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐡⟢𝐴) ∧ ((βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯ ≀ 𝑦 β†’ (πΉβ€˜π‘₯) ≲ (πΉβ€˜π‘¦)) ∧ βˆ€π‘’ ∈ 𝐡 βˆ€π‘£ ∈ 𝐡 (𝑒 ≲ 𝑣 β†’ (πΊβ€˜π‘’) ≀ (πΊβ€˜π‘£))) ∧ (βˆ€π‘’ ∈ 𝐡 (πΉβ€˜(πΊβ€˜π‘’)) ≲ 𝑒 ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ ≀ (πΊβ€˜(πΉβ€˜π‘₯)))))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061   class class class wbr 5106  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358  Basecbs 17088  lecple 17145   Proset cproset 18187  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-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8770  df-proset 18189  df-mgc 31890
This theorem is referenced by:  mgcmnt1d  31906  mgcmnt2d  31907  mgcf1olem1  31910  mgcf1olem2  31911  mgcf1o  31912
  Copyright terms: Public domain W3C validator