Users' Mathboxes 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 31890
Description: Define monotone Galois connections. See mgcval 31896 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 31888 . 2 class MGalConn
2 vv . . 3 setvar 𝑣
3 vw . . 3 setvar 𝑀
4 cvv 3444 . . 3 class V
5 va . . . 4 setvar π‘Ž
62cv 1541 . . . . 5 class 𝑣
7 cbs 17088 . . . . 5 class Base
86, 7cfv 6497 . . . 4 class (Baseβ€˜π‘£)
9 vb . . . . 5 setvar 𝑏
103cv 1541 . . . . . 6 class 𝑀
1110, 7cfv 6497 . . . . 5 class (Baseβ€˜π‘€)
12 vf . . . . . . . . . 10 setvar 𝑓
1312cv 1541 . . . . . . . . 9 class 𝑓
149cv 1541 . . . . . . . . . 10 class 𝑏
155cv 1541 . . . . . . . . . 10 class π‘Ž
16 cmap 8768 . . . . . . . . . 10 class ↑m
1714, 15, 16co 7358 . . . . . . . . 9 class (𝑏 ↑m π‘Ž)
1813, 17wcel 2107 . . . . . . . 8 wff 𝑓 ∈ (𝑏 ↑m π‘Ž)
19 vg . . . . . . . . . 10 setvar 𝑔
2019cv 1541 . . . . . . . . 9 class 𝑔
2115, 14, 16co 7358 . . . . . . . . 9 class (π‘Ž ↑m 𝑏)
2220, 21wcel 2107 . . . . . . . 8 wff 𝑔 ∈ (π‘Ž ↑m 𝑏)
2318, 22wa 397 . . . . . . 7 wff (𝑓 ∈ (𝑏 ↑m π‘Ž) ∧ 𝑔 ∈ (π‘Ž ↑m 𝑏))
24 vx . . . . . . . . . . . . 13 setvar π‘₯
2524cv 1541 . . . . . . . . . . . 12 class π‘₯
2625, 13cfv 6497 . . . . . . . . . . 11 class (π‘“β€˜π‘₯)
27 vy . . . . . . . . . . . 12 setvar 𝑦
2827cv 1541 . . . . . . . . . . 11 class 𝑦
29 cple 17145 . . . . . . . . . . . 12 class le
3010, 29cfv 6497 . . . . . . . . . . 11 class (leβ€˜π‘€)
3126, 28, 30wbr 5106 . . . . . . . . . 10 wff (π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦
3228, 20cfv 6497 . . . . . . . . . . 11 class (π‘”β€˜π‘¦)
336, 29cfv 6497 . . . . . . . . . . 11 class (leβ€˜π‘£)
3425, 32, 33wbr 5106 . . . . . . . . . 10 wff π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦)
3531, 34wb 205 . . . . . . . . 9 wff ((π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦 ↔ π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦))
3635, 27, 14wral 3061 . . . . . . . 8 wff βˆ€π‘¦ ∈ 𝑏 ((π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦 ↔ π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦))
3736, 24, 15wral 3061 . . . . . . 7 wff βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 ((π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦 ↔ π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦))
3823, 37wa 397 . . . . . 6 wff ((𝑓 ∈ (𝑏 ↑m π‘Ž) ∧ 𝑔 ∈ (π‘Ž ↑m 𝑏)) ∧ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 ((π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦 ↔ π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦)))
3938, 12, 19copab 5168 . . . . 5 class {βŸ¨π‘“, π‘”βŸ© ∣ ((𝑓 ∈ (𝑏 ↑m π‘Ž) ∧ 𝑔 ∈ (π‘Ž ↑m 𝑏)) ∧ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 ((π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦 ↔ π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦)))}
409, 11, 39csb 3856 . . . 4 class ⦋(Baseβ€˜π‘€) / π‘β¦Œ{βŸ¨π‘“, π‘”βŸ© ∣ ((𝑓 ∈ (𝑏 ↑m π‘Ž) ∧ 𝑔 ∈ (π‘Ž ↑m 𝑏)) ∧ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 ((π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦 ↔ π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦)))}
415, 8, 40csb 3856 . . 3 class ⦋(Baseβ€˜π‘£) / π‘Žβ¦Œβ¦‹(Baseβ€˜π‘€) / π‘β¦Œ{βŸ¨π‘“, π‘”βŸ© ∣ ((𝑓 ∈ (𝑏 ↑m π‘Ž) ∧ 𝑔 ∈ (π‘Ž ↑m 𝑏)) ∧ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 ((π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦 ↔ π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦)))}
422, 3, 4, 4, 41cmpo 7360 . 2 class (𝑣 ∈ V, 𝑀 ∈ V ↦ ⦋(Baseβ€˜π‘£) / π‘Žβ¦Œβ¦‹(Baseβ€˜π‘€) / π‘β¦Œ{βŸ¨π‘“, π‘”βŸ© ∣ ((𝑓 ∈ (𝑏 ↑m π‘Ž) ∧ 𝑔 ∈ (π‘Ž ↑m 𝑏)) ∧ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 ((π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦 ↔ π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦)))})
431, 42wceq 1542 1 wff MGalConn = (𝑣 ∈ V, 𝑀 ∈ V ↦ ⦋(Baseβ€˜π‘£) / π‘Žβ¦Œβ¦‹(Baseβ€˜π‘€) / π‘β¦Œ{βŸ¨π‘“, π‘”βŸ© ∣ ((𝑓 ∈ (𝑏 ↑m π‘Ž) ∧ 𝑔 ∈ (π‘Ž ↑m 𝑏)) ∧ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ 𝑏 ((π‘“β€˜π‘₯)(leβ€˜π‘€)𝑦 ↔ π‘₯(leβ€˜π‘£)(π‘”β€˜π‘¦)))})
Colors of variables: wff setvar class
This definition is referenced by:  mgcoval  31895
  Copyright terms: Public domain W3C validator