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 31559
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 31550 . . . 4 (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ∀𝑥𝐴𝑦𝐵 ((𝐹𝑥) 𝑦𝑥 (𝐺𝑦)))))
98simprbda 500 . . 3 ((𝜑𝐹𝐻𝐺) → (𝐹:𝐴𝐵𝐺:𝐵𝐴))
106ad4antr 730 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑉 ∈ Proset )
117ad4antr 730 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑊 ∈ Proset )
12 simp-4r 782 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝐹𝐻𝐺)
13 simpllr 774 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑥𝐴)
14 simplr 767 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑦𝐴)
15 simpr 486 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → 𝑥 𝑦)
161, 2, 3, 4, 5, 10, 11, 12, 13, 14, 15mgcmnt1 31555 . . . . . . . 8 (((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) ∧ 𝑥 𝑦) → (𝐹𝑥) (𝐹𝑦))
1716ex 414 . . . . . . 7 ((((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) ∧ 𝑦𝐴) → (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
1817anasss 468 . . . . . 6 (((𝜑𝐹𝐻𝐺) ∧ (𝑥𝐴𝑦𝐴)) → (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
1918ralrimivva 3194 . . . . 5 ((𝜑𝐹𝐻𝐺) → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
206ad4antr 730 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑉 ∈ Proset )
217ad4antr 730 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑊 ∈ Proset )
22 simp-4r 782 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝐹𝐻𝐺)
23 simpllr 774 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑢𝐵)
24 simplr 767 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑣𝐵)
25 simpr 486 . . . . . . . . 9 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → 𝑢 𝑣)
261, 2, 3, 4, 5, 20, 21, 22, 23, 24, 25mgcmnt2 31556 . . . . . . . 8 (((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) ∧ 𝑢 𝑣) → (𝐺𝑢) (𝐺𝑣))
2726ex 414 . . . . . . 7 ((((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) ∧ 𝑣𝐵) → (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
2827anasss 468 . . . . . 6 (((𝜑𝐹𝐻𝐺) ∧ (𝑢𝐵𝑣𝐵)) → (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
2928ralrimivva 3194 . . . . 5 ((𝜑𝐹𝐻𝐺) → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
3019, 29jca 513 . . . 4 ((𝜑𝐹𝐻𝐺) → (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))))
316ad2antrr 724 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → 𝑉 ∈ Proset )
327ad2antrr 724 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → 𝑊 ∈ Proset )
33 simplr 767 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → 𝐹𝐻𝐺)
34 simpr 486 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → 𝑢𝐵)
351, 2, 3, 4, 5, 31, 32, 33, 34mgccole2 31554 . . . . . 6 (((𝜑𝐹𝐻𝐺) ∧ 𝑢𝐵) → (𝐹‘(𝐺𝑢)) 𝑢)
3635ralrimiva 3140 . . . . 5 ((𝜑𝐹𝐻𝐺) → ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢)
376ad2antrr 724 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝑉 ∈ Proset )
387ad2antrr 724 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝑊 ∈ Proset )
39 simplr 767 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝐹𝐻𝐺)
40 simpr 486 . . . . . . 7 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝑥𝐴)
411, 2, 3, 4, 5, 37, 38, 39, 40mgccole1 31553 . . . . . 6 (((𝜑𝐹𝐻𝐺) ∧ 𝑥𝐴) → 𝑥 (𝐺‘(𝐹𝑥)))
4241ralrimiva 3140 . . . . 5 ((𝜑𝐹𝐻𝐺) → ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))
4336, 42jca 513 . . . 4 ((𝜑𝐹𝐻𝐺) → (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))))
4430, 43jca 513 . . 3 ((𝜑𝐹𝐻𝐺) → ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))))
459, 44jca 513 . 2 ((𝜑𝐹𝐻𝐺) → ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))))))
466ad4antr 730 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝑉 ∈ Proset )
477ad4antr 730 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝑊 ∈ Proset )
48 simp-4r 782 . . . . . . 7 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → (𝐹:𝐴𝐵𝐺:𝐵𝐴))
4948simpld 496 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝐹:𝐴𝐵)
5048simprd 497 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝐺:𝐵𝐴)
51 simpllr 774 . . . . . . . 8 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))))
5251simpld 496 . . . . . . 7 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
53 breq1 5099 . . . . . . . . 9 (𝑥 = 𝑚 → (𝑥 𝑦𝑚 𝑦))
54 fveq2 6829 . . . . . . . . . 10 (𝑥 = 𝑚 → (𝐹𝑥) = (𝐹𝑚))
5554breq1d 5106 . . . . . . . . 9 (𝑥 = 𝑚 → ((𝐹𝑥) (𝐹𝑦) ↔ (𝐹𝑚) (𝐹𝑦)))
5653, 55imbi12d 345 . . . . . . . 8 (𝑥 = 𝑚 → ((𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ↔ (𝑚 𝑦 → (𝐹𝑚) (𝐹𝑦))))
57 breq2 5100 . . . . . . . . 9 (𝑦 = 𝑛 → (𝑚 𝑦𝑚 𝑛))
58 fveq2 6829 . . . . . . . . . 10 (𝑦 = 𝑛 → (𝐹𝑦) = (𝐹𝑛))
5958breq2d 5108 . . . . . . . . 9 (𝑦 = 𝑛 → ((𝐹𝑚) (𝐹𝑦) ↔ (𝐹𝑚) (𝐹𝑛)))
6057, 59imbi12d 345 . . . . . . . 8 (𝑦 = 𝑛 → ((𝑚 𝑦 → (𝐹𝑚) (𝐹𝑦)) ↔ (𝑚 𝑛 → (𝐹𝑚) (𝐹𝑛))))
6156, 60cbvral2vw 3224 . . . . . . 7 (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ↔ ∀𝑚𝐴𝑛𝐴 (𝑚 𝑛 → (𝐹𝑚) (𝐹𝑛)))
6252, 61sylib 217 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → ∀𝑚𝐴𝑛𝐴 (𝑚 𝑛 → (𝐹𝑚) (𝐹𝑛)))
6351simprd 497 . . . . . . 7 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
64 breq1 5099 . . . . . . . . 9 (𝑢 = 𝑖 → (𝑢 𝑣𝑖 𝑣))
65 fveq2 6829 . . . . . . . . . 10 (𝑢 = 𝑖 → (𝐺𝑢) = (𝐺𝑖))
6665breq1d 5106 . . . . . . . . 9 (𝑢 = 𝑖 → ((𝐺𝑢) (𝐺𝑣) ↔ (𝐺𝑖) (𝐺𝑣)))
6764, 66imbi12d 345 . . . . . . . 8 (𝑢 = 𝑖 → ((𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)) ↔ (𝑖 𝑣 → (𝐺𝑖) (𝐺𝑣))))
68 breq2 5100 . . . . . . . . 9 (𝑣 = 𝑗 → (𝑖 𝑣𝑖 𝑗))
69 fveq2 6829 . . . . . . . . . 10 (𝑣 = 𝑗 → (𝐺𝑣) = (𝐺𝑗))
7069breq2d 5108 . . . . . . . . 9 (𝑣 = 𝑗 → ((𝐺𝑖) (𝐺𝑣) ↔ (𝐺𝑖) (𝐺𝑗)))
7168, 70imbi12d 345 . . . . . . . 8 (𝑣 = 𝑗 → ((𝑖 𝑣 → (𝐺𝑖) (𝐺𝑣)) ↔ (𝑖 𝑗 → (𝐺𝑖) (𝐺𝑗))))
7267, 71cbvral2vw 3224 . . . . . . 7 (∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)) ↔ ∀𝑖𝐵𝑗𝐵 (𝑖 𝑗 → (𝐺𝑖) (𝐺𝑗)))
7363, 72sylib 217 . . . . . 6 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → ∀𝑖𝐵𝑗𝐵 (𝑖 𝑗 → (𝐺𝑖) (𝐺𝑗)))
74 id 22 . . . . . . . 8 (𝑥 = 𝑚𝑥 = 𝑚)
75 2fveq3 6834 . . . . . . . 8 (𝑥 = 𝑚 → (𝐺‘(𝐹𝑥)) = (𝐺‘(𝐹𝑚)))
7674, 75breq12d 5109 . . . . . . 7 (𝑥 = 𝑚 → (𝑥 (𝐺‘(𝐹𝑥)) ↔ 𝑚 (𝐺‘(𝐹𝑚))))
77 simplr 767 . . . . . . 7 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑚𝐴) → ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))
78 simpr 486 . . . . . . 7 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑚𝐴) → 𝑚𝐴)
7976, 77, 78rspcdva 3574 . . . . . 6 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑚𝐴) → 𝑚 (𝐺‘(𝐹𝑚)))
80 2fveq3 6834 . . . . . . . 8 (𝑢 = 𝑖 → (𝐹‘(𝐺𝑢)) = (𝐹‘(𝐺𝑖)))
81 id 22 . . . . . . . 8 (𝑢 = 𝑖𝑢 = 𝑖)
8280, 81breq12d 5109 . . . . . . 7 (𝑢 = 𝑖 → ((𝐹‘(𝐺𝑢)) 𝑢 ↔ (𝐹‘(𝐺𝑖)) 𝑖))
83 simpllr 774 . . . . . . 7 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑖𝐵) → ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢)
84 simpr 486 . . . . . . 7 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑖𝐵) → 𝑖𝐵)
8582, 83, 84rspcdva 3574 . . . . . 6 ((((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) ∧ 𝑖𝐵) → (𝐹‘(𝐺𝑖)) 𝑖)
861, 2, 3, 4, 5, 46, 47, 49, 50, 62, 73, 79, 85dfmgc2lem 31558 . . . . 5 (((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢) ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))) → 𝐹𝐻𝐺)
8786anasss 468 . . . 4 ((((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))) → 𝐹𝐻𝐺)
8887anasss 468 . . 3 (((𝜑 ∧ (𝐹:𝐴𝐵𝐺:𝐵𝐴)) ∧ ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥))))) → 𝐹𝐻𝐺)
8988anasss 468 . 2 ((𝜑 ∧ ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))))) → 𝐹𝐻𝐺)
9045, 89impbida 799 1 (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1541  wcel 2106  wral 3062   class class class wbr 5096  wf 6479  cfv 6483  (class class class)co 7341  Basecbs 17009  lecple 17066   Proset cproset 18108  MGalConncmgc 31542
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 2708  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-opab 5159  df-id 5522  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-fv 6491  df-ov 7344  df-oprab 7345  df-mpo 7346  df-map 8692  df-proset 18110  df-mgc 31544
This theorem is referenced by:  mgcmnt1d  31560  mgcmnt2d  31561  mgcf1olem1  31564  mgcf1olem2  31565  mgcf1o  31566
  Copyright terms: Public domain W3C validator