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

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 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ) } )