Definition df-mgc

Description: Define monotone Galois connections. See mgcval for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024)

	Ref	Expression
Assertion	df-mgc	⊢ MGalConn = ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( Base ‘ 𝑣 ) / 𝑎 ⦌ ⦋ ( Base ‘ 𝑤 ) / 𝑏 ⦌ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑏 ↑m 𝑎 ) ∧ 𝑔 ∈ ( 𝑎 ↑m 𝑏 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑣 ) ( 𝑔 ‘ 𝑦 ) ) ) } )

Detailed syntax breakdown

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