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

Theorem wessf1ornlem 37297
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 5200 . . . . . . . . 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 466 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ran  F )  ->  dom  F  =  A )
72, 6sseqtrd 3497 . . . . . . 7  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( `' F " { u } )  C_  A
)
8 wessf1ornlem.r . . . . . . . . . 10  |-  ( ph  ->  R  We  A )
98adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  R  We  A )
101, 5syl5sseq 3509 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F " { u } ) 
C_  A )
11 wessf1ornlem.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  V )
12 ssexg 4563 . . . . . . . . . . 11  |-  ( ( ( `' F " { u } ) 
C_  A  /\  A  e.  V )  ->  ( `' F " { u } )  e.  _V )
1310, 11, 12syl2anc 665 . . . . . . . . . 10  |-  ( ph  ->  ( `' F " { u } )  e.  _V )
1413adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( `' F " { u } )  e.  _V )
15 inisegn0 5212 . . . . . . . . . . 11  |-  ( u  e.  ran  F  <->  ( `' F " { u }
)  =/=  (/) )
1615biimpi 197 . . . . . . . . . 10  |-  ( u  e.  ran  F  -> 
( `' F " { u } )  =/=  (/) )
1716adantl 467 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( `' F " { u } )  =/=  (/) )
18 wereu 4842 . . . . . . . . 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 1266 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ran  F )  ->  E! v  e.  ( `' F " { u }
) A. t  e.  ( `' F " { u } )  -.  t R v )
20 riotacl 6273 . . . . . . . 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 3462 . . . . . 6  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e.  A )
2322ralrimiva 2837 . . . . 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 4003 . . . . . . . . . . 11  |-  ( y  =  u  ->  { y }  =  { u } )
2625imaeq2d 5180 . . . . . . . . . 10  |-  ( y  =  u  ->  ( `' F " { y } )  =  ( `' F " { u } ) )
2726raleqdv 3029 . . . . . . . . . 10  |-  ( y  =  u  ->  ( A. z  e.  ( `' F " { y } )  -.  z R x  <->  A. z  e.  ( `' F " { u } )  -.  z R x ) )
2826, 27riotaeqbidv 6262 . . . . . . . . 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 4420 . . . . . . . . . . . . . . 15  |-  ( z  =  t  ->  (
z R x  <->  t R x ) )
3029notbid 295 . . . . . . . . . . . . . 14  |-  ( z  =  t  ->  ( -.  z R x  <->  -.  t R x ) )
3130cbvralv 3053 . . . . . . . . . . . . 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 4421 . . . . . . . . . . . . . 14  |-  ( x  =  v  ->  (
t R x  <->  t R
v ) )
3433notbid 295 . . . . . . . . . . . . 13  |-  ( x  =  v  ->  ( -.  t R x  <->  -.  t R v ) )
3534ralbidv 2862 . . . . . . . . . . . 12  |-  ( x  =  v  ->  ( A. t  e.  ( `' F " { u } )  -.  t R x  <->  A. t  e.  ( `' F " { u } )  -.  t R v ) )
3632, 35bitrd 256 . . . . . . . . . . 11  |-  ( x  =  v  ->  ( A. z  e.  ( `' F " { u } )  -.  z R x  <->  A. t  e.  ( `' F " { u } )  -.  t R v ) )
3736cbvriotav 6270 . . . . . . . . . 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 2461 . . . . . . . 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 4510 . . . . . . 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 2449 . . . . . 6  |-  G  =  ( u  e.  ran  F 
|->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
4241rnmptss 6059 . . . . 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 4564 . . . . 5  |-  ( ph  ->  ran  G  e.  _V )
45 elpwg 3984 . . . . 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 235 . . 3  |-  ( ph  ->  ran  G  e.  ~P A )
48 dffn3 5745 . . . . . . . . . 10  |-  ( F  Fn  A  <->  F : A
--> ran  F )
4948biimpi 197 . . . . . . . . 9  |-  ( F  Fn  A  ->  F : A --> ran  F )
503, 49syl 17 . . . . . . . 8  |-  ( ph  ->  F : A --> ran  F
)
5150, 43fssresd 5759 . . . . . . 7  |-  ( ph  ->  ( F  |`  ran  G
) : ran  G --> ran  F )
52 simpl 458 . . . . . . . . 9  |-  ( (
ph  /\  ( w  e.  ran  G  /\  t  e.  ran  G ) )  ->  ph )
53 simprl 762 . . . . . . . . 9  |-  ( (
ph  /\  ( w  e.  ran  G  /\  t  e.  ran  G ) )  ->  w  e.  ran  G )
54 simprr 764 . . . . . . . . 9  |-  ( (
ph  /\  ( w  e.  ran  G  /\  t  e.  ran  G ) )  ->  t  e.  ran  G )
55 simpl 458 . . . . . . . . . . 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 5887 . . . . . . . . . . . . . . 15  |-  ( w  e.  ran  G  -> 
( ( F  |`  ran  G ) `  w
)  =  ( F `
 w ) )
5756eqcomd 2428 . . . . . . . . . . . . . 14  |-  ( w  e.  ran  G  -> 
( F `  w
)  =  ( ( F  |`  ran  G ) `
 w ) )
5857ad2antrr 730 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 5887 . . . . . . . . . . . . . 14  |-  ( t  e.  ran  G  -> 
( ( F  |`  ran  G ) `  t
)  =  ( F `
 t ) )
6160ad2antlr 731 . . . . . . . . . . . . 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 2465 . . . . . . . . . . . 12  |-  ( ( ( w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `
 w )  =  ( ( F  |`  ran  G ) `  t
) )  ->  ( F `  w )  =  ( F `  t ) )
63623adantl1 1161 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `  w
)  =  ( ( F  |`  ran  G ) `
 t ) )  ->  ( F `  w )  =  ( F `  t ) )
64 simpl1 1008 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  ph )
65 simpl3 1010 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
t  e.  ran  G
)
66 vex 3081 . . . . . . . . . . . . . . . . . . 19  |-  w  e. 
_V
6741elrnmpt 5093 . . . . . . . . . . . . . . . . . . 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 197 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . 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 1168 . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  w  e.  ran  G )
73 id 23 . . . . . . . . . . . . . . . 16  |-  ( ( F `  w )  =  ( F `  t )  ->  ( F `  w )  =  ( F `  t ) )
7473eqcomd 2428 . . . . . . . . . . . . . . 15  |-  ( ( F `  w )  =  ( F `  t )  ->  ( F `  t )  =  ( F `  w ) )
7574adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
( F `  t
)  =  ( F `
 w ) )
76 eleq1 2492 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  w  ->  (
b  e.  ran  G  <->  w  e.  ran  G ) )
77763anbi3d 1341 . . . . . . . . . . . . . . . . 17  |-  ( b  =  w  ->  (
( ph  /\  t  e.  ran  G  /\  b  e.  ran  G )  <->  ( ph  /\  t  e.  ran  G  /\  w  e.  ran  G ) ) )
78 fveq2 5873 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  w  ->  ( F `  b )  =  ( F `  w ) )
7978eqeq2d 2434 . . . . . . . . . . . . . . . . 17  |-  ( b  =  w  ->  (
( F `  t
)  =  ( F `
 b )  <->  ( F `  t )  =  ( F `  w ) ) )
8077, 79anbi12d 715 . . . . . . . . . . . . . . . 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 4420 . . . . . . . . . . . . . . . . 17  |-  ( b  =  w  ->  (
b R t  <->  w R
t ) )
8281notbid 295 . . . . . . . . . . . . . . . 16  |-  ( b  =  w  ->  ( -.  b R t  <->  -.  w R t ) )
8380, 82imbi12d 321 . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  t  ->  (
a  e.  ran  G  <->  t  e.  ran  G ) )
85843anbi2d 1340 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  t  ->  (
( ph  /\  a  e.  ran  G  /\  b  e.  ran  G )  <->  ( ph  /\  t  e.  ran  G  /\  b  e.  ran  G ) ) )
86 fveq2 5873 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  t  ->  ( F `  a )  =  ( F `  t ) )
8786eqeq1d 2422 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  t  ->  (
( F `  a
)  =  ( F `
 b )  <->  ( F `  t )  =  ( F `  b ) ) )
8885, 87anbi12d 715 . . . . . . . . . . . . . . . . 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 4421 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  t  ->  (
b R a  <->  b R
t ) )
9089notbid 295 . . . . . . . . . . . . . . . . 17  |-  ( a  =  t  ->  ( -.  b R a  <->  -.  b R t ) )
9188, 90imbi12d 321 . . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  b  ->  (
t  e.  ran  G  <->  b  e.  ran  G ) )
93923anbi3d 1341 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  b  ->  (
( ph  /\  a  e.  ran  G  /\  t  e.  ran  G )  <->  ( ph  /\  a  e.  ran  G  /\  b  e.  ran  G ) ) )
94 fveq2 5873 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  b  ->  ( F `  t )  =  ( F `  b ) )
9594eqeq2d 2434 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  b  ->  (
( F `  a
)  =  ( F `
 t )  <->  ( F `  a )  =  ( F `  b ) ) )
9693, 95anbi12d 715 . . . . . . . . . . . . . . . . . 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 4420 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  b  ->  (
t R a  <->  b R
a ) )
9897notbid 295 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  b  ->  ( -.  t R a  <->  -.  b R a ) )
9996, 98imbi12d 321 . . . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  a  ->  (
w  e.  ran  G  <->  a  e.  ran  G ) )
1011003anbi2d 1340 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  a  ->  (
( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  <->  ( ph  /\  a  e.  ran  G  /\  t  e.  ran  G ) ) )
102 fveq2 5873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  a  ->  ( F `  w )  =  ( F `  a ) )
103102eqeq1d 2422 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  a  ->  (
( F `  w
)  =  ( F `
 t )  <->  ( F `  a )  =  ( F `  t ) ) )
104101, 103anbi12d 715 . . . . . . . . . . . . . . . . . . 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 4421 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  a  ->  (
t R w  <->  t R
a ) )
106105notbid 295 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  a  ->  ( -.  t R w  <->  -.  t R a ) )
107104, 106imbi12d 321 . . . . . . . . . . . . . . . . . 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 1751 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ u ph
109 nfcv 2582 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ u w
110 nfmpt1 4507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ u
( u  e.  ran  F 
|->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
11141, 110nfcxfr 2580 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ u G
112111nfrn 5089 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ u ran  G
113109, 112nfel 2595 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ u  w  e.  ran  G
114112nfcri 2575 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ u  t  e.  ran  G
115108, 113, 114nf3an 1985 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ u
( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )
116 nfv 1751 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ u
( F `  w
)  =  ( F `
 t )
117115, 116nfan 1983 . . . . . . . . . . . . . . . . . . . 20  |-  F/ u
( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )
118 nfv 1751 . . . . . . . . . . . . . . . . . . . 20  |-  F/ u  -.  t R w
119 simp3 1007 . . . . . . . . . . . . . . . . . . . . . . . . 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 2428 . . . . . . . . . . . . . . . . . . . . . . . 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 1035 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( v  =  w  ->  (
t R v  <->  t R w ) )
125124notbid 295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( v  =  w  ->  ( -.  t R v  <->  -.  t R w ) )
126125ralbidv 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( v  =  w  ->  ( A. t  e.  ( `' F " { u } )  -.  t R v  <->  A. t  e.  ( `' F " { u } )  -.  t R w ) )
127126cbvriotav 6270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ran  F )  ->  E! w  e.  ( `' F " { u }
) A. t  e.  ( `' F " { u } )  -.  t R w )
133 riota1 6277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . . 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 6281 . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . . . . . . . . . . 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 1257 . . . . . . . . . . . . . . . . . . . . . 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 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  t  e.  ran  G )  ->  t  e.  A )
1451443adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  w  e.  ran  G  /\  t  e. 
ran  G )  -> 
t  e.  A )
146145adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
t  e.  A )
1471463ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  /\  u  e. 
ran  F )  -> 
( F `  t
)  =  ( F `
 w ) )
1491483adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . 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 6010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1257 . . . . . . . . . . . . . . . . . . . . . . . . 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 2461 . . . . . . . . . . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . . . . . . . . . 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 6010 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  w  e.  ran  G  /\  t  e. 
ran  G )  -> 
( t  e.  ( `' F " { u } )  <->  ( t  e.  A  /\  ( F `  t )  =  u ) ) )
160159ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 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 1025 . . . . . . . . . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . . . . . . . . . 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 2790 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A. t  e.  ( `' F " { u } )  -.  t R w  /\  t  e.  ( `' F " { u } ) )  ->  -.  t R w )
164143, 162, 163syl2anc 665 . . . . . . . . . . . . . . . . . . . . 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 1204 . . . . . . . . . . . . . . . . . . . 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 2907 . . . . . . . . . . . . . . . . . . 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 2067 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  a  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  a )  =  ( F `  t ) )  ->  -.  t R a )
16999, 168chvarv 2067 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  a  e.  ran  G  /\  b  e.  ran  G )  /\  ( F `  a )  =  ( F `  b ) )  ->  -.  b R a )
17091, 169chvarv 2067 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  ran  G  /\  b  e.  ran  G )  /\  ( F `  t )  =  ( F `  b ) )  ->  -.  b R t )
17183, 170chvarv 2067 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  ran  G  /\  w  e.  ran  G )  /\  ( F `  t )  =  ( F `  w ) )  ->  -.  w R t )
17264, 65, 72, 75, 171syl31anc 1267 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  -.  w R t )
173172, 167jca 534 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
( -.  w R t  /\  -.  t R w ) )
174 weso 4837 . . . . . . . . . . . . . . . 16  |-  ( R  We  A  ->  R  Or  A )
1758, 174syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  R  Or  A )
176175adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( F `  w )  =  ( F `  t ) )  ->  R  Or  A )
1771763ad2antl1 1167 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  R  Or  A )
17843sselda 3461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w  e.  ran  G )  ->  w  e.  A )
1791783adant3 1025 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w  e.  ran  G  /\  t  e. 
ran  G )  ->  w  e.  A )
180179adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  w  e.  A )
181 sotrieq2 4795 . . . . . . . . . . . . 13  |-  ( ( R  Or  A  /\  ( w  e.  A  /\  t  e.  A
) )  ->  (
w  =  t  <->  ( -.  w R t  /\  -.  t R w ) ) )
182177, 180, 146, 181syl12anc 1262 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  -> 
( w  =  t  <-> 
( -.  w R t  /\  -.  t R w ) ) )
183173, 182mpbird 235 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( F `  w )  =  ( F `  t ) )  ->  w  =  t )
18455, 63, 183syl2anc 665 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ran  G  /\  t  e.  ran  G )  /\  ( ( F  |`  ran  G ) `  w
)  =  ( ( F  |`  ran  G ) `
 t ) )  ->  w  =  t )
185184ex 435 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  ran  G  /\  t  e. 
ran  G )  -> 
( ( ( F  |`  ran  G ) `  w )  =  ( ( F  |`  ran  G
) `  t )  ->  w  =  t ) )
18652, 53, 54, 185syl3anc 1264 . . . . . . . 8  |-  ( (
ph  /\  ( w  e.  ran  G  /\  t  e.  ran  G ) )  ->  ( ( ( F  |`  ran  G ) `
 w )  =  ( ( F  |`  ran  G ) `  t
)  ->  w  =  t ) )
187186ralrimivva 2844 . . . . . . 7  |-  ( ph  ->  A. w  e.  ran  G A. t  e.  ran  G ( ( ( F  |`  ran  G ) `  w )  =  ( ( F  |`  ran  G
) `  t )  ->  w  =  t ) )
18851, 187jca 534 . . . . . 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 6166 . . . . . 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 215 . . . . 5  |-  ( ph  ->  ( F  |`  ran  G
) : ran  G -1-1-> ran 
F )
191 riotaex 6263 . . . . . . . . . . . . . 14  |-  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )  e. 
_V
192191rgenw 2784 . . . . . . . . . . . . 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 5745 . . . . . . . . . . . 12  |-  ( G  Fn  ran  F  <->  G : ran  F --> ran  G )
197196biimpi 197 . . . . . . . . . . 11  |-  ( G  Fn  ran  F  ->  G : ran  F --> ran  G
)
198195, 197syl 17 . . . . . . . . . 10  |-  ( ph  ->  G : ran  F --> ran  G )
199198ffvelrnda 6029 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( G `  u )  e.  ran  G )
200 fvres 5887 . . . . . . . . . . 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 215 . . . . . . . . . . . . . 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 5965 . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( G `  u )  =  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
206205, 21eqeltrd 2508 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( G `  u )  e.  ( `' F " { u } ) )
207 fvex 5883 . . . . . . . . . . . . . 14  |-  ( G `
 u )  e. 
_V
208 eleq1 2492 . . . . . . . . . . . . . . . 16  |-  ( w  =  ( G `  u )  ->  (
w  e.  ( `' F " { u } )  <->  ( G `  u )  e.  ( `' F " { u } ) ) )
209 eleq1 2492 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( G `  u )  ->  (
w  e.  A  <->  ( G `  u )  e.  A
) )
210 fveq2 5873 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  ( G `  u )  ->  ( F `  w )  =  ( F `  ( G `  u ) ) )
211210eqeq1d 2422 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( G `  u )  ->  (
( F `  w
)  =  u  <->  ( F `  ( G `  u
) )  =  u ) )
212209, 211anbi12d 715 . . . . . . . . . . . . . . . 16  |-  ( w  =  ( G `  u )  ->  (
( w  e.  A  /\  ( F `  w
)  =  u )  <-> 
( ( G `  u )  e.  A  /\  ( F `  ( G `  u )
)  =  u ) ) )
213208, 212bibi12d 322 . . . . . . . . . . . . . . 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 317 . . . . . . . . . . . . . 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 3130 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( G `  u )  e.  ( `' F " { u } )  <->  ( ( G `  u )  e.  A  /\  ( F `  ( G `  u ) )  =  u ) ) )
217216adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ran  F )  ->  (
( G `  u
)  e.  ( `' F " { u } )  <->  ( ( G `  u )  e.  A  /\  ( F `  ( G `  u ) )  =  u ) ) )
218206, 217mpbid 213 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ran  F )  ->  (
( G `  u
)  e.  A  /\  ( F `  ( G `
 u ) )  =  u ) )
219218simprd 464 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ran  F )  ->  ( F `  ( G `  u ) )  =  u )
220201, 219eqtr2d 2462 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ran  F )  ->  u  =  ( ( F  |`  ran  G ) `  ( G `  u ) ) )
221 fveq2 5873 . . . . . . . . . . 11  |-  ( w  =  ( G `  u )  ->  (
( F  |`  ran  G
) `  w )  =  ( ( F  |`  ran  G ) `  ( G `  u ) ) )
222221eqeq2d 2434 . . . . . . . . . 10  |-  ( w  =  ( G `  u )  ->  (
u  =  ( ( F  |`  ran  G ) `
 w )  <->  u  =  ( ( F  |`  ran  G ) `  ( G `  u )
) ) )
223222rspcev 3179 . . . . . . . . 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 665 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ran  F )  ->  E. w  e.  ran  G  u  =  ( ( F  |`  ran  G ) `  w
) )
225224ralrimiva 2837 . . . . . . 7  |-  ( ph  ->  A. u  e.  ran  F E. w  e.  ran  G  u  =  ( ( F  |`  ran  G ) `
 w ) )
22651, 225jca 534 . . . . . 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 6044 . . . . . 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 215 . . . . 5  |-  ( ph  ->  ( F  |`  ran  G
) : ran  G -onto-> ran  F )
229190, 228jca 534 . . . 4  |-  ( ph  ->  ( ( F  |`  ran  G ) : ran  G
-1-1-> ran  F  /\  ( F  |`  ran  G ) : ran  G -onto-> ran  F ) )
230 df-f1o 5600 . . . 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 215 . . 3  |-  ( ph  ->  ( F  |`  ran  G
) : ran  G -1-1-onto-> ran  F )
232 nfcv 2582 . . . . . 6  |-  F/_ v F
233 nfcv 2582 . . . . . . . . 9  |-  F/_ v ran  F
234 nfriota1 6266 . . . . . . . . 9  |-  F/_ v
( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v )
235233, 234nfmpt 4506 . . . . . . . 8  |-  F/_ v
( u  e.  ran  F 
|->  ( iota_ v  e.  ( `' F " { u } ) A. t  e.  ( `' F " { u } )  -.  t R v ) )
23641, 235nfcxfr 2580 . . . . . . 7  |-  F/_ v G
237236nfrn 5089 . . . . . 6  |-  F/_ v ran  G
238232, 237nfres 5119 . . . . 5  |-  F/_ v
( F  |`  ran  G
)
239238, 237, 233nff1o 5821 . . . 4  |-  F/ v ( F  |`  ran  G
) : ran  G -1-1-onto-> ran  F
240 reseq2 5112 . . . . 5  |-  ( v  =  ran  G  -> 
( F  |`  v
)  =  ( F  |`  ran  G ) )
241 id 23 . . . . 5  |-  ( v  =  ran  G  -> 
v  =  ran  G
)
242 eqidd 2421 . . . . 5  |-  ( v  =  ran  G  ->  ran  F  =  ran  F
)
243240, 241, 242f1oeq123d 5820 . . . 4  |-  ( v  =  ran  G  -> 
( ( F  |`  v ) : v -1-1-onto-> ran 
F  <->  ( F  |`  ran  G ) : ran  G -1-1-onto-> ran 
F ) )
244239, 243rspce 3174 . . 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 665 . 2  |-  ( ph  ->  E. v  e.  ~P  A ( F  |`  v ) : v -1-1-onto-> ran 
F )
246 reseq2 5112 . . . 4  |-  ( v  =  x  ->  ( F  |`  v )  =  ( F  |`  x
) )
247 id 23 . . . 4  |-  ( v  =  x  ->  v  =  x )
248 eqidd 2421 . . . 4  |-  ( v  =  x  ->  ran  F  =  ran  F )
249246, 247, 248f1oeq123d 5820 . . 3  |-  ( v  =  x  ->  (
( F  |`  v
) : v -1-1-onto-> ran  F  <->  ( F  |`  x ) : x -1-1-onto-> ran  F ) )
250249cbvrexv 3054 . 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 199 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 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1867    =/= wne 2616   A.wral 2773   E.wrex 2774   E!wreu 2775   _Vcvv 3078    C_ wss 3433   (/)c0 3758   ~Pcpw 3976   {csn 3993   class class class wbr 4417    |-> cmpt 4476    Or wor 4766    We wwe 4804   `'ccnv 4845   dom cdm 4846   ran crn 4847    |` cres 4848   "cima 4849    Fn wfn 5588   -->wf 5589   -1-1->wf1 5590   -onto->wfo 5591   -1-1-onto->wf1o 5592   ` cfv 5593   iota_crio 6258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4477  df-mpt 4478  df-id 4761  df-po 4767  df-so 4768  df-fr 4805  df-we 4807  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6259
This theorem is referenced by:  wessf1orn  37298
  Copyright terms: Public domain W3C validator