Metamath Proof Explorer

Theorem dfmgc2lem

Description: Lemma for dfmgc2, backwards direction. (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 )
dfmgc2lem.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
dfmgc2lem.2 ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
dfmgc2lem.3 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
dfmgc2lem.4 ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
dfmgc2lem.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
dfmgc2lem.6 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
Assertion dfmgc2lem ( 𝜑 → 𝐹 𝐻 𝐺 )

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 dfmgc2lem.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
9 dfmgc2lem.2 ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
10 dfmgc2lem.3 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
11 dfmgc2lem.4 ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
12 dfmgc2lem.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
13 dfmgc2lem.6 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
14 8 9 jca ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) )
15 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → 𝑉 ∈ Proset )
16 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → 𝑧 ∈ 𝐴 )
17 16 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → 𝑧 ∈ 𝐴 )
18 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → 𝐺 : 𝐵 ⟶ 𝐴 )
19 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
20 19 17 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
21 18 20 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝐴 )
22 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → 𝐺 : 𝐵 ⟶ 𝐴 )
23 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ 𝐵 )
24 22 23 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝐴 )
25 24 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝐴 )
26 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
27 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
28 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) ∧ 𝑥 = 𝑧 ) → 𝑥 = 𝑧 )
29 28 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) ∧ 𝑥 = 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
30 29 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) ∧ 𝑥 = 𝑧 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) )
31 28 30 breq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) ∧ 𝑥 = 𝑧 ) → ( 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ 𝑧 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
32 17 31 rspcdv ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → ( ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) → 𝑧 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
33 27 32 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → 𝑧 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) )
34 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
35 breq1 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( 𝑢 ≲ 𝑣 ↔ ( 𝐹 ‘ 𝑧 ) ≲ 𝑣 ) )
36 fveq2 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( 𝐺 ‘ 𝑢 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) )
37 36 breq1d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ↔ ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑣 ) ) )
38 35 37 imbi12d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑣 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) )
39 breq2 ⊢ ( 𝑣 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑣 ↔ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) )
40 fveq2 ⊢ ( 𝑣 = 𝑤 → ( 𝐺 ‘ 𝑣 ) = ( 𝐺 ‘ 𝑤 ) )
41 40 breq2d ⊢ ( 𝑣 = 𝑤 → ( ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑣 ) ↔ ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑤 ) ) )
42 39 41 imbi12d ⊢ ( 𝑣 = 𝑤 → ( ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑣 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑣 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑤 ) ) ) )
43 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
44 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
45 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 = ( 𝐹 ‘ 𝑧 ) ) → 𝐵 = 𝐵 )
46 38 42 44 45 23 rspc2vd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑤 ) ) ) )
47 34 46 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑤 ) ) )
48 47 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑤 ) )
49 1 3 prstr ⊢ ( ( 𝑉 ∈ Proset ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝐴 ) ∧ ( 𝑧 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∧ ( 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝐺 ‘ 𝑤 ) ) ) → 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) )
50 15 17 21 25 33 48 49 syl132anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ) → 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) )
51 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → 𝑊 ∈ Proset )
52 43 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
53 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
54 24 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝐴 )
55 53 54 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ 𝐵 )
56 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → 𝑤 ∈ 𝐵 )
57 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
58 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦 ) )
59 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
60 59 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
61 58 60 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑧 ≤ 𝑦 → ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) )
62 breq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( 𝑧 ≤ 𝑦 ↔ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) )
63 fveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) )
64 63 breq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) )
65 62 64 imbi12d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝑧 ≤ 𝑦 → ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ) )
66 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑥 = 𝑧 ) → 𝐴 = 𝐴 )
67 61 65 16 66 24 rspc2vd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) → ( 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ) )
68 57 67 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) )
69 68 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) )
70 13 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
71 70 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 )
72 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) ∧ 𝑢 = 𝑤 ) → 𝑢 = 𝑤 )
73 72 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) ∧ 𝑢 = 𝑤 ) → ( 𝐺 ‘ 𝑢 ) = ( 𝐺 ‘ 𝑤 ) )
74 73 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) ∧ 𝑢 = 𝑤 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) )
75 74 72 breq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) ∧ 𝑢 = 𝑤 ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ≲ 𝑤 ) )
76 56 75 rspcdv ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ≲ 𝑤 ) )
77 71 76 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ≲ 𝑤 )
78 2 4 prstr ⊢ ( ( 𝑊 ∈ Proset ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ≲ 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 )
79 51 52 55 56 69 77 78 syl132anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 )
80 50 79 impbida ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ↔ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) )
81 80 anasss ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ↔ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) )
82 81 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ↔ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) )
83 1 2 3 4 5 6 7 mgcval ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) ≲ 𝑤 ↔ 𝑧 ≤ ( 𝐺 ‘ 𝑤 ) ) ) ) )
84 14 82 83 mpbir2and ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )