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