Metamath Proof Explorer

Theorem mgcf1o

Description: Given a Galois connection, exhibit an order isomorphism. (Contributed by Thierry Arnoux, 26-Jul-2024)

Ref Expression
Hypotheses mgcf1o.h ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
mgcf1o.a ⊢ 𝐴 = ( Base ‘ 𝑉 )
mgcf1o.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
mgcf1o.1 ⊢ ≤ = ( le ‘ 𝑉 )
mgcf1o.2 ⊢ ≲ = ( le ‘ 𝑊 )
mgcf1o.v ⊢ ( 𝜑 → 𝑉 ∈ Poset )
mgcf1o.w ⊢ ( 𝜑 → 𝑊 ∈ Poset )
mgcf1o.f ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
Assertion mgcf1o ( 𝜑 → ( 𝐹 ↾ ran 𝐺 ) Isom ≤ , ≲ ( ran 𝐺 , ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 mgcf1o.h ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
2 mgcf1o.a ⊢ 𝐴 = ( Base ‘ 𝑉 )
3 mgcf1o.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
4 mgcf1o.1 ⊢ ≤ = ( le ‘ 𝑉 )
5 mgcf1o.2 ⊢ ≲ = ( le ‘ 𝑊 )
6 mgcf1o.v ⊢ ( 𝜑 → 𝑉 ∈ Poset )
7 mgcf1o.w ⊢ ( 𝜑 → 𝑊 ∈ Poset )
8 mgcf1o.f ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
9 eqid ⊢ ( 𝑥 ∈ ran 𝐺 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ran 𝐺 ↦ ( 𝐹 ‘ 𝑥 ) )
10 posprs ⊢ ( 𝑉 ∈ Poset → 𝑉 ∈ Proset )
11 6 10 syl ⊢ ( 𝜑 → 𝑉 ∈ Proset )
12 posprs ⊢ ( 𝑊 ∈ Poset → 𝑊 ∈ Proset )
13 7 12 syl ⊢ ( 𝜑 → 𝑊 ∈ Proset )
14 2 3 4 5 1 11 13 dfmgc2 ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) ) )
15 8 14 mpbid ⊢ ( 𝜑 → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
16 15 simplld ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
17 16 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
18 15 simplrd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
19 18 frnd ⊢ ( 𝜑 → ran 𝐺 ⊆ 𝐴 )
20 19 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) → 𝑥 ∈ 𝐴 )
21 fnfvelrn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
22 17 20 21 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
23 18 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
24 16 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
25 24 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → 𝑢 ∈ 𝐵 )
26 fnfvelrn ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑢 ) ∈ ran 𝐺 )
27 23 25 26 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( 𝐺 ‘ 𝑢 ) ∈ ran 𝐺 )
28 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → 𝑉 ∈ Poset )
29 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → 𝑊 ∈ Poset )
30 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → 𝐹 𝐻 𝐺 )
31 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → 𝑦 ∈ 𝐴 )
32 1 2 3 4 5 28 29 30 31 mgcf1olem1 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
33 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → ( 𝐹 ‘ 𝑦 ) = 𝑢 )
34 33 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑦 ) ) = ( 𝐺 ‘ 𝑢 ) )
35 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → 𝑥 = ( 𝐺 ‘ 𝑢 ) )
36 34 35 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑦 ) ) = 𝑥 )
37 36 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
38 32 37 33 3eqtr3rd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑢 ) → 𝑢 = ( 𝐹 ‘ 𝑥 ) )
39 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) → 𝐹 Fn 𝐴 )
40 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) → 𝑢 ∈ ran 𝐹 )
41 fvelrnb ⊢ ( 𝐹 Fn 𝐴 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = 𝑢 ) )
42 41 biimpa ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑢 ∈ ran 𝐹 ) → ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = 𝑢 )
43 39 40 42 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) → ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = 𝑢 )
44 38 43 r19.29a ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑥 = ( 𝐺 ‘ 𝑢 ) ) → 𝑢 = ( 𝐹 ‘ 𝑥 ) )
45 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → 𝑉 ∈ Poset )
46 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → 𝑊 ∈ Poset )
47 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → 𝐹 𝐻 𝐺 )
48 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → 𝑣 ∈ 𝐵 )
49 1 2 3 4 5 45 46 47 48 mgcf1olem2 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑣 ) ) ) = ( 𝐺 ‘ 𝑣 ) )
50 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → ( 𝐺 ‘ 𝑣 ) = 𝑥 )
51 50 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑣 ) ) = ( 𝐹 ‘ 𝑥 ) )
52 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → 𝑢 = ( 𝐹 ‘ 𝑥 ) )
53 51 52 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑣 ) ) = 𝑢 )
54 53 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑣 ) ) ) = ( 𝐺 ‘ 𝑢 ) )
55 49 54 50 3eqtr3rd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑥 ) → 𝑥 = ( 𝐺 ‘ 𝑢 ) )
56 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) → 𝐺 Fn 𝐵 )
57 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) → 𝑥 ∈ ran 𝐺 )
58 fvelrnb ⊢ ( 𝐺 Fn 𝐵 → ( 𝑥 ∈ ran 𝐺 ↔ ∃ 𝑣 ∈ 𝐵 ( 𝐺 ‘ 𝑣 ) = 𝑥 ) )
59 58 biimpa ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺 ) → ∃ 𝑣 ∈ 𝐵 ( 𝐺 ‘ 𝑣 ) = 𝑥 )
60 56 57 59 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑣 ∈ 𝐵 ( 𝐺 ‘ 𝑣 ) = 𝑥 )
61 55 60 r19.29a ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) ∧ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) → 𝑥 = ( 𝐺 ‘ 𝑢 ) )
62 44 61 impbida ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑢 ∈ ran 𝐹 ) ) → ( 𝑥 = ( 𝐺 ‘ 𝑢 ) ↔ 𝑢 = ( 𝐹 ‘ 𝑥 ) ) )
63 9 22 27 62 f1o2d ⊢ ( 𝜑 → ( 𝑥 ∈ ran 𝐺 ↦ ( 𝐹 ‘ 𝑥 ) ) : ran 𝐺 –1-1-onto→ ran 𝐹 )
64 16 19 feqresmpt ⊢ ( 𝜑 → ( 𝐹 ↾ ran 𝐺 ) = ( 𝑥 ∈ ran 𝐺 ↦ ( 𝐹 ‘ 𝑥 ) ) )
65 64 f1oeq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1-onto→ ran 𝐹 ↔ ( 𝑥 ∈ ran 𝐺 ↦ ( 𝐹 ‘ 𝑥 ) ) : ran 𝐺 –1-1-onto→ ran 𝐹 ) )
66 63 65 mpbird ⊢ ( 𝜑 → ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1-onto→ ran 𝐹 )
67 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ 𝑥 ≤ 𝑦 ) → 𝜑 )
68 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) → ran 𝐺 ⊆ 𝐴 )
69 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) → 𝑥 ∈ ran 𝐺 )
70 68 69 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) → 𝑥 ∈ 𝐴 )
71 70 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ∈ 𝐴 )
72 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) → 𝑦 ∈ ran 𝐺 )
73 68 72 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) → 𝑦 ∈ 𝐴 )
74 73 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑦 ∈ 𝐴 )
75 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ≤ 𝑦 )
76 15 simprld ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ≲ 𝑣 → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) ) ) )
77 76 simpld ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
78 77 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
79 78 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
80 79 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) )
81 67 71 74 75 80 syl1111anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) )
82 69 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
83 82 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ 𝑥 ≤ 𝑦 ) → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
84 72 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
85 84 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ 𝑥 ≤ 𝑦 ) → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
86 81 83 85 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ 𝑥 ≤ 𝑦 ) → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) ≲ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) )
87 82 84 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) → ( ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) ≲ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
88 87 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) ≲ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) )
89 7 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → 𝑊 ∈ Poset )
90 6 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → 𝑉 ∈ Poset )
91 1 11 13 8 mgcmnt2d ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑊 Monot 𝑉 ) )
92 91 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → 𝐺 ∈ ( 𝑊 Monot 𝑉 ) )
93 16 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
94 18 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → 𝐺 : 𝐵 ⟶ 𝐴 )
95 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → 𝑢 ∈ 𝐵 )
96 94 95 ffvelcdmd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐺 ‘ 𝑢 ) ∈ 𝐴 )
97 93 96 ffvelcdmd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ∈ 𝐵 )
98 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → 𝑣 ∈ 𝐵 )
99 94 98 ffvelcdmd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐺 ‘ 𝑣 ) ∈ 𝐴 )
100 93 99 ffvelcdmd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑣 ) ) ∈ 𝐵 )
101 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) )
102 101 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) )
103 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐺 ‘ 𝑢 ) = 𝑥 )
104 103 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = ( 𝐹 ‘ 𝑥 ) )
105 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐺 ‘ 𝑣 ) = 𝑦 )
106 105 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑣 ) ) = ( 𝐹 ‘ 𝑦 ) )
107 102 104 106 3brtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ≲ ( 𝐹 ‘ ( 𝐺 ‘ 𝑣 ) ) )
108 3 2 5 4 89 90 92 97 100 107 ismntd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) ≤ ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
109 8 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → 𝐹 𝐻 𝐺 )
110 1 2 3 4 5 90 89 109 95 mgcf1olem2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) = ( 𝐺 ‘ 𝑢 ) )
111 1 2 3 4 5 90 89 109 98 mgcf1olem2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑣 ) ) ) = ( 𝐺 ‘ 𝑣 ) )
112 108 110 111 3brtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → ( 𝐺 ‘ 𝑢 ) ≤ ( 𝐺 ‘ 𝑣 ) )
113 112 103 105 3brtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑣 ) = 𝑦 ) → 𝑥 ≤ 𝑦 )
114 23 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) → 𝐺 Fn 𝐵 )
115 114 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) → 𝐺 Fn 𝐵 )
116 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) → 𝑦 ∈ ran 𝐺 )
117 fvelrnb ⊢ ( 𝐺 Fn 𝐵 → ( 𝑦 ∈ ran 𝐺 ↔ ∃ 𝑣 ∈ 𝐵 ( 𝐺 ‘ 𝑣 ) = 𝑦 ) )
118 117 biimpa ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑦 ∈ ran 𝐺 ) → ∃ 𝑣 ∈ 𝐵 ( 𝐺 ‘ 𝑣 ) = 𝑦 )
119 115 116 118 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) → ∃ 𝑣 ∈ 𝐵 ( 𝐺 ‘ 𝑣 ) = 𝑦 )
120 113 119 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑢 ) = 𝑥 ) → 𝑥 ≤ 𝑦 )
121 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ ran 𝐺 )
122 fvelrnb ⊢ ( 𝐺 Fn 𝐵 → ( 𝑥 ∈ ran 𝐺 ↔ ∃ 𝑢 ∈ 𝐵 ( 𝐺 ‘ 𝑢 ) = 𝑥 ) )
123 122 biimpa ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑥 ∈ ran 𝐺 ) → ∃ 𝑢 ∈ 𝐵 ( 𝐺 ‘ 𝑢 ) = 𝑥 )
124 114 121 123 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝐺 ‘ 𝑢 ) = 𝑥 )
125 120 124 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ≤ 𝑦 )
126 88 125 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) ≲ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) ) → 𝑥 ≤ 𝑦 )
127 86 126 impbida ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐺 ) → ( 𝑥 ≤ 𝑦 ↔ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) ≲ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) ) )
128 127 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( 𝑥 ≤ 𝑦 ↔ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) ≲ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) ) )
129 128 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( 𝑥 ≤ 𝑦 ↔ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) ≲ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) ) )
130 df-isom ⊢ ( ( 𝐹 ↾ ran 𝐺 ) Isom ≤ , ≲ ( ran 𝐺 , ran 𝐹 ) ↔ ( ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1-onto→ ran 𝐹 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( 𝑥 ≤ 𝑦 ↔ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑥 ) ≲ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑦 ) ) ) )
131 66 129 130 sylanbrc ⊢ ( 𝜑 → ( 𝐹 ↾ ran 𝐺 ) Isom ≤ , ≲ ( ran 𝐺 , ran 𝐹 ) )