This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑣 ) ( 𝑔 ‘ 𝑦 ) ) ) } )