Metamath Proof Explorer


Theorem mgcoval

Description: Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024)

Ref Expression
Hypotheses mgcoval.1 𝐴 = ( Base ‘ 𝑉 )
mgcoval.2 𝐵 = ( Base ‘ 𝑊 )
mgcoval.3 = ( le ‘ 𝑉 )
mgcoval.4 = ( le ‘ 𝑊 )
Assertion mgcoval ( ( 𝑉𝑋𝑊𝑌 ) → ( 𝑉 MGalConn 𝑊 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) } )

Proof

Step Hyp Ref Expression
1 mgcoval.1 𝐴 = ( Base ‘ 𝑉 )
2 mgcoval.2 𝐵 = ( Base ‘ 𝑊 )
3 mgcoval.3 = ( le ‘ 𝑉 )
4 mgcoval.4 = ( le ‘ 𝑊 )
5 df-mgc MGalConn = ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ( Base ‘ 𝑣 ) / 𝑎 ( Base ‘ 𝑤 ) / 𝑏 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑏m 𝑎 ) ∧ 𝑔 ∈ ( 𝑎m 𝑏 ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ) ) } )
6 5 a1i ( ( 𝑉𝑋𝑊𝑌 ) → MGalConn = ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ( Base ‘ 𝑣 ) / 𝑎 ( Base ‘ 𝑤 ) / 𝑏 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑏m 𝑎 ) ∧ 𝑔 ∈ ( 𝑎m 𝑏 ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ) ) } ) )
7 fvexd ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) → ( Base ‘ 𝑣 ) ∈ V )
8 simprl ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) → 𝑣 = 𝑉 )
9 8 fveq2d ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) → ( Base ‘ 𝑣 ) = ( Base ‘ 𝑉 ) )
10 9 1 eqtr4di ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) → ( Base ‘ 𝑣 ) = 𝐴 )
11 fvexd ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) → ( Base ‘ 𝑤 ) ∈ V )
12 simplrr ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) → 𝑤 = 𝑊 )
13 12 fveq2d ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
14 13 2 eqtr4di ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) → ( Base ‘ 𝑤 ) = 𝐵 )
15 simpr ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
16 simplr ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → 𝑎 = 𝐴 )
17 15 16 oveq12d ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( 𝑏m 𝑎 ) = ( 𝐵m 𝐴 ) )
18 17 eleq2d ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ∈ ( 𝑏m 𝑎 ) ↔ 𝑓 ∈ ( 𝐵m 𝐴 ) ) )
19 16 15 oveq12d ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( 𝑎m 𝑏 ) = ( 𝐴m 𝐵 ) )
20 19 eleq2d ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( 𝑔 ∈ ( 𝑎m 𝑏 ) ↔ 𝑔 ∈ ( 𝐴m 𝐵 ) ) )
21 18 20 anbi12d ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑓 ∈ ( 𝑏m 𝑎 ) ∧ 𝑔 ∈ ( 𝑎m 𝑏 ) ) ↔ ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ) )
22 12 adantr ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → 𝑤 = 𝑊 )
23 22 fveq2d ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( le ‘ 𝑤 ) = ( le ‘ 𝑊 ) )
24 23 4 eqtr4di ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( le ‘ 𝑤 ) = )
25 24 breqd ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦 ↔ ( 𝑓𝑥 ) 𝑦 ) )
26 8 ad2antrr ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → 𝑣 = 𝑉 )
27 26 fveq2d ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( le ‘ 𝑣 ) = ( le ‘ 𝑉 ) )
28 27 3 eqtr4di ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( le ‘ 𝑣 ) = )
29 28 breqd ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ↔ 𝑥 ( 𝑔𝑦 ) ) )
30 25 29 bibi12d ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ) ↔ ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) )
31 15 30 raleqbidv ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑦𝑏 ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ) ↔ ∀ 𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) )
32 16 31 raleqbidv ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) )
33 21 32 anbi12d ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑓 ∈ ( 𝑏m 𝑎 ) ∧ 𝑔 ∈ ( 𝑎m 𝑏 ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ) ) ↔ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) ) )
34 33 opabbidv ( ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) ∧ 𝑏 = 𝐵 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑏m 𝑎 ) ∧ 𝑔 ∈ ( 𝑎m 𝑏 ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) } )
35 11 14 34 csbied2 ( ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) ∧ 𝑎 = 𝐴 ) → ( Base ‘ 𝑤 ) / 𝑏 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑏m 𝑎 ) ∧ 𝑔 ∈ ( 𝑎m 𝑏 ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) } )
36 7 10 35 csbied2 ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( 𝑣 = 𝑉𝑤 = 𝑊 ) ) → ( Base ‘ 𝑣 ) / 𝑎 ( Base ‘ 𝑤 ) / 𝑏 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑏m 𝑎 ) ∧ 𝑔 ∈ ( 𝑎m 𝑏 ) ) ∧ ∀ 𝑥𝑎𝑦𝑏 ( ( 𝑓𝑥 ) ( le ‘ 𝑤 ) 𝑦𝑥 ( le ‘ 𝑣 ) ( 𝑔𝑦 ) ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) } )
37 simpl ( ( 𝑉𝑋𝑊𝑌 ) → 𝑉𝑋 )
38 37 elexd ( ( 𝑉𝑋𝑊𝑌 ) → 𝑉 ∈ V )
39 simpr ( ( 𝑉𝑋𝑊𝑌 ) → 𝑊𝑌 )
40 39 elexd ( ( 𝑉𝑋𝑊𝑌 ) → 𝑊 ∈ V )
41 ovexd ( ( 𝑉𝑋𝑊𝑌 ) → ( 𝐵m 𝐴 ) ∈ V )
42 ovexd ( ( 𝑉𝑋𝑊𝑌 ) → ( 𝐴m 𝐵 ) ∈ V )
43 simprll ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) ) → 𝑓 ∈ ( 𝐵m 𝐴 ) )
44 simprlr ( ( ( 𝑉𝑋𝑊𝑌 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) ) → 𝑔 ∈ ( 𝐴m 𝐵 ) )
45 41 42 43 44 opabex2 ( ( 𝑉𝑋𝑊𝑌 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) } ∈ V )
46 6 36 38 40 45 ovmpod ( ( 𝑉𝑋𝑊𝑌 ) → ( 𝑉 MGalConn 𝑊 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴m 𝐵 ) ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝑓𝑥 ) 𝑦𝑥 ( 𝑔𝑦 ) ) ) } )