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