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

Metamath Proof Explorer

Theorem dfmgc2

Description: Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024)

Ref Expression
Hypotheses mgcoval.1 ⊢ 𝐴 = ( Base ‘ 𝑉 )
mgcoval.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
mgcoval.3 ⊢ ≤ = ( le ‘ 𝑉 )
mgcoval.4 ⊢ ≲ = ( le ‘ 𝑊 )
mgcval.1 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
mgcval.2 ⊢ ( 𝜑 → 𝑉 ∈ Proset )
mgcval.3 ⊢ ( 𝜑 → 𝑊 ∈ Proset )
Assertion dfmgc2 ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mgcoval.1 ⊢ 𝐴 = ( Base ‘ 𝑉 )
2 mgcoval.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
3 mgcoval.3 ⊢ ≤ = ( le ‘ 𝑉 )
4 mgcoval.4 ⊢ ≲ = ( le ‘ 𝑊 )
5 mgcval.1 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
6 mgcval.2 ⊢ ( 𝜑 → 𝑉 ∈ Proset )
7 mgcval.3 ⊢ ( 𝜑 → 𝑊 ∈ Proset )
8 1 2 3 4 5 6 7 mgcval ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) )
9 8 simprbda ⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) )
10 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑉 ∈ Proset )
11 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑊 ∈ Proset )
12 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝐹 𝐻 𝐺 )
13 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ∈ 𝐴 )
14 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑦 ∈ 𝐴 )
15 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ≤ 𝑦 )
16 1 2 3 4 5 10 11 12 13 14 15 mgcmnt1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) )
17 16 ex ⊢ ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
18 17 anasss ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
19 18 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
20 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑉 ∈ Proset )
21 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑊 ∈ Proset )
22 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝐹 𝐻 𝐺 )
23 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑢 ∈ 𝐵 )
24 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑣 ∈ 𝐵 )
25 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → 𝑢 ≲ 𝑣 )
26 1 2 3 4 5 20 21 22 23 24 25 mgcmnt2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ≲ 𝑣 ) → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) )
27 26 ex ⊢ ( ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
28 27 anasss ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
29 28 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
30 19 29 jca ⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) )
31 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑉 ∈ Proset )
32 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑊 ∈ Proset )
33 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → 𝐹 𝐻 𝐺 )
34 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
35 1 2 3 4 5 31 32 33 34 mgccole2 ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
36 35 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
37 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑉 ∈ Proset )
38 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑊 ∈ Proset )
39 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐹 𝐻 𝐺 )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
41 1 2 3 4 5 37 38 39 40 mgccole1 ⊢ ( ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
42 41 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
43 36 42 jca ⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
44 30 43 jca ⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
45 9 44 jca ⊢ ( ( 𝜑 ∧ 𝐹 𝐻 𝐺 ) → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
46 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑉 ∈ Proset )
47 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑊 ∈ Proset )
48 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) )
49 48 simpld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
50 48 simprd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝐺 : 𝐵 ⟶ 𝐴 )
51 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) )
52 51 simpld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
53 breq1 ⊢ ( 𝑥 = 𝑚 → ( 𝑥 ≤ 𝑦 ↔ 𝑚 ≤ 𝑦 ) )
54 fveq2 ⊢ ( 𝑥 = 𝑚 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑚 ) )
55 54 breq1d ⊢ ( 𝑥 = 𝑚 → ( ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
56 53 55 imbi12d ⊢ ( 𝑥 = 𝑚 → ( ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑚 ≤ 𝑦 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) )
57 breq2 ⊢ ( 𝑦 = 𝑛 → ( 𝑚 ≤ 𝑦 ↔ 𝑚 ≤ 𝑛 ) )
58 fveq2 ⊢ ( 𝑦 = 𝑛 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑛 ) )
59 58 breq2d ⊢ ( 𝑦 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑛 ) ) )
60 57 59 imbi12d ⊢ ( 𝑦 = 𝑛 → ( ( 𝑚 ≤ 𝑦 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑚 ≤ 𝑛 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑛 ) ) ) )
61 56 60 cbvral2vw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑚 ∈ 𝐴 ∀ 𝑛 ∈ 𝐴 ( 𝑚 ≤ 𝑛 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑛 ) ) )
62 52 61 sylib ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑚 ∈ 𝐴 ∀ 𝑛 ∈ 𝐴 ( 𝑚 ≤ 𝑛 → ( 𝐹 ‘ 𝑚 ) ≲ ( 𝐹 ‘ 𝑛 ) ) )
63 51 simprd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
64 breq1 ⊢ ( 𝑢 = 𝑖 → ( 𝑢 ≲ 𝑣 ↔ 𝑖 ≲ 𝑣 ) )
65 fveq2 ⊢ ( 𝑢 = 𝑖 → ( 𝐺 ‘ 𝑢 ) = ( 𝐺 ‘ 𝑖 ) )
66 65 breq1d ⊢ ( 𝑢 = 𝑖 → ( ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ↔ ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
67 64 66 imbi12d ⊢ ( 𝑢 = 𝑖 → ( ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ↔ ( 𝑖 ≲ 𝑣 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) )
68 breq2 ⊢ ( 𝑣 = 𝑗 → ( 𝑖 ≲ 𝑣 ↔ 𝑖 ≲ 𝑗 ) )
69 fveq2 ⊢ ( 𝑣 = 𝑗 → ( 𝐺 ‘ 𝑣 ) = ( 𝐺 ‘ 𝑗 ) )
70 69 breq2d ⊢ ( 𝑣 = 𝑗 → ( ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑣 ) ↔ ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑗 ) ) )
71 68 70 imbi12d ⊢ ( 𝑣 = 𝑗 → ( ( 𝑖 ≲ 𝑣 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ↔ ( 𝑖 ≲ 𝑗 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑗 ) ) ) )
72 67 71 cbvral2vw ⊢ ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ↔ ∀ 𝑖 ∈ 𝐵 ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≲ 𝑗 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑗 ) ) )
73 63 72 sylib ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑖 ∈ 𝐵 ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≲ 𝑗 → ( 𝐺 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑗 ) ) )
74 id ⊢ ( 𝑥 = 𝑚 → 𝑥 = 𝑚 )
75 2fveq3 ⊢ ( 𝑥 = 𝑚 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑚 ) ) )
76 74 75 breq12d ⊢ ( 𝑥 = 𝑚 → ( 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ 𝑚 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
77 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
78 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ∈ 𝐴 )
79 76 77 78 rspcdva ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑚 ) ) )
80 2fveq3 ⊢ ( 𝑢 = 𝑖 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑖 ) ) )
81 id ⊢ ( 𝑢 = 𝑖 → 𝑢 = 𝑖 )
82 80 81 breq12d ⊢ ( 𝑢 = 𝑖 → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑖 ) ) ≲ 𝑖 ) )
83 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑖 ∈ 𝐵 ) → ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
84 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑖 ∈ 𝐵 ) → 𝑖 ∈ 𝐵 )
85 82 83 84 rspcdva ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑖 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑖 ) ) ≲ 𝑖 )
86 1 2 3 4 5 46 47 49 50 62 73 79 85 dfmgc2lem ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝐹 𝐻 𝐺 )
87 86 anasss ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) → 𝐹 𝐻 𝐺 )
88 87 anasss ⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) → 𝐹 𝐻 𝐺 )
89 88 anasss ⊢ ( ( 𝜑 ∧ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) ) → 𝐹 𝐻 𝐺 )
90 45 89 impbida ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) ) )