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 31856
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 31847 . . . 4 (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ∀𝑥𝐴𝑦𝐵 ((𝐹𝑥) 𝑦𝑥 (𝐺𝑦)))))
98simprbda 499 . . 3 ((𝜑𝐹𝐻𝐺) → (𝐹:𝐴𝐵𝐺:𝐵𝐴))
106ad4antr 730 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑉 ∈ Proset )
117ad4antr 730 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑊 ∈ Proset )
12 simp-4r 782 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝐹𝐻𝐺)
13 simpllr 774 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑥𝐴)
14 simplr 767 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑦𝐴)
15 simpr 485 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑥 𝑦)
161, 2, 3, 4, 5, 10, 11, 12, 13, 14, 15mgcmnt1 31852 . . . . . . . 8 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → (𝐹𝑥) (𝐹𝑦))
1716ex 413 . . . . . . 7 ((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) → (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
1817anasss 467 . . . . . 6 (((𝜑𝐹𝐻𝐺) ∧ (𝑥𝐴𝑦𝐴)) → (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
1918ralrimivva 3197 . . . . 5 ((𝜑𝐹𝐻𝐺) → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
206ad4antr 730 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑉 ∈ Proset )
217ad4antr 730 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑊 ∈ Proset )
22 simp-4r 782 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝐹𝐻𝐺)
23 simpllr 774 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑢𝐵)
24 simplr 767 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑣𝐵)
25 simpr 485 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑢 𝑣)
261, 2, 3, 4, 5, 20, 21, 22, 23, 24, 25mgcmnt2 31853 . . . . . . . 8 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → (𝐺𝑢) (𝐺𝑣))
2726ex 413 . . . . . . 7 ((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) → (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
2827anasss 467 . . . . . 6 (((𝜑𝐹𝐻𝐺) ∧ (𝑢𝐵𝑣𝐵)) → (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
2928ralrimivva 3197 . . . . 5 ((𝜑𝐹𝐻𝐺) → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
3019, 29jca 512 . . . 4 ((𝜑𝐹𝐻𝐺) → (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))))
316ad2antrr 724 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → 𝑉 ∈ Proset )
327ad2antrr 724 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → 𝑊 ∈ Proset )
33 simplr 767 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → 𝐹𝐻𝐺)
34 simpr 485 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → 𝑢𝐵)
351, 2, 3, 4, 5, 31, 32, 33, 34mgccole2 31851 . . . . . 6 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → (𝐹‘(𝐺𝑢)) 𝑢)
3635ralrimiva 3143 . . . . 5 ((𝜑𝐹𝐻𝐺) → ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢)
376ad2antrr 724 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝑉 ∈ Proset )
387ad2antrr 724 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝑊 ∈ Proset )
39 simplr 767 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝐹𝐻𝐺)
40 simpr 485 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝑥𝐴)
411, 2, 3, 4, 5, 37, 38, 39, 40mgccole1 31850 . . . . . 6 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝑥 (𝐺‘(𝐹𝑥)))
4241ralrimiva 3143 . . . . 5 ((𝜑𝐹𝐻𝐺) → ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))
4336, 42jca 512 . . . 4 ((𝜑𝐹𝐻𝐺) → (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))))
4430, 43jca 512 . . 3 ((𝜑𝐹𝐻𝐺) → ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))))
459, 44jca 512 . 2 ((𝜑𝐹𝐻𝐺) → ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))))))
466ad4antr 730 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝑉 ∈ Proset )
477ad4antr 730 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝑊 ∈ Proset )
48 simp-4r 782 . . . . . . 7 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → (𝐹:𝐴𝐵𝐺:𝐵𝐴))
4948simpld 495 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝐹:𝐴𝐵)
5048simprd 496 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝐺:𝐵𝐴)
51 simpllr 774 . . . . . . . 8 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))))
5251simpld 495 . . . . . . 7 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
53 breq1 5108 . . . . . . . . 9 (𝑥 = 𝑚 → (𝑥 𝑦𝑚 𝑦))
54 fveq2 6842 . . . . . . . . . 10 (𝑥 = 𝑚 → (𝐹𝑥) = (𝐹𝑚))
5554breq1d 5115 . . . . . . . . 9 (𝑥 = 𝑚 → ((𝐹𝑥) (𝐹𝑦) ↔ (𝐹𝑚) (𝐹𝑦)))
5653, 55imbi12d 344 . . . . . . . 8 (𝑥 = 𝑚 → ((𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ↔ (𝑚 𝑦 → (𝐹𝑚) (𝐹𝑦))))
57 breq2 5109 . . . . . . . . 9 (𝑦 = 𝑛 → (𝑚 𝑦𝑚 𝑛))
58 fveq2 6842 . . . . . . . . . 10 (𝑦 = 𝑛 → (𝐹𝑦) = (𝐹𝑛))
5958breq2d 5117 . . . . . . . . 9 (𝑦 = 𝑛 → ((𝐹𝑚) (𝐹𝑦) ↔ (𝐹𝑚) (𝐹𝑛)))
6057, 59imbi12d 344 . . . . . . . 8 (𝑦 = 𝑛 → ((𝑚 𝑦 → (𝐹𝑚) (𝐹𝑦)) ↔ (𝑚 𝑛 → (𝐹𝑚) (𝐹𝑛))))
6156, 60cbvral2vw 3227 . . . . . . 7 (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ↔ ∀𝑚𝐴𝑛𝐴 (𝑚 𝑛 → (𝐹𝑚) (𝐹𝑛)))
6252, 61sylib 217 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → ∀𝑚𝐴𝑛𝐴 (𝑚 𝑛 → (𝐹𝑚) (𝐹𝑛)))
6351simprd 496 . . . . . . 7 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
64 breq1 5108 . . . . . . . . 9 (𝑢 = 𝑖 → (𝑢 𝑣𝑖 𝑣))
65 fveq2 6842 . . . . . . . . . 10 (𝑢 = 𝑖 → (𝐺𝑢) = (𝐺𝑖))
6665breq1d 5115 . . . . . . . . 9 (𝑢 = 𝑖 → ((𝐺𝑢) (𝐺𝑣) ↔ (𝐺𝑖) (𝐺𝑣)))
6764, 66imbi12d 344 . . . . . . . 8 (𝑢 = 𝑖 → ((𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)) ↔ (𝑖 𝑣 → (𝐺𝑖) (𝐺𝑣))))
68 breq2 5109 . . . . . . . . 9 (𝑣 = 𝑗 → (𝑖 𝑣𝑖 𝑗))
69 fveq2 6842 . . . . . . . . . 10 (𝑣 = 𝑗 → (𝐺𝑣) = (𝐺𝑗))
7069breq2d 5117 . . . . . . . . 9 (𝑣 = 𝑗 → ((𝐺𝑖) (𝐺𝑣) ↔ (𝐺𝑖) (𝐺𝑗)))
7168, 70imbi12d 344 . . . . . . . 8 (𝑣 = 𝑗 → ((𝑖 𝑣 → (𝐺𝑖) (𝐺𝑣)) ↔ (𝑖 𝑗 → (𝐺𝑖) (𝐺𝑗))))
7267, 71cbvral2vw 3227 . . . . . . 7 (∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)) ↔ ∀𝑖𝐵𝑗𝐵 (𝑖 𝑗 → (𝐺𝑖) (𝐺𝑗)))
7363, 72sylib 217 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → ∀𝑖𝐵𝑗𝐵 (𝑖 𝑗 → (𝐺𝑖) (𝐺𝑗)))
74 id 22 . . . . . . . 8 (𝑥 = 𝑚𝑥 = 𝑚)
75 2fveq3 6847 . . . . . . . 8 (𝑥 = 𝑚 → (𝐺‘(𝐹𝑥)) = (𝐺‘(𝐹𝑚)))
7674, 75breq12d 5118 . . . . . . 7 (𝑥 = 𝑚 → (𝑥 (𝐺‘(𝐹𝑥)) ↔ 𝑚 (𝐺‘(𝐹𝑚))))
77 simplr 767 . . . . . . 7 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑚𝐴) → ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))
78 simpr 485 . . . . . . 7 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑚𝐴) → 𝑚𝐴)
7976, 77, 78rspcdva 3582 . . . . . 6 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑚𝐴) → 𝑚 (𝐺‘(𝐹𝑚)))
80 2fveq3 6847 . . . . . . . 8 (𝑢 = 𝑖 → (𝐹‘(𝐺𝑢)) = (𝐹‘(𝐺𝑖)))
81 id 22 . . . . . . . 8 (𝑢 = 𝑖𝑢 = 𝑖)
8280, 81breq12d 5118 . . . . . . 7 (𝑢 = 𝑖 → ((𝐹‘(𝐺𝑢)) 𝑢 ↔ (𝐹‘(𝐺𝑖)) 𝑖))
83 simpllr 774 . . . . . . 7 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑖𝐵) → ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢)
84 simpr 485 . . . . . . 7 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑖𝐵) → 𝑖𝐵)
8582, 83, 84rspcdva 3582 . . . . . 6 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑖𝐵) → (𝐹‘(𝐺𝑖)) 𝑖)
861, 2, 3, 4, 5, 46, 47, 49, 50, 62, 73, 79, 85dfmgc2lem 31855 . . . . 5 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝐹𝐻𝐺)
8786anasss 467 . . . 4 ((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))) → 𝐹𝐻𝐺)
8887anasss 467 . . 3 (((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))))) → 𝐹𝐻𝐺)
8988anasss 467 . 2 ((𝜑 ∧ ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))))) → 𝐹𝐻𝐺)
9045, 89impbida 799 1 (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3064   class class class wbr 5105  wf 6492  cfv 6496  (class class class)co 7357  Basecbs 17083  lecple 17140   Proset cproset 18182  MGalConncmgc 31839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-map 8767  df-proset 18184  df-mgc 31841
This theorem is referenced by:  mgcmnt1d  31857  mgcmnt2d  31858  mgcf1olem1  31861  mgcf1olem2  31862  mgcf1o  31863
  Copyright terms: Public domain W3C validator