Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mgc Structured version   Visualization version   GIF version

Definition df-mgc 30689
 Description: Define monotone Galois connections. See mgcval 30695 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.)
Assertion
Ref Expression
df-mgc MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ (Base‘𝑣) / 𝑎(Base‘𝑤) / 𝑏{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏m 𝑎) ∧ 𝑔 ∈ (𝑎m 𝑏)) ∧ ∀𝑥𝑎𝑦𝑏 ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦)))})
Distinct variable group:   𝑤,𝑣,𝑎,𝑏,𝑓,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-mgc
StepHypRef Expression
1 cmgc 30687 . 2 class MGalConn
2 vv . . 3 setvar 𝑣
3 vw . . 3 setvar 𝑤
4 cvv 3441 . . 3 class V
5 va . . . 4 setvar 𝑎
62cv 1537 . . . . 5 class 𝑣
7 cbs 16475 . . . . 5 class Base
86, 7cfv 6324 . . . 4 class (Base‘𝑣)
9 vb . . . . 5 setvar 𝑏
103cv 1537 . . . . . 6 class 𝑤
1110, 7cfv 6324 . . . . 5 class (Base‘𝑤)
12 vf . . . . . . . . . 10 setvar 𝑓
1312cv 1537 . . . . . . . . 9 class 𝑓
149cv 1537 . . . . . . . . . 10 class 𝑏
155cv 1537 . . . . . . . . . 10 class 𝑎
16 cmap 8389 . . . . . . . . . 10 class m
1714, 15, 16co 7135 . . . . . . . . 9 class (𝑏m 𝑎)
1813, 17wcel 2111 . . . . . . . 8 wff 𝑓 ∈ (𝑏m 𝑎)
19 vg . . . . . . . . . 10 setvar 𝑔
2019cv 1537 . . . . . . . . 9 class 𝑔
2115, 14, 16co 7135 . . . . . . . . 9 class (𝑎m 𝑏)
2220, 21wcel 2111 . . . . . . . 8 wff 𝑔 ∈ (𝑎m 𝑏)
2318, 22wa 399 . . . . . . 7 wff (𝑓 ∈ (𝑏m 𝑎) ∧ 𝑔 ∈ (𝑎m 𝑏))
24 vx . . . . . . . . . . . . 13 setvar 𝑥
2524cv 1537 . . . . . . . . . . . 12 class 𝑥
2625, 13cfv 6324 . . . . . . . . . . 11 class (𝑓𝑥)
27 vy . . . . . . . . . . . 12 setvar 𝑦
2827cv 1537 . . . . . . . . . . 11 class 𝑦
29 cple 16564 . . . . . . . . . . . 12 class le
3010, 29cfv 6324 . . . . . . . . . . 11 class (le‘𝑤)
3126, 28, 30wbr 5030 . . . . . . . . . 10 wff (𝑓𝑥)(le‘𝑤)𝑦
3228, 20cfv 6324 . . . . . . . . . . 11 class (𝑔𝑦)
336, 29cfv 6324 . . . . . . . . . . 11 class (le‘𝑣)
3425, 32, 33wbr 5030 . . . . . . . . . 10 wff 𝑥(le‘𝑣)(𝑔𝑦)
3531, 34wb 209 . . . . . . . . 9 wff ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦))
3635, 27, 14wral 3106 . . . . . . . 8 wff 𝑦𝑏 ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦))
3736, 24, 15wral 3106 . . . . . . 7 wff 𝑥𝑎𝑦𝑏 ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦))
3823, 37wa 399 . . . . . 6 wff ((𝑓 ∈ (𝑏m 𝑎) ∧ 𝑔 ∈ (𝑎m 𝑏)) ∧ ∀𝑥𝑎𝑦𝑏 ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦)))
3938, 12, 19copab 5092 . . . . 5 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏m 𝑎) ∧ 𝑔 ∈ (𝑎m 𝑏)) ∧ ∀𝑥𝑎𝑦𝑏 ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦)))}
409, 11, 39csb 3828 . . . 4 class (Base‘𝑤) / 𝑏{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏m 𝑎) ∧ 𝑔 ∈ (𝑎m 𝑏)) ∧ ∀𝑥𝑎𝑦𝑏 ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦)))}
415, 8, 40csb 3828 . . 3 class (Base‘𝑣) / 𝑎(Base‘𝑤) / 𝑏{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏m 𝑎) ∧ 𝑔 ∈ (𝑎m 𝑏)) ∧ ∀𝑥𝑎𝑦𝑏 ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦)))}
422, 3, 4, 4, 41cmpo 7137 . 2 class (𝑣 ∈ V, 𝑤 ∈ V ↦ (Base‘𝑣) / 𝑎(Base‘𝑤) / 𝑏{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏m 𝑎) ∧ 𝑔 ∈ (𝑎m 𝑏)) ∧ ∀𝑥𝑎𝑦𝑏 ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦)))})
431, 42wceq 1538 1 wff MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ (Base‘𝑣) / 𝑎(Base‘𝑤) / 𝑏{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏m 𝑎) ∧ 𝑔 ∈ (𝑎m 𝑏)) ∧ ∀𝑥𝑎𝑦𝑏 ((𝑓𝑥)(le‘𝑤)𝑦𝑥(le‘𝑣)(𝑔𝑦)))})
 Colors of variables: wff setvar class This definition is referenced by:  mgcoval  30694
 Copyright terms: Public domain W3C validator