Definition df-mgc 30770

Description: Define monotone Galois connections. See mgcval 30776 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

Step	Hyp	Ref	Expression
1		cmgc 30768	. 2 class MGalConn
2		vv	. . 3 setvar 𝑣
3		vw	. . 3 setvar 𝑤
4		cvv 3407	. . 3 class V
5		va	. . . 4 setvar 𝑎
6	2	cv 1538	. . . . 5 class 𝑣
7		cbs 16526	. . . . 5 class Base
8	6, 7	cfv 6328	. . . 4 class (Base‘𝑣)
9		vb	. . . . 5 setvar 𝑏
10	3	cv 1538	. . . . . 6 class 𝑤
11	10, 7	cfv 6328	. . . . 5 class (Base‘𝑤)
12		vf	. . . . . . . . . 10 setvar 𝑓
13	12	cv 1538	. . . . . . . . 9 class 𝑓
14	9	cv 1538	. . . . . . . . . 10 class 𝑏
15	5	cv 1538	. . . . . . . . . 10 class 𝑎
16		cmap 8409	. . . . . . . . . 10 class ↑m
17	14, 15, 16	co 7143	. . . . . . . . 9 class (𝑏 ↑m 𝑎)
18	13, 17	wcel 2112	. . . . . . . 8 wff 𝑓 ∈ (𝑏 ↑m 𝑎)
19		vg	. . . . . . . . . 10 setvar 𝑔
20	19	cv 1538	. . . . . . . . 9 class 𝑔
21	15, 14, 16	co 7143	. . . . . . . . 9 class (𝑎 ↑m 𝑏)
22	20, 21	wcel 2112	. . . . . . . 8 wff 𝑔 ∈ (𝑎 ↑m 𝑏)
23	18, 22	wa 400	. . . . . . 7 wff (𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏))
24		vx	. . . . . . . . . . . . 13 setvar 𝑥
25	24	cv 1538	. . . . . . . . . . . 12 class 𝑥
26	25, 13	cfv 6328	. . . . . . . . . . 11 class (𝑓‘𝑥)
27		vy	. . . . . . . . . . . 12 setvar 𝑦
28	27	cv 1538	. . . . . . . . . . 11 class 𝑦
29		cple 16615	. . . . . . . . . . . 12 class le
30	10, 29	cfv 6328	. . . . . . . . . . 11 class (le‘𝑤)
31	26, 28, 30	wbr 5025	. . . . . . . . . 10 wff (𝑓‘𝑥)(le‘𝑤)𝑦
32	28, 20	cfv 6328	. . . . . . . . . . 11 class (𝑔‘𝑦)
33	6, 29	cfv 6328	. . . . . . . . . . 11 class (le‘𝑣)
34	25, 32, 33	wbr 5025	. . . . . . . . . 10 wff 𝑥(le‘𝑣)(𝑔‘𝑦)
35	31, 34	wb 209	. . . . . . . . 9 wff ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦))
36	35, 27, 14	wral 3068	. . . . . . . 8 wff ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦))
37	36, 24, 15	wral 3068	. . . . . . 7 wff ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦))
38	23, 37	wa 400	. . . . . 6 wff ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))
39	38, 12, 19	copab 5087	. . . . 5 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))}
40	9, 11, 39	csb 3801	. . . 4 class ⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))}
41	5, 8, 40	csb 3801	. . 3 class ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))}
42	2, 3, 4, 4, 41	cmpo 7145	. 2 class (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))})
43	1, 42	wceq 1539	1 wff MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))})

This definition is referenced by:  mgcoval  30775