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

Theorem mgcmnt2d 31026
Description: Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
Hypotheses
Ref Expression
mgcmntd.1 𝐻 = (𝑉MGalConn𝑊)
mgcmntd.2 (𝜑𝑉 ∈ Proset )
mgcmntd.3 (𝜑𝑊 ∈ Proset )
mgcmntd.4 (𝜑𝐹𝐻𝐺)
Assertion
Ref Expression
mgcmnt2d (𝜑𝐺 ∈ (𝑊Monot𝑉))

Proof of Theorem mgcmnt2d
Dummy variables 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mgcmntd.3 . 2 (𝜑𝑊 ∈ Proset )
2 mgcmntd.2 . 2 (𝜑𝑉 ∈ Proset )
3 eqid 2739 . . 3 (Base‘𝑉) = (Base‘𝑉)
4 eqid 2739 . . 3 (Base‘𝑊) = (Base‘𝑊)
5 eqid 2739 . . 3 (le‘𝑉) = (le‘𝑉)
6 eqid 2739 . . 3 (le‘𝑊) = (le‘𝑊)
7 mgcmntd.1 . . 3 𝐻 = (𝑉MGalConn𝑊)
8 mgcmntd.4 . . 3 (𝜑𝐹𝐻𝐺)
93, 4, 5, 6, 7, 2, 1, 8mgcf2 31017 . 2 (𝜑𝐺:(Base‘𝑊)⟶(Base‘𝑉))
103, 4, 5, 6, 7, 2, 1dfmgc2 31024 . . . . 5 (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:(Base‘𝑉)⟶(Base‘𝑊) ∧ 𝐺:(Base‘𝑊)⟶(Base‘𝑉)) ∧ ((∀𝑥 ∈ (Base‘𝑉)∀𝑦 ∈ (Base‘𝑉)(𝑥(le‘𝑉)𝑦 → (𝐹𝑥)(le‘𝑊)(𝐹𝑦)) ∧ ∀𝑢 ∈ (Base‘𝑊)∀𝑣 ∈ (Base‘𝑊)(𝑢(le‘𝑊)𝑣 → (𝐺𝑢)(le‘𝑉)(𝐺𝑣))) ∧ (∀𝑢 ∈ (Base‘𝑊)(𝐹‘(𝐺𝑢))(le‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑉)𝑥(le‘𝑉)(𝐺‘(𝐹𝑥)))))))
118, 10mpbid 235 . . . 4 (𝜑 → ((𝐹:(Base‘𝑉)⟶(Base‘𝑊) ∧ 𝐺:(Base‘𝑊)⟶(Base‘𝑉)) ∧ ((∀𝑥 ∈ (Base‘𝑉)∀𝑦 ∈ (Base‘𝑉)(𝑥(le‘𝑉)𝑦 → (𝐹𝑥)(le‘𝑊)(𝐹𝑦)) ∧ ∀𝑢 ∈ (Base‘𝑊)∀𝑣 ∈ (Base‘𝑊)(𝑢(le‘𝑊)𝑣 → (𝐺𝑢)(le‘𝑉)(𝐺𝑣))) ∧ (∀𝑢 ∈ (Base‘𝑊)(𝐹‘(𝐺𝑢))(le‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑉)𝑥(le‘𝑉)(𝐺‘(𝐹𝑥))))))
1211simprld 772 . . 3 (𝜑 → (∀𝑥 ∈ (Base‘𝑉)∀𝑦 ∈ (Base‘𝑉)(𝑥(le‘𝑉)𝑦 → (𝐹𝑥)(le‘𝑊)(𝐹𝑦)) ∧ ∀𝑢 ∈ (Base‘𝑊)∀𝑣 ∈ (Base‘𝑊)(𝑢(le‘𝑊)𝑣 → (𝐺𝑢)(le‘𝑉)(𝐺𝑣))))
1312simprd 499 . 2 (𝜑 → ∀𝑢 ∈ (Base‘𝑊)∀𝑣 ∈ (Base‘𝑊)(𝑢(le‘𝑊)𝑣 → (𝐺𝑢)(le‘𝑉)(𝐺𝑣)))
144, 3, 6, 5ismnt 31011 . . 3 ((𝑊 ∈ Proset ∧ 𝑉 ∈ Proset ) → (𝐺 ∈ (𝑊Monot𝑉) ↔ (𝐺:(Base‘𝑊)⟶(Base‘𝑉) ∧ ∀𝑢 ∈ (Base‘𝑊)∀𝑣 ∈ (Base‘𝑊)(𝑢(le‘𝑊)𝑣 → (𝐺𝑢)(le‘𝑉)(𝐺𝑣)))))
1514biimpar 481 . 2 (((𝑊 ∈ Proset ∧ 𝑉 ∈ Proset ) ∧ (𝐺:(Base‘𝑊)⟶(Base‘𝑉) ∧ ∀𝑢 ∈ (Base‘𝑊)∀𝑣 ∈ (Base‘𝑊)(𝑢(le‘𝑊)𝑣 → (𝐺𝑢)(le‘𝑉)(𝐺𝑣)))) → 𝐺 ∈ (𝑊Monot𝑉))
161, 2, 9, 13, 15syl22anc 839 1 (𝜑𝐺 ∈ (𝑊Monot𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2112  wral 3064   class class class wbr 5069  wf 6396  cfv 6400  (class class class)co 7234  Basecbs 16792  lecple 16841   Proset cproset 17832  Monotcmnt 31006  MGalConncmgc 31007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-br 5070  df-opab 5132  df-id 5471  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-fv 6408  df-ov 7237  df-oprab 7238  df-mpo 7239  df-map 8533  df-proset 17834  df-mnt 31008  df-mgc 31009
This theorem is referenced by:  mgcf1o  31031
  Copyright terms: Public domain W3C validator