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 
|- H = ( V MGalConn W )
mgcf1o.a 
|- A = ( Base ` V )
mgcf1o.b 
|- B = ( Base ` W )
mgcf1o.1 
|- .<_ = ( le ` V )
mgcf1o.2 
|- .c_ = ( le ` W )
mgcf1o.v 
|- ( ph -> V e. Poset )
mgcf1o.w 
|- ( ph -> W e. Poset )
mgcf1o.f 
|- ( ph -> F H G )
Assertion mgcf1o 
|- ( ph -> ( F |` ran G ) Isom .<_ , .c_ ( ran G , ran F ) )

Proof

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