Metamath Proof Explorer

Theorem wessf1ornlem

Description: Given a function F on a well-ordered domain A there exists a subset of A such that F restricted to such subset is injective and onto the range of F (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses wessf1ornlem.f 
|- ( ph -> F Fn A )
wessf1ornlem.a 
|- ( ph -> A e. V )
wessf1ornlem.r 
|- ( ph -> R We A )
wessf1ornlem.g 
|- G = ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) )
Assertion wessf1ornlem 
|- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )

Proof

Step Hyp Ref Expression
1 wessf1ornlem.f 
 |-  ( ph -> F Fn A )
2 wessf1ornlem.a 
 |-  ( ph -> A e. V )
3 wessf1ornlem.r 
 |-  ( ph -> R We A )
4 wessf1ornlem.g 
 |-  G = ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) )
5 cnvimass 
 |-  ( `' F " { u } ) C_ dom F
6 1 fndmd 
 |-  ( ph -> dom F = A )
7 6 adantr 
 |-  ( ( ph /\ u e. ran F ) -> dom F = A )
8 5 7 sseqtrid 
 |-  ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) C_ A )
9 3 adantr 
 |-  ( ( ph /\ u e. ran F ) -> R We A )
10 5 6 sseqtrid 
 |-  ( ph -> ( `' F " { u } ) C_ A )
11 2 10 ssexd 
 |-  ( ph -> ( `' F " { u } ) e. _V )
12 11 adantr 
 |-  ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) e. _V )
13 inisegn0 
 |-  ( u e. ran F <-> ( `' F " { u } ) =/= (/) )
14 13 bilani 
 |-  ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) =/= (/) )
15 wereu 
 |-  ( ( R We A /\ ( ( `' F " { u } ) e. _V /\ ( `' F " { u } ) C_ A /\ ( `' F " { u } ) =/= (/) ) ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
16 9 12 8 14 15 syl13anc 
 |-  ( ( ph /\ u e. ran F ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
17 riotacl 
 |-  ( E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. ( `' F " { u } ) )
18 16 17 syl 
 |-  ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. ( `' F " { u } ) )
19 8 18 sseldd 
 |-  ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A )
20 19 ralrimiva 
 |-  ( ph -> A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A )
21 sneq 
 |-  ( y = u -> { y } = { u } )
22 21 imaeq2d 
 |-  ( y = u -> ( `' F " { y } ) = ( `' F " { u } ) )
23 22 raleqdv 
 |-  ( y = u -> ( A. z e. ( `' F " { y } ) -. z R x <-> A. z e. ( `' F " { u } ) -. z R x ) )
24 22 23 riotaeqbidv 
 |-  ( y = u -> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) = ( iota_ x e. ( `' F " { u } ) A. z e. ( `' F " { u } ) -. z R x ) )
25 breq1 
 |-  ( z = t -> ( z R x <-> t R x ) )
26 25 notbid 
 |-  ( z = t -> ( -. z R x <-> -. t R x ) )
27 26 cbvralvw 
 |-  ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R x )
28 breq2 
 |-  ( x = v -> ( t R x <-> t R v ) )
29 28 notbid 
 |-  ( x = v -> ( -. t R x <-> -. t R v ) )
30 29 ralbidv 
 |-  ( x = v -> ( A. t e. ( `' F " { u } ) -. t R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
31 27 30 bitrid 
 |-  ( x = v -> ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
32 31 cbvriotavw 
 |-  ( iota_ x e. ( `' F " { u } ) A. z e. ( `' F " { u } ) -. z R x ) = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
33 24 32 eqtrdi 
 |-  ( y = u -> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
34 33 cbvmptv 
 |-  ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) ) = ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
35 4 34 eqtri 
 |-  G = ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
36 35 rnmptss 
 |-  ( A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A -> ran G C_ A )
37 20 36 syl 
 |-  ( ph -> ran G C_ A )
38 2 37 sselpwd 
 |-  ( ph -> ran G e. ~P A )
39 dffn3 
 |-  ( F Fn A <-> F : A --> ran F )
40 1 39 sylib 
 |-  ( ph -> F : A --> ran F )
41 40 37 fssresd 
 |-  ( ph -> ( F |` ran G ) : ran G --> ran F )
42 fvres 
 |-  ( w e. ran G -> ( ( F |` ran G ) ` w ) = ( F ` w ) )
43 42 eqcomd 
 |-  ( w e. ran G -> ( F ` w ) = ( ( F |` ran G ) ` w ) )
44 43 ad2antrr 
 |-  ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( ( F |` ran G ) ` w ) )
45 simpr 
 |-  ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) )
46 fvres 
 |-  ( t e. ran G -> ( ( F |` ran G ) ` t ) = ( F ` t ) )
47 46 ad2antlr 
 |-  ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( ( F |` ran G ) ` t ) = ( F ` t ) )
48 44 45 47 3eqtrd 
 |-  ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
49 48 3adantl1 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
50 simpl1 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ph )
51 simpl3 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. ran G )
52 simpl2 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. ran G )
53 id 
 |-  ( ( F ` w ) = ( F ` t ) -> ( F ` w ) = ( F ` t ) )
54 53 eqcomd 
 |-  ( ( F ` w ) = ( F ` t ) -> ( F ` t ) = ( F ` w ) )
55 54 adantl 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( F ` t ) = ( F ` w ) )
56 eleq1w 
 |-  ( b = w -> ( b e. ran G <-> w e. ran G ) )
57 56 3anbi3d 
 |-  ( b = w -> ( ( ph /\ t e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ w e. ran G ) ) )
58 fveq2 
 |-  ( b = w -> ( F ` b ) = ( F ` w ) )
59 58 eqeq2d 
 |-  ( b = w -> ( ( F ` t ) = ( F ` b ) <-> ( F ` t ) = ( F ` w ) ) )
60 57 59 anbi12d 
 |-  ( b = w -> ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) <-> ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) ) )
61 breq1 
 |-  ( b = w -> ( b R t <-> w R t ) )
62 61 notbid 
 |-  ( b = w -> ( -. b R t <-> -. w R t ) )
63 60 62 imbi12d 
 |-  ( b = w -> ( ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t ) <-> ( ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) -> -. w R t ) ) )
64 eleq1w 
 |-  ( a = t -> ( a e. ran G <-> t e. ran G ) )
65 64 3anbi2d 
 |-  ( a = t -> ( ( ph /\ a e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ b e. ran G ) ) )
66 fveqeq2 
 |-  ( a = t -> ( ( F ` a ) = ( F ` b ) <-> ( F ` t ) = ( F ` b ) ) )
67 65 66 anbi12d 
 |-  ( a = t -> ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) <-> ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) ) )
68 breq2 
 |-  ( a = t -> ( b R a <-> b R t ) )
69 68 notbid 
 |-  ( a = t -> ( -. b R a <-> -. b R t ) )
70 67 69 imbi12d 
 |-  ( a = t -> ( ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a ) <-> ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t ) ) )
71 eleq1w 
 |-  ( t = b -> ( t e. ran G <-> b e. ran G ) )
72 71 3anbi3d 
 |-  ( t = b -> ( ( ph /\ a e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ b e. ran G ) ) )
73 fveq2 
 |-  ( t = b -> ( F ` t ) = ( F ` b ) )
74 73 eqeq2d 
 |-  ( t = b -> ( ( F ` a ) = ( F ` t ) <-> ( F ` a ) = ( F ` b ) ) )
75 72 74 anbi12d 
 |-  ( t = b -> ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) <-> ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) ) )
76 breq1 
 |-  ( t = b -> ( t R a <-> b R a ) )
77 76 notbid 
 |-  ( t = b -> ( -. t R a <-> -. b R a ) )
78 75 77 imbi12d 
 |-  ( t = b -> ( ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a ) <-> ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a ) ) )
79 eleq1w 
 |-  ( w = a -> ( w e. ran G <-> a e. ran G ) )
80 79 3anbi2d 
 |-  ( w = a -> ( ( ph /\ w e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ t e. ran G ) ) )
81 fveqeq2 
 |-  ( w = a -> ( ( F ` w ) = ( F ` t ) <-> ( F ` a ) = ( F ` t ) ) )
82 80 81 anbi12d 
 |-  ( w = a -> ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) <-> ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) ) )
83 breq2 
 |-  ( w = a -> ( t R w <-> t R a ) )
84 83 notbid 
 |-  ( w = a -> ( -. t R w <-> -. t R a ) )
85 82 84 imbi12d 
 |-  ( w = a -> ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. t R w ) <-> ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a ) ) )
86 35 elrnmpt 
 |-  ( w e. _V -> ( w e. ran G <-> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) )
87 86 elv 
 |-  ( w e. ran G <-> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
88 87 birani 
 |-  ( ( w e. ran G /\ ( F ` w ) = ( F ` t ) ) -> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
89 88 3ad2antl2 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
90 simp3 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
91 90 eqcomd 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) = w )
92 simp11 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ph )
93 id 
 |-  ( w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
94 breq2 
 |-  ( v = w -> ( t R v <-> t R w ) )
95 94 notbid 
 |-  ( v = w -> ( -. t R v <-> -. t R w ) )
96 95 ralbidv 
 |-  ( v = w -> ( A. t e. ( `' F " { u } ) -. t R v <-> A. t e. ( `' F " { u } ) -. t R w ) )
97 96 cbvriotavw 
 |-  ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) = ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
98 93 97 eqtr2di 
 |-  ( w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w )
99 98 3ad2ant3 
 |-  ( ( ph /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w )
100 96 cbvreuvw 
 |-  ( E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v <-> E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
101 16 100 sylib 
 |-  ( ( ph /\ u e. ran F ) -> E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
102 riota1 
 |-  ( E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w -> ( ( w e. ( `' F " { u } ) /\ A. t e. ( `' F " { u } ) -. t R w ) <-> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w ) )
103 101 102 syl 
 |-  ( ( ph /\ u e. ran F ) -> ( ( w e. ( `' F " { u } ) /\ A. t e. ( `' F " { u } ) -. t R w ) <-> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w ) )
104 103 3adant3 
 |-  ( ( ph /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( ( w e. ( `' F " { u } ) /\ A. t e. ( `' F " { u } ) -. t R w ) <-> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w ) )
105 99 104 mpbird 
 |-  ( ( ph /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( w e. ( `' F " { u } ) /\ A. t e. ( `' F " { u } ) -. t R w ) )
106 105 simpld 
 |-  ( ( ph /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> w e. ( `' F " { u } ) )
107 92 106 syld3an1 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> w e. ( `' F " { u } ) )
108 simp2 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> u e. ran F )
109 92 108 16 syl2anc 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
110 96 riota2 
 |-  ( ( w e. ( `' F " { u } ) /\ E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> ( A. t e. ( `' F " { u } ) -. t R w <-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) = w ) )
111 107 109 110 syl2anc 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( A. t e. ( `' F " { u } ) -. t R w <-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) = w ) )
112 91 111 mpbird 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> A. t e. ( `' F " { u } ) -. t R w )
113 112 3adant1r 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> A. t e. ( `' F " { u } ) -. t R w )
114 37 sselda 
 |-  ( ( ph /\ t e. ran G ) -> t e. A )
115 114 3adant2 
 |-  ( ( ph /\ w e. ran G /\ t e. ran G ) -> t e. A )
116 115 adantr 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. A )
117 116 3ad2ant1 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> t e. A )
118 54 ad2antlr 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F ) -> ( F ` t ) = ( F ` w ) )
119 118 3adant3 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( F ` t ) = ( F ` w ) )
120 fniniseg 
 |-  ( F Fn A -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) )
121 92 1 120 3syl 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) )
122 107 121 mpbid 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( w e. A /\ ( F ` w ) = u ) )
123 122 simprd 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( F ` w ) = u )
124 123 3adant1r 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( F ` w ) = u )
125 119 124 eqtrd 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( F ` t ) = u )
126 fniniseg 
 |-  ( F Fn A -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
127 1 126 syl 
 |-  ( ph -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
128 127 3ad2ant1 
 |-  ( ( ph /\ w e. ran G /\ t e. ran G ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
129 128 ad2antrr 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
130 129 3adant3 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
131 117 125 130 mpbir2and 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> t e. ( `' F " { u } ) )
132 rspa 
 |-  ( ( A. t e. ( `' F " { u } ) -. t R w /\ t e. ( `' F " { u } ) ) -> -. t R w )
133 113 131 132 syl2anc 
 |-  ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> -. t R w )
134 133 rexlimdv3a 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> -. t R w ) )
135 89 134 mpd 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. t R w )
136 85 135 chvarvv 
 |-  ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a )
137 78 136 chvarvv 
 |-  ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a )
138 70 137 chvarvv 
 |-  ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t )
139 63 138 chvarvv 
 |-  ( ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) -> -. w R t )
140 50 51 52 55 139 syl31anc 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. w R t )
141 weso 
 |-  ( R We A -> R Or A )
142 3 141 syl 
 |-  ( ph -> R Or A )
143 142 adantr 
 |-  ( ( ph /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
144 143 3ad2antl1 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
145 37 sselda 
 |-  ( ( ph /\ w e. ran G ) -> w e. A )
146 145 3adant3 
 |-  ( ( ph /\ w e. ran G /\ t e. ran G ) -> w e. A )
147 146 adantr 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. A )
148 sotrieq2 
 |-  ( ( R Or A /\ ( w e. A /\ t e. A ) ) -> ( w = t <-> ( -. w R t /\ -. t R w ) ) )
149 144 147 116 148 syl12anc 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( w = t <-> ( -. w R t /\ -. t R w ) ) )
150 140 135 149 mpbir2and 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w = t )
151 49 150 syldan 
 |-  ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> w = t )
152 151 ex 
 |-  ( ( ph /\ w e. ran G /\ t e. ran G ) -> ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) )
153 152 3expb 
 |-  ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) )
154 153 ralrimivva 
 |-  ( ph -> A. w e. ran G A. t e. ran G ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) )
155 dff13 
 |-  ( ( F |` ran G ) : ran G -1-1-> ran F <-> ( ( F |` ran G ) : ran G --> ran F /\ A. w e. ran G A. t e. ran G ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) ) )
156 41 154 155 sylanbrc 
 |-  ( ph -> ( F |` ran G ) : ran G -1-1-> ran F )
157 riotaex 
 |-  ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V
158 157 rgenw 
 |-  A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V
159 35 fnmpt 
 |-  ( A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V -> G Fn ran F )
160 158 159 mp1i 
 |-  ( ph -> G Fn ran F )
161 dffn3 
 |-  ( G Fn ran F <-> G : ran F --> ran G )
162 160 161 sylib 
 |-  ( ph -> G : ran F --> ran G )
163 162 ffvelcdmda 
 |-  ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ran G )
164 163 fvresd 
 |-  ( ( ph /\ u e. ran F ) -> ( ( F |` ran G ) ` ( G ` u ) ) = ( F ` ( G ` u ) ) )
165 simpr 
 |-  ( ( ph /\ u e. ran F ) -> u e. ran F )
166 157 a1i 
 |-  ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V )
167 4 33 165 166 fvmptd3 
 |-  ( ( ph /\ u e. ran F ) -> ( G ` u ) = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
168 167 18 eqeltrd 
 |-  ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ( `' F " { u } ) )
169 fvex 
 |-  ( G ` u ) e. _V
170 eleq1 
 |-  ( w = ( G ` u ) -> ( w e. ( `' F " { u } ) <-> ( G ` u ) e. ( `' F " { u } ) ) )
171 eleq1 
 |-  ( w = ( G ` u ) -> ( w e. A <-> ( G ` u ) e. A ) )
172 fveqeq2 
 |-  ( w = ( G ` u ) -> ( ( F ` w ) = u <-> ( F ` ( G ` u ) ) = u ) )
173 171 172 anbi12d 
 |-  ( w = ( G ` u ) -> ( ( w e. A /\ ( F ` w ) = u ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
174 170 173 bibi12d 
 |-  ( w = ( G ` u ) -> ( ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) <-> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) ) )
175 174 imbi2d 
 |-  ( w = ( G ` u ) -> ( ( ph -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) ) <-> ( ph -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) ) ) )
176 1 120 syl 
 |-  ( ph -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) )
177 169 175 176 vtocl 
 |-  ( ph -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
178 177 adantr 
 |-  ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
179 168 178 mpbid 
 |-  ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) )
180 179 simprd 
 |-  ( ( ph /\ u e. ran F ) -> ( F ` ( G ` u ) ) = u )
181 164 180 eqtr2d 
 |-  ( ( ph /\ u e. ran F ) -> u = ( ( F |` ran G ) ` ( G ` u ) ) )
182 fveq2 
 |-  ( w = ( G ` u ) -> ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` ( G ` u ) ) )
183 182 rspceeqv 
 |-  ( ( ( G ` u ) e. ran G /\ u = ( ( F |` ran G ) ` ( G ` u ) ) ) -> E. w e. ran G u = ( ( F |` ran G ) ` w ) )
184 163 181 183 syl2anc 
 |-  ( ( ph /\ u e. ran F ) -> E. w e. ran G u = ( ( F |` ran G ) ` w ) )
185 184 ralrimiva 
 |-  ( ph -> A. u e. ran F E. w e. ran G u = ( ( F |` ran G ) ` w ) )
186 dffo3 
 |-  ( ( F |` ran G ) : ran G -onto-> ran F <-> ( ( F |` ran G ) : ran G --> ran F /\ A. u e. ran F E. w e. ran G u = ( ( F |` ran G ) ` w ) ) )
187 41 185 186 sylanbrc 
 |-  ( ph -> ( F |` ran G ) : ran G -onto-> ran F )
188 df-f1o 
 |-  ( ( F |` ran G ) : ran G -1-1-onto-> ran F <-> ( ( F |` ran G ) : ran G -1-1-> ran F /\ ( F |` ran G ) : ran G -onto-> ran F ) )
189 156 187 188 sylanbrc 
 |-  ( ph -> ( F |` ran G ) : ran G -1-1-onto-> ran F )
190 reseq2 
 |-  ( v = ran G -> ( F |` v ) = ( F |` ran G ) )
191 id 
 |-  ( v = ran G -> v = ran G )
192 eqidd 
 |-  ( v = ran G -> ran F = ran F )
193 190 191 192 f1oeq123d 
 |-  ( v = ran G -> ( ( F |` v ) : v -1-1-onto-> ran F <-> ( F |` ran G ) : ran G -1-1-onto-> ran F ) )
194 193 rspcev 
 |-  ( ( ran G e. ~P A /\ ( F |` ran G ) : ran G -1-1-onto-> ran F ) -> E. v e. ~P A ( F |` v ) : v -1-1-onto-> ran F )
195 38 189 194 syl2anc 
 |-  ( ph -> E. v e. ~P A ( F |` v ) : v -1-1-onto-> ran F )
196 reseq2 
 |-  ( v = x -> ( F |` v ) = ( F |` x ) )
197 id 
 |-  ( v = x -> v = x )
198 eqidd 
 |-  ( v = x -> ran F = ran F )
199 196 197 198 f1oeq123d 
 |-  ( v = x -> ( ( F |` v ) : v -1-1-onto-> ran F <-> ( F |` x ) : x -1-1-onto-> ran F ) )
200 199 cbvrexvw 
 |-  ( E. v e. ~P A ( F |` v ) : v -1-1-onto-> ran F <-> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )
201 195 200 sylib 
 |-  ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )