Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wessf1ornlem Structured version   Visualization version   Unicode version

Theorem wessf1ornlem 37530
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.)
Hypotheses
Ref Expression
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
Ref Expression
wessf1ornlem  |-  ( ph  ->  E. x  e.  ~P  A ( F  |`  x ) : x -1-1-onto-> ran 
F )
Distinct variable groups:    x, A    x, F, y, z    x, R, y, z
Allowed substitution hints:    ph( x, y, z)    A( y, z)    G( x, y, z)    V( x, y, z)

Proof of Theorem wessf1ornlem
Dummy variables  t  u  v  w  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnvimass 5194 . . . . . . . . 9  |-  ( `' F " { u } )  C_  dom  F
21a1i 11 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( `' F " { u } )  C_  dom  F )
3 wessf1ornlem.f . . . . . . . . . 10  |-  ( ph  ->  F  Fn  A )
4 fndm 5685 . . . . . . . . . 10  |-  ( F  Fn  A  ->  dom  F  =  A )
53, 4syl 17 . . . . . . . . 9  |-  ( ph  ->  dom  F  =  A )
65adantr 472 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ran  F )  ->  dom  F  =  A )
72, 6sseqtrd 3454 . . . . . . 7  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( `' F " { u } )  C_  A
)
8 wessf1ornlem.r . . . . . . . . . 10  |-  ( ph  ->  R  We  A )
98adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  R  We  A )
101, 5syl5sseq 3466 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F " { u } ) 
C_  A )
11 wessf1ornlem.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  V )
12 ssexg 4542 . . . . . . . . . . 11  |-  ( ( ( `' F " { u } ) 
C_  A  /\  A  e.  V )  ->  ( `' F " { u } )  e.  _V )
1310, 11, 12syl2anc 673 . . . . . . . . . 10  |-  ( ph  ->  ( `' F " { u } )  e.  _V )
1413adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( `' F " { u } )  e.  _V )
15 inisegn0 5206 . . . . . . . . . . 11  |-  ( u  e.  ran  F  <->  ( `' F " { u }
)  =/=  (/) )
1615biimpi 199 . . . . . . . . . 10  |-  ( u  e.  ran  F  -> 
( `' F " { u } )  =/=  (/) )
1716adantl 473 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( `' F " { u } )  =/=  (/) )
18 wereu 4835 . . . . . . . . 9  |-  ( ( 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 )
199, 14, 7, 17, 18syl13anc 1294 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ran  F )  ->  E! v  e.  ( `' F " { u }
) A. t  e.  ( `' F " { u } )  -.  t R v )
20 riotacl 6284 . . . . . . . 8  |-  ( 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 } ) )
2119, 20syl 17 . . . . . . 7  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e.  ( `' F " { u } ) )
227, 21sseldd 3419 . . . . . 6  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e.  A )
2322ralrimiva 2809 . . . . 5  |-  ( ph  ->  A. u  e.  ran  F ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e.  A )
24 wessf1ornlem.g . . . . . . 7  |-  G  =  ( y  e.  ran  F 
|->  ( iota_ x  e.  ( `' F " { y } ) A. z  e.  ( `' F " { y } )  -.  z R x ) )
25 sneq 3969 . . . . . . . . . . 11  |-  ( y  =  u  ->  { y }  =  { u } )
2625imaeq2d 5174 . . . . . . . . . 10  |-  ( y  =  u  ->  ( `' F " { y } )  =  ( `' F " { u } ) )
2726raleqdv 2979 . . . . . . . . . 10  |-  ( y  =  u  ->  ( A. z  e.  ( `' F " { y } )  -.  z R x  <->  A. z  e.  ( `' F " { u } )  -.  z R x ) )
2826, 27riotaeqbidv 6273 . . . . . . . . 9  |-  ( 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 ) )
29 breq1 4398 . . . . . . . . . . . . . . 15  |-  ( z  =  t  ->  (
z R x  <->  t R x ) )
3029notbid 301 . . . . . . . . . . . . . 14  |-  ( z  =  t  ->  ( -.  z R x  <->  -.  t R x ) )
3130cbvralv 3005 . . . . . . . . . . . . 13  |-  ( A. z  e.  ( `' F " { u }
)  -.  z R x  <->  A. t  e.  ( `' F " { u } )  -.  t R x )
3231a1i 11 . . . . . . . . . . . 12  |-  ( x  =  v  ->  ( A. z  e.  ( `' F " { u } )  -.  z R x  <->  A. t  e.  ( `' F " { u } )  -.  t R x ) )
33 breq2 4399 . . . . . . . . . . . . . 14  |-  ( x  =  v  ->  (
t R x  <->  t R
v ) )
3433notbid 301 . . . . . . . . . . . . 13  |-  ( x  =  v  ->  ( -.  t R x  <->  -.  t R v ) )
3534ralbidv 2829 . . . . . . . . . . . 12  |-  ( x  =  v  ->  ( A. t  e.  ( `' F " { u } )  -.  t R x  <->  A. t  e.  ( `' F " { u } )  -.  t R v ) )
3632, 35bitrd 261 . . . . . . . . . . 11  |-  ( x  =  v  ->  ( A. z  e.  ( `' F " { u } )  -.  z R x  <->  A. t  e.  ( `' F " { u } )  -.  t R v ) )
3736cbvriotav 6281 . . . . . . . . . 10  |-  ( 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 )
3837a1i 11 . . . . . . . . 9  |-  ( y  =  u  ->  ( 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 ) )
3928, 38eqtrd 2505 . . . . . . . 8  |-  ( 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 ) )
4039cbvmptv 4488 . . . . . . 7  |-  ( 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 ) )
4124, 40eqtri 2493 . . . . . 6  |-  G  =  ( u  e.  ran  F 
|->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
4241rnmptss 6068 . . . . 5  |-  ( A. u  e.  ran  F (
iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e.  A  ->  ran  G  C_  A )
4323, 42syl 17 . . . 4  |-  ( ph  ->  ran  G  C_  A
)
4411, 43ssexd 4543 . . . . 5  |-  ( ph  ->  ran  G  e.  _V )
45 elpwg 3950 . . . . 5  |-  ( ran 
G  e.  _V  ->  ( ran  G  e.  ~P A 
<->  ran  G  C_  A
) )
4644, 45syl 17 . . . 4  |-  ( ph  ->  ( ran  G  e. 
~P A  <->  ran  G  C_  A ) )
4743, 46mpbird 240 . . 3  |-  ( ph  ->  ran  G  e.  ~P A )
48 dffn3 5748 . . . . . . . . . 10  |-  ( F  Fn  A  <->  F : A
--> ran  F )
4948biimpi 199 . . . . . . . . 9  |-  ( F  Fn  A  ->  F : A --> ran  F )
503, 49syl 17 . . . . . . . 8  |-  ( ph  ->  F : A --> ran  F
)
5150, 43fssresd 5762 . . . . . . 7  |-  ( ph  ->  ( F  |`  ran  G
) : ran  G --> ran  F )
52 simpl 464 . . . . . . . . 9  |-  ( (
ph  /\  ( w  e.  ran  G  /\  t  e.  ran  G ) )  ->  ph )
53 simprl 772 . . . . . . . . 9  |-  ( (
ph  /\  ( w  e.  ran  G  /\  t  e.  ran  G ) )  ->  w  e.  ran  G )
54 simprr 774 . . . . . . . . 9  |-  ( (
ph  /\  ( w  e.  ran  G  /\  t  e.  ran  G ) )  ->  t  e.  ran  G )
55 simpl 464 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `  w
)  =  ( ( F  |`  ran  G ) `
 t ) )  ->  ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G ) )
56 fvres 5893 . . . . . . . . . . . . . . 15  |-  ( w  e.  ran  G  -> 
( ( F  |`  ran  G ) `  w
)  =  ( F `
 w ) )
5756eqcomd 2477 . . . . . . . . . . . . . 14  |-  ( w  e.  ran  G  -> 
( F `  w
)  =  ( ( F  |`  ran  G ) `
 w ) )
5857ad2antrr 740 . . . . . . . . . . . . 13  |-  ( ( ( w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `
 w )  =  ( ( F  |`  ran  G ) `  t
) )  ->  ( F `  w )  =  ( ( F  |`  ran  G ) `  w ) )
59 simpr 468 . . . . . . . . . . . . 13  |-  ( ( ( w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `
 w )  =  ( ( F  |`  ran  G ) `  t
) )  ->  (
( F  |`  ran  G
) `  w )  =  ( ( F  |`  ran  G ) `  t ) )
60 fvres 5893 . . . . . . . . . . . . . 14  |-  ( t  e.  ran  G  -> 
( ( F  |`  ran  G ) `  t
)  =  ( F `
 t ) )
6160ad2antlr 741 . . . . . . . . . . . . 13  |-  ( ( ( w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `
 w )  =  ( ( F  |`  ran  G ) `  t
) )  ->  (
( F  |`  ran  G
) `  t )  =  ( F `  t ) )
6258, 59, 613eqtrd 2509 . . . . . . . . . . . 12  |-  ( ( ( w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `
 w )  =  ( ( F  |`  ran  G ) `  t
) )  ->  ( F `  w )  =  ( F `  t ) )
63623adantl1 1186 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `  w
)  =  ( ( F  |`  ran  G ) `
 t ) )  ->  ( F `  w )  =  ( F `  t ) )
64 simpl1 1033 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  ph )
65 simpl3 1035 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
t  e.  ran  G
)
66 vex 3034 . . . . . . . . . . . . . . . . . . 19  |-  w  e. 
_V
6741elrnmpt 5087 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) )
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ran  G  <->  E. u  e.  ran  F  w  =  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
6968biimpi 199 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  ran  G  ->  E. u  e.  ran  F  w  =  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
7069adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) )
71703ad2antl2 1193 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) )
7271, 68sylibr 217 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  w  e.  ran  G )
73 id 22 . . . . . . . . . . . . . . . 16  |-  ( ( F `  w )  =  ( F `  t )  ->  ( F `  w )  =  ( F `  t ) )
7473eqcomd 2477 . . . . . . . . . . . . . . 15  |-  ( ( F `  w )  =  ( F `  t )  ->  ( F `  t )  =  ( F `  w ) )
7574adantl 473 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
( F `  t
)  =  ( F `
 w ) )
76 eleq1 2537 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  w  ->  (
b  e.  ran  G  <->  w  e.  ran  G ) )
77763anbi3d 1371 . . . . . . . . . . . . . . . . 17  |-  ( b  =  w  ->  (
( ph  /\  t  e.  ran  G  /\  b  e.  ran  G )  <->  ( ph  /\  t  e.  ran  G  /\  w  e.  ran  G ) ) )
78 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  w  ->  ( F `  b )  =  ( F `  w ) )
7978eqeq2d 2481 . . . . . . . . . . . . . . . . 17  |-  ( b  =  w  ->  (
( F `  t
)  =  ( F `
 b )  <->  ( F `  t )  =  ( F `  w ) ) )
8077, 79anbi12d 725 . . . . . . . . . . . . . . . 16  |-  ( 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
) ) ) )
81 breq1 4398 . . . . . . . . . . . . . . . . 17  |-  ( b  =  w  ->  (
b R t  <->  w R
t ) )
8281notbid 301 . . . . . . . . . . . . . . . 16  |-  ( b  =  w  ->  ( -.  b R t  <->  -.  w R t ) )
8380, 82imbi12d 327 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) )
84 eleq1 2537 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  t  ->  (
a  e.  ran  G  <->  t  e.  ran  G ) )
85843anbi2d 1370 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  t  ->  (
( ph  /\  a  e.  ran  G  /\  b  e.  ran  G )  <->  ( ph  /\  t  e.  ran  G  /\  b  e.  ran  G ) ) )
86 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  t  ->  ( F `  a )  =  ( F `  t ) )
8786eqeq1d 2473 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  t  ->  (
( F `  a
)  =  ( F `
 b )  <->  ( F `  t )  =  ( F `  b ) ) )
8885, 87anbi12d 725 . . . . . . . . . . . . . . . . 17  |-  ( 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
) ) ) )
89 breq2 4399 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  t  ->  (
b R a  <->  b R
t ) )
9089notbid 301 . . . . . . . . . . . . . . . . 17  |-  ( a  =  t  ->  ( -.  b R a  <->  -.  b R t ) )
9188, 90imbi12d 327 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) )
92 eleq1 2537 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  b  ->  (
t  e.  ran  G  <->  b  e.  ran  G ) )
93923anbi3d 1371 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  b  ->  (
( ph  /\  a  e.  ran  G  /\  t  e.  ran  G )  <->  ( ph  /\  a  e.  ran  G  /\  b  e.  ran  G ) ) )
94 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  b  ->  ( F `  t )  =  ( F `  b ) )
9594eqeq2d 2481 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  b  ->  (
( F `  a
)  =  ( F `
 t )  <->  ( F `  a )  =  ( F `  b ) ) )
9693, 95anbi12d 725 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) ) ) )
97 breq1 4398 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  b  ->  (
t R a  <->  b R
a ) )
9897notbid 301 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  b  ->  ( -.  t R a  <->  -.  b R a ) )
9996, 98imbi12d 327 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
100 eleq1 2537 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  a  ->  (
w  e.  ran  G  <->  a  e.  ran  G ) )
1011003anbi2d 1370 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  a  ->  (
( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  <->  ( ph  /\  a  e.  ran  G  /\  t  e.  ran  G ) ) )
102 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  a  ->  ( F `  w )  =  ( F `  a ) )
103102eqeq1d 2473 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  a  ->  (
( F `  w
)  =  ( F `
 t )  <->  ( F `  a )  =  ( F `  t ) ) )
104101, 103anbi12d 725 . . . . . . . . . . . . . . . . . . 19  |-  ( 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
) ) ) )
105 breq2 4399 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  a  ->  (
t R w  <->  t R
a ) )
106105notbid 301 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  a  ->  ( -.  t R w  <->  -.  t R a ) )
107104, 106imbi12d 327 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) )
108 nfv 1769 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ u ph
109 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ u w
110 nfmpt1 4485 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ u
( u  e.  ran  F 
|->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
11141, 110nfcxfr 2610 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ u G
112111nfrn 5083 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ u ran  G
113109, 112nfel 2624 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ u  w  e.  ran  G
114112nfcri 2606 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ u  t  e.  ran  G
115108, 113, 114nf3an 2033 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ u
( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )
116 nfv 1769 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ u
( F `  w
)  =  ( F `
 t )
117115, 116nfan 2031 . . . . . . . . . . . . . . . . . . . 20  |-  F/ u
( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )
118 nfv 1769 . . . . . . . . . . . . . . . . . . . 20  |-  F/ u  -.  t R w
119 simp3 1032 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 ) )
120119eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 )
121 simp11 1060 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 )
122 simp2 1031 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 )
123 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) )
124 breq2 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( v  =  w  ->  (
t R v  <->  t R w ) )
125124notbid 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( v  =  w  ->  ( -.  t R v  <->  -.  t R w ) )
126125ralbidv 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( v  =  w  ->  ( A. t  e.  ( `' F " { u } )  -.  t R v  <->  A. t  e.  ( `' F " { u } )  -.  t R w ) )
127126cbvriotav 6281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 )
128127a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 )  =  ( iota_ w  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R w ) )
129123, 128eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 )
1301293ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
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 )
131126cbvreuv 3007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 )
13219, 131sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ran  F )  ->  E! w  e.  ( `' F " { u }
) A. t  e.  ( `' F " { u } )  -.  t R w )
133 riota1 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) )
134132, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
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 ) )
1351343adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
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 ) )
136130, 135mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
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 ) )
137136simpld 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ran  F  /\  w  =  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )  ->  w  e.  ( `' F " { u } ) )
138121, 122, 119, 137syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 } ) )
139121, 122, 19syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 )
140126riota2 6292 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 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 ) )
141138, 139, 140syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) )
142120, 141mpbird 240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 )
1431423adant1r 1285 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 )
14443sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  t  e.  ran  G )  ->  t  e.  A )
1451443adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  w  e.  ran  G  /\  t  e. 
ran  G )  -> 
t  e.  A )
146145adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
t  e.  A )
1471463ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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
)
14874ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  /\  u  e. 
ran  F )  -> 
( F `  t
)  =  ( F `
 w ) )
1491483adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) )
150 fniniseg 6018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( F  Fn  A  ->  (
w  e.  ( `' F " { u } )  <->  ( w  e.  A  /\  ( F `  w )  =  u ) ) )
151121, 3, 1503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 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 ) ) )
152138, 151mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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 ) )
153152simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 )
1541533adant1r 1285 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 )
155149, 154eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
156147, 155jca 541 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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  /\  ( F `
 t )  =  u ) )
157 fniniseg 6018 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F  Fn  A  ->  (
t  e.  ( `' F " { u } )  <->  ( t  e.  A  /\  ( F `  t )  =  u ) ) )
1583, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( t  e.  ( `' F " { u } )  <->  ( t  e.  A  /\  ( F `  t )  =  u ) ) )
1591583ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  w  e.  ran  G  /\  t  e. 
ran  G )  -> 
( t  e.  ( `' F " { u } )  <->  ( t  e.  A  /\  ( F `  t )  =  u ) ) )
160159ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 ) ) )
1611603adant3 1050 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) ) )
162156, 161mpbird 240 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 } ) )
163 rspa 2774 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A. t  e.  ( `' F " { u } )  -.  t R w  /\  t  e.  ( `' F " { u } ) )  ->  -.  t R w )
164143, 162, 163syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
1651643exp 1230 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )
166117, 118, 165rexlimd 2866 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) )
16771, 166mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  -.  t R w )
168107, 167chvarv 2120 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  a  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  a )  =  ( F `  t ) )  ->  -.  t R a )
16999, 168chvarv 2120 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  a  e.  ran  G  /\  b  e.  ran  G )  /\  ( F `  a )  =  ( F `  b ) )  ->  -.  b R a )
17091, 169chvarv 2120 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  ran  G  /\  b  e.  ran  G )  /\  ( F `  t )  =  ( F `  b ) )  ->  -.  b R t )
17183, 170chvarv 2120 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  ran  G  /\  w  e.  ran  G )  /\  ( F `  t )  =  ( F `  w ) )  ->  -.  w R t )
17264, 65, 72, 75, 171syl31anc 1295 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  -.  w R t )
173172, 167jca 541 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
( -.  w R t  /\  -.  t R w ) )
174 weso 4830 . . . . . . . . . . . . . . . 16  |-  ( R  We  A  ->  R  Or  A )
1758, 174syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  R  Or  A )
176175adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( F `  w )  =  ( F `  t ) )  ->  R  Or  A )
1771763ad2antl1 1192 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  R  Or  A )
17843sselda 3418 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w  e.  ran  G )  ->  w  e.  A )
1791783adant3 1050 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w  e.  ran  G  /\  t  e. 
ran  G )  ->  w  e.  A )
180179adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  w  e.  A )
181 sotrieq2 4788 . . . . . . . . . . . . 13  |-  ( ( R  Or  A  /\  ( w  e.  A  /\  t  e.  A
) )  ->  (
w  =  t  <->  ( -.  w R t  /\  -.  t R w ) ) )
182177, 180, 146, 181syl12anc 1290 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
( w  =  t  <-> 
( -.  w R t  /\  -.  t R w ) ) )
183173, 182mpbird 240 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  w  =  t )
18455, 63, 183syl2anc 673 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `  w
)  =  ( ( F  |`  ran  G ) `
 t ) )  ->  w  =  t )
185184ex 441 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ran  G  /\  t  e. 
ran  G )  -> 
( ( ( F  |`  ran  G ) `  w )  =  ( ( F  |`  ran  G
) `  t )  ->  w  =  t ) )
18652, 53, 54, 185syl3anc 1292 . . . . . . . 8  |-  ( (
ph  /\  ( w  e.  ran  G  /\  t  e.  ran  G ) )  ->  ( ( ( F  |`  ran  G ) `
 w )  =  ( ( F  |`  ran  G ) `  t
)  ->  w  =  t ) )
187186ralrimivva 2814 . . . . . . 7  |-  ( ph  ->  A. w  e.  ran  G A. t  e.  ran  G ( ( ( F  |`  ran  G ) `  w )  =  ( ( F  |`  ran  G
) `  t )  ->  w  =  t ) )
18851, 187jca 541 . . . . . 6  |-  ( ph  ->  ( ( 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 )
) )
189 dff13 6177 . . . . . 6  |-  ( ( 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 )
) )
190188, 189sylibr 217 . . . . 5  |-  ( ph  ->  ( F  |`  ran  G
) : ran  G -1-1-> ran 
F )
191 riotaex 6274 . . . . . . . . . . . . . 14  |-  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e. 
_V
192191rgenw 2768 . . . . . . . . . . . . 13  |-  A. u  e.  ran  F ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e. 
_V
193192a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  A. u  e.  ran  F ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e.  _V )
19441fnmpt 5714 . . . . . . . . . . . 12  |-  ( A. u  e.  ran  F (
iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e.  _V  ->  G  Fn  ran  F )
195193, 194syl 17 . . . . . . . . . . 11  |-  ( ph  ->  G  Fn  ran  F
)
196 dffn3 5748 . . . . . . . . . . . 12  |-  ( G  Fn  ran  F  <->  G : ran  F --> ran  G )
197196biimpi 199 . . . . . . . . . . 11  |-  ( G  Fn  ran  F  ->  G : ran  F --> ran  G
)
198195, 197syl 17 . . . . . . . . . 10  |-  ( ph  ->  G : ran  F --> ran  G )
199198ffvelrnda 6037 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( G `  u )  e.  ran  G )
200 fvres 5893 . . . . . . . . . . 11  |-  ( ( G `  u )  e.  ran  G  -> 
( ( F  |`  ran  G ) `  ( G `  u )
)  =  ( F `
 ( G `  u ) ) )
201199, 200syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ran  F )  ->  (
( F  |`  ran  G
) `  ( G `  u ) )  =  ( F `  ( G `  u )
) )
20217, 15sylibr 217 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ran  F )  ->  u  e.  ran  F )
203191a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e.  _V )
20441fvmpt2 5972 . . . . . . . . . . . . . 14  |-  ( ( u  e.  ran  F  /\  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e.  _V )  ->  ( G `  u
)  =  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
205202, 203, 204syl2anc 673 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( G `  u )  =  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
206205, 21eqeltrd 2549 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( G `  u )  e.  ( `' F " { u } ) )
207 fvex 5889 . . . . . . . . . . . . . 14  |-  ( G `
 u )  e. 
_V
208 eleq1 2537 . . . . . . . . . . . . . . . 16  |-  ( w  =  ( G `  u )  ->  (
w  e.  ( `' F " { u } )  <->  ( G `  u )  e.  ( `' F " { u } ) ) )
209 eleq1 2537 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( G `  u )  ->  (
w  e.  A  <->  ( G `  u )  e.  A
) )
210 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  ( G `  u )  ->  ( F `  w )  =  ( F `  ( G `  u ) ) )
211210eqeq1d 2473 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( G `  u )  ->  (
( F `  w
)  =  u  <->  ( F `  ( G `  u
) )  =  u ) )
212209, 211anbi12d 725 . . . . . . . . . . . . . . . 16  |-  ( w  =  ( G `  u )  ->  (
( w  e.  A  /\  ( F `  w
)  =  u )  <-> 
( ( G `  u )  e.  A  /\  ( F `  ( G `  u )
)  =  u ) ) )
213208, 212bibi12d 328 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) )
214213imbi2d 323 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) )
2153, 150syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( w  e.  ( `' F " { u } )  <->  ( w  e.  A  /\  ( F `  w )  =  u ) ) )
216207, 214, 215vtocl 3086 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( G `  u )  e.  ( `' F " { u } )  <->  ( ( G `  u )  e.  A  /\  ( F `  ( G `  u ) )  =  u ) ) )
217216adantr 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ran  F )  ->  (
( G `  u
)  e.  ( `' F " { u } )  <->  ( ( G `  u )  e.  A  /\  ( F `  ( G `  u ) )  =  u ) ) )
218206, 217mpbid 215 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ran  F )  ->  (
( G `  u
)  e.  A  /\  ( F `  ( G `
 u ) )  =  u ) )
219218simprd 470 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( F `  ( G `  u ) )  =  u )
220201, 219eqtr2d 2506 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  u  =  ( ( F  |`  ran  G ) `  ( G `  u ) ) )
221 fveq2 5879 . . . . . . . . . . 11  |-  ( w  =  ( G `  u )  ->  (
( F  |`  ran  G
) `  w )  =  ( ( F  |`  ran  G ) `  ( G `  u ) ) )
222221eqeq2d 2481 . . . . . . . . . 10  |-  ( w  =  ( G `  u )  ->  (
u  =  ( ( F  |`  ran  G ) `
 w )  <->  u  =  ( ( F  |`  ran  G ) `  ( G `  u )
) ) )
223222rspcev 3136 . . . . . . . . 9  |-  ( ( ( G `  u
)  e.  ran  G  /\  u  =  (
( F  |`  ran  G
) `  ( G `  u ) ) )  ->  E. w  e.  ran  G  u  =  ( ( F  |`  ran  G ) `
 w ) )
224199, 220, 223syl2anc 673 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ran  F )  ->  E. w  e.  ran  G  u  =  ( ( F  |`  ran  G ) `  w
) )
225224ralrimiva 2809 . . . . . . 7  |-  ( ph  ->  A. u  e.  ran  F E. w  e.  ran  G  u  =  ( ( F  |`  ran  G ) `
 w ) )
22651, 225jca 541 . . . . . 6  |-  ( ph  ->  ( ( F  |`  ran  G ) : ran  G --> ran  F  /\  A. u  e.  ran  F E. w  e.  ran  G  u  =  ( ( F  |`  ran  G ) `  w ) ) )
227 dffo3 6052 . . . . . 6  |-  ( ( 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 ) ) )
228226, 227sylibr 217 . . . . 5  |-  ( ph  ->  ( F  |`  ran  G
) : ran  G -onto-> ran  F )
229190, 228jca 541 . . . 4  |-  ( ph  ->  ( ( F  |`  ran  G ) : ran  G
-1-1-> ran  F  /\  ( F  |`  ran  G ) : ran  G -onto-> ran  F ) )
230 df-f1o 5596 . . . 4  |-  ( ( 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
) )
231229, 230sylibr 217 . . 3  |-  ( ph  ->  ( F  |`  ran  G
) : ran  G -1-1-onto-> ran  F )
232 nfcv 2612 . . . . . 6  |-  F/_ v F
233 nfcv 2612 . . . . . . . . 9  |-  F/_ v ran  F
234 nfriota1 6277 . . . . . . . . 9  |-  F/_ v
( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )
235233, 234nfmpt 4484 . . . . . . . 8  |-  F/_ v
( u  e.  ran  F 
|->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
23641, 235nfcxfr 2610 . . . . . . 7  |-  F/_ v G
237236nfrn 5083 . . . . . 6  |-  F/_ v ran  G
238232, 237nfres 5113 . . . . 5  |-  F/_ v
( F  |`  ran  G
)
239238, 237, 233nff1o 5826 . . . 4  |-  F/ v ( F  |`  ran  G
) : ran  G -1-1-onto-> ran  F
240 reseq2 5106 . . . . 5  |-  ( v  =  ran  G  -> 
( F  |`  v
)  =  ( F  |`  ran  G ) )
241 id 22 . . . . 5  |-  ( v  =  ran  G  -> 
v  =  ran  G
)
242 eqidd 2472 . . . . 5  |-  ( v  =  ran  G  ->  ran  F  =  ran  F
)
243240, 241, 242f1oeq123d 5824 . . . 4  |-  ( v  =  ran  G  -> 
( ( F  |`  v ) : v -1-1-onto-> ran 
F  <->  ( F  |`  ran  G ) : ran  G -1-1-onto-> ran 
F ) )
244239, 243rspce 3131 . . 3  |-  ( ( 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 )
24547, 231, 244syl2anc 673 . 2  |-  ( ph  ->  E. v  e.  ~P  A ( F  |`  v ) : v -1-1-onto-> ran 
F )
246 reseq2 5106 . . . 4  |-  ( v  =  x  ->  ( F  |`  v )  =  ( F  |`  x
) )
247 id 22 . . . 4  |-  ( v  =  x  ->  v  =  x )
248 eqidd 2472 . . . 4  |-  ( v  =  x  ->  ran  F  =  ran  F )
249246, 247, 248f1oeq123d 5824 . . 3  |-  ( v  =  x  ->  (
( F  |`  v
) : v -1-1-onto-> ran  F  <->  ( F  |`  x ) : x -1-1-onto-> ran  F ) )
250249cbvrexv 3006 . 2  |-  ( 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
)
251245, 250sylib 201 1  |-  ( ph  ->  E. x  e.  ~P  A ( F  |`  x ) : x -1-1-onto-> ran 
F )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904    =/= wne 2641   A.wral 2756   E.wrex 2757   E!wreu 2758   _Vcvv 3031    C_ wss 3390   (/)c0 3722   ~Pcpw 3942   {csn 3959   class class class wbr 4395    |-> cmpt 4454    Or wor 4759    We wwe 4797   `'ccnv 4838   dom cdm 4839   ran crn 4840    |` cres 4841   "cima 4842    Fn wfn 5584   -->wf 5585   -1-1->wf1 5586   -onto->wfo 5587   -1-1-onto->wf1o 5588   ` cfv 5589   iota_crio 6269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270
This theorem is referenced by:  wessf1orn  37531
  Copyright terms: Public domain W3C validator