MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fpwwe2lem12 Structured version   Visualization version   Unicode version

Theorem fpwwe2lem12 9071
Description: Lemma for fpwwe2 9073. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1  |-  W  =  { <. x ,  r
>.  |  ( (
x  C_  A  /\  r  C_  ( x  X.  x ) )  /\  ( r  We  x  /\  A. y  e.  x  [. ( `' r " { y } )  /  u ]. (
u F ( r  i^i  ( u  X.  u ) ) )  =  y ) ) }
fpwwe2.2  |-  ( ph  ->  A  e.  _V )
fpwwe2.3  |-  ( (
ph  /\  ( x  C_  A  /\  r  C_  ( x  X.  x
)  /\  r  We  x ) )  -> 
( x F r )  e.  A )
fpwwe2.4  |-  X  = 
U. dom  W
Assertion
Ref Expression
fpwwe2lem12  |-  ( ph  ->  X  e.  dom  W
)
Distinct variable groups:    y, u, r, x, F    X, r, u, x, y    ph, r, u, x, y    A, r, x    W, r, u, x, y
Allowed substitution hints:    A( y, u)

Proof of Theorem fpwwe2lem12
Dummy variables  a 
b  s  t  v  w  z  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fpwwe2.4 . . . . 5  |-  X  = 
U. dom  W
2 vex 3050 . . . . . . . . 9  |-  a  e. 
_V
32eldm 5035 . . . . . . . 8  |-  ( a  e.  dom  W  <->  E. s 
a W s )
4 fpwwe2.1 . . . . . . . . . . . . . 14  |-  W  =  { <. x ,  r
>.  |  ( (
x  C_  A  /\  r  C_  ( x  X.  x ) )  /\  ( r  We  x  /\  A. y  e.  x  [. ( `' r " { y } )  /  u ]. (
u F ( r  i^i  ( u  X.  u ) ) )  =  y ) ) }
5 fpwwe2.2 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  _V )
64, 5fpwwe2lem2 9062 . . . . . . . . . . . . 13  |-  ( ph  ->  ( a W s  <-> 
( ( a  C_  A  /\  s  C_  (
a  X.  a ) )  /\  ( s  We  a  /\  A. y  e.  a  [. ( `' s " {
y } )  /  u ]. ( u F ( s  i^i  (
u  X.  u ) ) )  =  y ) ) ) )
76simprbda 629 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  (
a  C_  A  /\  s  C_  ( a  X.  a ) ) )
87simpld 461 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  a  C_  A )
9 selpw 3960 . . . . . . . . . . 11  |-  ( a  e.  ~P A  <->  a  C_  A )
108, 9sylibr 216 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  a  e.  ~P A )
1110ex 436 . . . . . . . . 9  |-  ( ph  ->  ( a W s  ->  a  e.  ~P A ) )
1211exlimdv 1781 . . . . . . . 8  |-  ( ph  ->  ( E. s  a W s  ->  a  e.  ~P A ) )
133, 12syl5bi 221 . . . . . . 7  |-  ( ph  ->  ( a  e.  dom  W  ->  a  e.  ~P A ) )
1413ssrdv 3440 . . . . . 6  |-  ( ph  ->  dom  W  C_  ~P A )
15 sspwuni 4370 . . . . . 6  |-  ( dom 
W  C_  ~P A  <->  U.
dom  W  C_  A )
1614, 15sylib 200 . . . . 5  |-  ( ph  ->  U. dom  W  C_  A )
171, 16syl5eqss 3478 . . . 4  |-  ( ph  ->  X  C_  A )
18 vex 3050 . . . . . . . 8  |-  s  e. 
_V
1918elrn 5078 . . . . . . 7  |-  ( s  e.  ran  W  <->  E. a 
a W s )
207simprd 465 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( a  X.  a
) )
214relopabi 4962 . . . . . . . . . . . . . . . 16  |-  Rel  W
2221releldmi 5074 . . . . . . . . . . . . . . 15  |-  ( a W s  ->  a  e.  dom  W )
2322adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a W
s )  ->  a  e.  dom  W )
24 elssuni 4230 . . . . . . . . . . . . . 14  |-  ( a  e.  dom  W  -> 
a  C_  U. dom  W
)
2523, 24syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  a  C_ 
U. dom  W )
2625, 1syl6sseqr 3481 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  a  C_  X )
27 xpss12 4943 . . . . . . . . . . . 12  |-  ( ( a  C_  X  /\  a  C_  X )  -> 
( a  X.  a
)  C_  ( X  X.  X ) )
2826, 26, 27syl2anc 667 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  (
a  X.  a ) 
C_  ( X  X.  X ) )
2920, 28sstrd 3444 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( X  X.  X
) )
30 selpw 3960 . . . . . . . . . 10  |-  ( s  e.  ~P ( X  X.  X )  <->  s  C_  ( X  X.  X
) )
3129, 30sylibr 216 . . . . . . . . 9  |-  ( (
ph  /\  a W
s )  ->  s  e.  ~P ( X  X.  X ) )
3231ex 436 . . . . . . . 8  |-  ( ph  ->  ( a W s  ->  s  e.  ~P ( X  X.  X
) ) )
3332exlimdv 1781 . . . . . . 7  |-  ( ph  ->  ( E. a  a W s  ->  s  e.  ~P ( X  X.  X ) ) )
3419, 33syl5bi 221 . . . . . 6  |-  ( ph  ->  ( s  e.  ran  W  ->  s  e.  ~P ( X  X.  X
) ) )
3534ssrdv 3440 . . . . 5  |-  ( ph  ->  ran  W  C_  ~P ( X  X.  X
) )
36 sspwuni 4370 . . . . 5  |-  ( ran 
W  C_  ~P ( X  X.  X )  <->  U. ran  W  C_  ( X  X.  X
) )
3735, 36sylib 200 . . . 4  |-  ( ph  ->  U. ran  W  C_  ( X  X.  X
) )
3817, 37jca 535 . . 3  |-  ( ph  ->  ( X  C_  A  /\  U. ran  W  C_  ( X  X.  X
) ) )
39 n0 3743 . . . . . . . . 9  |-  ( n  =/=  (/)  <->  E. y  y  e.  n )
40 ssel2 3429 . . . . . . . . . . . . . 14  |-  ( ( n  C_  X  /\  y  e.  n )  ->  y  e.  X )
4140adantl 468 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  -> 
y  e.  X )
421eleq2i 2523 . . . . . . . . . . . . . 14  |-  ( y  e.  X  <->  y  e.  U.
dom  W )
43 eluni2 4205 . . . . . . . . . . . . . 14  |-  ( y  e.  U. dom  W  <->  E. a  e.  dom  W  y  e.  a )
4442, 43bitri 253 . . . . . . . . . . . . 13  |-  ( y  e.  X  <->  E. a  e.  dom  W  y  e.  a )
4541, 44sylib 200 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  ->  E. a  e.  dom  W  y  e.  a )
462inex2 4548 . . . . . . . . . . . . . . . . . . 19  |-  ( n  i^i  a )  e. 
_V
4746a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( n  i^i  a
)  e.  _V )
486simplbda 630 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  a W
s )  ->  (
s  We  a  /\  A. y  e.  a  [. ( `' s " {
y } )  /  u ]. ( u F ( s  i^i  (
u  X.  u ) ) )  =  y ) )
4948simpld 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  a W
s )  ->  s  We  a )
5049ad2ant2r 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
s  We  a )
51 wefr 4827 . . . . . . . . . . . . . . . . . . 19  |-  ( s  We  a  ->  s  Fr  a )
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
s  Fr  a )
53 inss2 3655 . . . . . . . . . . . . . . . . . . 19  |-  ( n  i^i  a )  C_  a
5453a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( n  i^i  a
)  C_  a )
55 simplrr 772 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  n )
56 simprr 767 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  a )
57 inelcm 3821 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  n  /\  y  e.  a )  ->  ( n  i^i  a
)  =/=  (/) )
5855, 56, 57syl2anc 667 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( n  i^i  a
)  =/=  (/) )
59 fri 4799 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( n  i^i  a )  e.  _V  /\  s  Fr  a )  /\  ( ( n  i^i  a )  C_  a  /\  ( n  i^i  a )  =/=  (/) ) )  ->  E. v  e.  ( n  i^i  a ) A. z  e.  ( n  i^i  a )  -.  z s v )
6047, 52, 54, 58, 59syl22anc 1270 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  ->  E. v  e.  (
n  i^i  a ) A. z  e.  (
n  i^i  a )  -.  z s v )
61 inss1 3654 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  i^i  a )  C_  n
62 simprl 765 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  /\  ( v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  -> 
v  e.  ( n  i^i  a ) )
6361, 62sseldi 3432 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  /\  ( v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  -> 
v  e.  n )
64 simplrr 772 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  w  e.  n )  ->  A. z  e.  ( n  i^i  a )  -.  z s v )
65 ralnex 2836 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. z  e.  ( n  i^i  a )  -.  z
s v  <->  -.  E. z  e.  ( n  i^i  a
) z s v )
6664, 65sylib 200 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  w  e.  n )  ->  -.  E. z  e.  ( n  i^i  a
) z s v )
67 df-br 4406 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w U. ran  W  v  <->  <. w ,  v >.  e.  U. ran  W )
68 eluni2 4205 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
w ,  v >.  e.  U. ran  W  <->  E. t  e.  ran  W <. w ,  v >.  e.  t )
6967, 68bitri 253 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w U. ran  W  v  <->  E. t  e.  ran  W
<. w ,  v >.  e.  t )
70 vex 3050 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  t  e. 
_V
7170elrn 5078 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  ran  W  <->  E. b 
b W t )
72 df-br 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w t v  <->  <. w ,  v >.  e.  t
)
73 simprll 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  w  e.  n
)
7473adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  w  e.  n
)
75 simprr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  w t v )
76 simp-4l 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  ph )
77 simprl 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
a W s )
7877ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  a W s )
79 simprlr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  b W t )
80 simprr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  b W t )
814, 5fpwwe2lem2 9062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ph  ->  ( b W t  <-> 
( ( b  C_  A  /\  t  C_  (
b  X.  b ) )  /\  ( t  We  b  /\  A. y  e.  b  [. ( `' t " {
y } )  /  u ]. ( u F ( t  i^i  (
u  X.  u ) ) )  =  y ) ) ) )
8281adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( b W t  <->  ( ( b 
C_  A  /\  t  C_  ( b  X.  b
) )  /\  (
t  We  b  /\  A. y  e.  b  [. ( `' t " {
y } )  /  u ]. ( u F ( t  i^i  (
u  X.  u ) ) )  =  y ) ) ) )
8380, 82mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( ( b 
C_  A  /\  t  C_  ( b  X.  b
) )  /\  (
t  We  b  /\  A. y  e.  b  [. ( `' t " {
y } )  /  u ]. ( u F ( t  i^i  (
u  X.  u ) ) )  =  y ) ) )
8483simpld 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( b  C_  A  /\  t  C_  (
b  X.  b ) ) )
8584simprd 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  C_  (
b  X.  b ) )
8676, 78, 79, 85syl12anc 1267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  t  C_  (
b  X.  b ) )
8786ssbrd 4447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  ( w t v  ->  w (
b  X.  b ) v ) )
8875, 87mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  w ( b  X.  b ) v )
89 brxp 4868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( w ( b  X.  b
) v  <->  ( w  e.  b  /\  v  e.  b ) )
9089simplbi 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( w ( b  X.  b
) v  ->  w  e.  b )
9188, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  w  e.  b )
9291adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  w  e.  b )
9353, 62sseldi 3432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  /\  ( v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  -> 
v  e.  a )
9493ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  v  e.  a )
95 simplrr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  w t v )
96 brinxp2 4899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( w ( t  i^i  (
b  X.  a ) ) v  <->  ( w  e.  b  /\  v  e.  a  /\  w
t v ) )
9792, 94, 95, 96syl3anbrc 1193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  w ( t  i^i  ( b  X.  a ) ) v )
98 simprr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  s  =  ( t  i^i  ( b  X.  a ) ) )
9998breqd 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  ( w s v  <->  w ( t  i^i  ( b  X.  a ) ) v ) )
10097, 99mpbird 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  w s v )
10176, 78, 20syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  s  C_  (
a  X.  a ) )
102101adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  s  C_  (
a  X.  a ) )
103102ssbrd 4447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  ( w s v  ->  w (
a  X.  a ) v ) )
104100, 103mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  w ( a  X.  a ) v )
105 brxp 4868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w ( a  X.  a
) v  <->  ( w  e.  a  /\  v  e.  a ) )
106105simplbi 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w ( a  X.  a
) v  ->  w  e.  a )
107104, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  w  e.  a )
10874, 107elind 3620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  w  e.  ( n  i^i  a ) )
109 breq1 4408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  w  ->  (
z s v  <->  w s
v ) )
110109rspcev 3152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( w  e.  ( n  i^i  a )  /\  w s v )  ->  E. z  e.  ( n  i^i  a ) z s v )
111108, 100, 110syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  E. z  e.  ( n  i^i  a ) z s v )
11273adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  w  e.  n
)
113 simprl 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  b  C_  a
)
11491adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  w  e.  b )
115113, 114sseldd 3435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  w  e.  a )
116112, 115elind 3620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  w  e.  ( n  i^i  a ) )
117 simplrr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  w t v )
118 simprr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  t  =  ( s  i^i  ( a  X.  b ) ) )
119 inss1 3654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( s  i^i  ( a  X.  b ) )  C_  s
120118, 119syl6eqss 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  t  C_  s
)
121120ssbrd 4447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  ( w t v  ->  w s
v ) )
122117, 121mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  w s v )
123116, 122, 110syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) )  ->  E. z  e.  ( n  i^i  a ) z s v )
1245adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  A  e.  _V )
125 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  ( x  C_  A  /\  r  C_  ( x  X.  x
)  /\  r  We  x ) )  -> 
( x F r )  e.  A )
126125adantlr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( x  C_  A  /\  r  C_  (
x  X.  x )  /\  r  We  x
) )  ->  (
x F r )  e.  A )
127 simprl 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  a W s )
1284, 124, 126, 127, 80fpwwe2lem10 9069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) )  \/  ( b  C_  a  /\  t  =  (
s  i^i  ( a  X.  b ) ) ) ) )
12976, 78, 79, 128syl12anc 1267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  ( ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) )  \/  ( b  C_  a  /\  t  =  (
s  i^i  ( a  X.  b ) ) ) ) )
130111, 123, 129mpjaodan 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w
t v ) )  ->  E. z  e.  ( n  i^i  a ) z s v )
131130expr 620 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( w  e.  n  /\  b W t ) )  ->  ( w
t v  ->  E. z  e.  ( n  i^i  a
) z s v ) )
13272, 131syl5bir 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  ( w  e.  n  /\  b W t ) )  ->  ( <. w ,  v >.  e.  t  ->  E. z  e.  ( n  i^i  a ) z s v ) )
133132expr 620 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  w  e.  n )  ->  ( b W t  ->  ( <. w ,  v >.  e.  t  ->  E. z  e.  ( n  i^i  a ) z s v ) ) )
134133exlimdv 1781 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  w  e.  n )  ->  ( E. b  b W t  ->  ( <. w ,  v >.  e.  t  ->  E. z  e.  ( n  i^i  a
) z s v ) ) )
13571, 134syl5bi 221 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  w  e.  n )  ->  ( t  e.  ran  W  ->  ( <. w ,  v >.  e.  t  ->  E. z  e.  ( n  i^i  a ) z s v ) ) )
136135rexlimdv 2879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  w  e.  n )  ->  ( E. t  e. 
ran  W <. w ,  v >.  e.  t  ->  E. z  e.  ( n  i^i  a ) z s v ) )
13769, 136syl5bi 221 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  w  e.  n )  ->  ( w U. ran  W  v  ->  E. z  e.  ( n  i^i  a
) z s v ) )
13866, 137mtod 181 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n
) )  /\  (
a W s  /\  y  e.  a )
)  /\  ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  /\  w  e.  n )  ->  -.  w U. ran  W  v )
139138ralrimiva 2804 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  /\  ( v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  ->  A. w  e.  n  -.  w U. ran  W  v )
14063, 139jca 535 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  /\  ( v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a
)  -.  z s v ) )  -> 
( v  e.  n  /\  A. w  e.  n  -.  w U. ran  W  v ) )
141140ex 436 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( v  e.  ( n  i^i  a
)  /\  A. z  e.  ( n  i^i  a
)  -.  z s v )  ->  (
v  e.  n  /\  A. w  e.  n  -.  w U. ran  W  v ) ) )
142141reximdv2 2860 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( E. v  e.  ( n  i^i  a
) A. z  e.  ( n  i^i  a
)  -.  z s v  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
14360, 142mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v )
144143exp32 610 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  -> 
( a W s  ->  ( y  e.  a  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) ) )
145144exlimdv 1781 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  -> 
( E. s  a W s  ->  (
y  e.  a  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) ) )
1463, 145syl5bi 221 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  -> 
( a  e.  dom  W  ->  ( y  e.  a  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) ) )
147146rexlimdv 2879 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  -> 
( E. a  e. 
dom  W  y  e.  a  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
14845, 147mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v )
149148expr 620 . . . . . . . . . 10  |-  ( (
ph  /\  n  C_  X
)  ->  ( y  e.  n  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
150149exlimdv 1781 . . . . . . . . 9  |-  ( (
ph  /\  n  C_  X
)  ->  ( E. y  y  e.  n  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
15139, 150syl5bi 221 . . . . . . . 8  |-  ( (
ph  /\  n  C_  X
)  ->  ( n  =/=  (/)  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
152151expimpd 608 . . . . . . 7  |-  ( ph  ->  ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
153152alrimiv 1775 . . . . . 6  |-  ( ph  ->  A. n ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
154 df-fr 4796 . . . . . 6  |-  ( U. ran  W  Fr  X  <->  A. n
( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
155153, 154sylibr 216 . . . . 5  |-  ( ph  ->  U. ran  W  Fr  X )
1561eleq2i 2523 . . . . . . . . . 10  |-  ( w  e.  X  <->  w  e.  U.
dom  W )
157 eluni2 4205 . . . . . . . . . 10  |-  ( w  e.  U. dom  W  <->  E. b  e.  dom  W  w  e.  b )
158156, 157bitri 253 . . . . . . . . 9  |-  ( w  e.  X  <->  E. b  e.  dom  W  w  e.  b )
15944, 158anbi12i 704 . . . . . . . 8  |-  ( ( y  e.  X  /\  w  e.  X )  <->  ( E. a  e.  dom  W  y  e.  a  /\  E. b  e.  dom  W  w  e.  b )
)
160 reeanv 2960 . . . . . . . 8  |-  ( E. a  e.  dom  W E. b  e.  dom  W ( y  e.  a  /\  w  e.  b )  <->  ( E. a  e.  dom  W  y  e.  a  /\  E. b  e.  dom  W  w  e.  b ) )
161159, 160bitr4i 256 . . . . . . 7  |-  ( ( y  e.  X  /\  w  e.  X )  <->  E. a  e.  dom  W E. b  e.  dom  W ( y  e.  a  /\  w  e.  b ) )
162 vex 3050 . . . . . . . . . . . 12  |-  b  e. 
_V
163162eldm 5035 . . . . . . . . . . 11  |-  ( b  e.  dom  W  <->  E. t 
b W t )
1643, 163anbi12i 704 . . . . . . . . . 10  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  ( E. s 
a W s  /\  E. t  b W t ) )
165 eeanv 2080 . . . . . . . . . 10  |-  ( E. s E. t ( a W s  /\  b W t )  <->  ( E. s  a W s  /\  E. t  b W t ) )
166164, 165bitr4i 256 . . . . . . . . 9  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  E. s E. t
( a W s  /\  b W t ) )
16783simprd 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( t  We  b  /\  A. y  e.  b  [. ( `' t " { y } )  /  u ]. ( u F ( t  i^i  ( u  X.  u ) ) )  =  y ) )
168167simpld 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  We  b
)
169168ad2antrr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
t  We  b )
170 weso 4828 . . . . . . . . . . . . . . 15  |-  ( t  We  b  ->  t  Or  b )
171169, 170syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
t  Or  b )
172 simprl 765 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
a  C_  b )
173 simplrl 771 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
y  e.  a )
174172, 173sseldd 3435 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
y  e.  b )
175 simplrr 772 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  ->  w  e.  b )
176 solin 4781 . . . . . . . . . . . . . 14  |-  ( ( t  Or  b  /\  ( y  e.  b  /\  w  e.  b ) )  ->  (
y t w  \/  y  =  w  \/  w t y ) )
177171, 174, 175, 176syl12anc 1267 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
( y t w  \/  y  =  w  \/  w t y ) )
17821relelrni 5075 . . . . . . . . . . . . . . . . . 18  |-  ( b W t  ->  t  e.  ran  W )
179178ad2antll 736 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  e.  ran  W )
180179ad2antrr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
t  e.  ran  W
)
181 elssuni 4230 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ran  W  -> 
t  C_  U. ran  W
)
182180, 181syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
t  C_  U. ran  W
)
183182ssbrd 4447 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
( y t w  ->  y U. ran  W  w ) )
184 idd 25 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
( y  =  w  ->  y  =  w ) )
185182ssbrd 4447 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
( w t y  ->  w U. ran  W  y ) )
186183, 184, 1853orim123d 1349 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
( ( y t w  \/  y  =  w  \/  w t y )  ->  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) )
187177, 186mpd 15 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) )
18849adantrr 724 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  We  a
)
189188ad2antrr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
s  We  a )
190 weso 4828 . . . . . . . . . . . . . . 15  |-  ( s  We  a  ->  s  Or  a )
191189, 190syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
s  Or  a )
192 simplrl 771 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
y  e.  a )
193 simprl 765 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
b  C_  a )
194 simplrr 772 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  ->  w  e.  b )
195193, 194sseldd 3435 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  ->  w  e.  a )
196 solin 4781 . . . . . . . . . . . . . 14  |-  ( ( s  Or  a  /\  ( y  e.  a  /\  w  e.  a ) )  ->  (
y s w  \/  y  =  w  \/  w s y ) )
197191, 192, 195, 196syl12anc 1267 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
( y s w  \/  y  =  w  \/  w s y ) )
19821relelrni 5075 . . . . . . . . . . . . . . . . . 18  |-  ( a W s  ->  s  e.  ran  W )
199198ad2antrl 735 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  e.  ran  W )
200199ad2antrr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
s  e.  ran  W
)
201 elssuni 4230 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ran  W  -> 
s  C_  U. ran  W
)
202200, 201syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
s  C_  U. ran  W
)
203202ssbrd 4447 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
( y s w  ->  y U. ran  W  w ) )
204 idd 25 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
( y  =  w  ->  y  =  w ) )
205202ssbrd 4447 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
( w s y  ->  w U. ran  W  y ) )
206203, 204, 2053orim123d 1349 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
( ( y s w  \/  y  =  w  \/  w s y )  ->  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) )
207197, 206mpd 15 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) )
208128adantr 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( y  e.  a  /\  w  e.  b ) )  -> 
( ( a  C_  b  /\  s  =  ( t  i^i  ( b  X.  a ) ) )  \/  ( b 
C_  a  /\  t  =  ( s  i^i  ( a  X.  b
) ) ) ) )
209187, 207, 208mpjaodan 796 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( y  e.  a  /\  w  e.  b ) )  -> 
( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) )
210209exp31 609 . . . . . . . . . 10  |-  ( ph  ->  ( ( a W s  /\  b W t )  ->  (
( y  e.  a  /\  w  e.  b )  ->  ( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) ) )
211210exlimdvv 1782 . . . . . . . . 9  |-  ( ph  ->  ( E. s E. t ( a W s  /\  b W t )  ->  (
( y  e.  a  /\  w  e.  b )  ->  ( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) ) )
212166, 211syl5bi 221 . . . . . . . 8  |-  ( ph  ->  ( ( a  e. 
dom  W  /\  b  e.  dom  W )  -> 
( ( y  e.  a  /\  w  e.  b )  ->  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) ) )
213212rexlimdvv 2887 . . . . . . 7  |-  ( ph  ->  ( E. a  e. 
dom  W E. b  e.  dom  W ( y  e.  a  /\  w  e.  b )  ->  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) )
214161, 213syl5bi 221 . . . . . 6  |-  ( ph  ->  ( ( y  e.  X  /\  w  e.  X )  ->  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) )
215214ralrimivv 2810 . . . . 5  |-  ( ph  ->  A. y  e.  X  A. w  e.  X  ( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) )
216 dfwe2 6613 . . . . 5  |-  ( U. ran  W  We  X  <->  ( U. ran  W  Fr  X  /\  A. y  e.  X  A. w  e.  X  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) )
217155, 215, 216sylanbrc 671 . . . 4  |-  ( ph  ->  U. ran  W  We  X )
2184fpwwe2cbv 9060 . . . . . . . . . . . . 13  |-  W  =  { <. z ,  t
>.  |  ( (
z  C_  A  /\  t  C_  ( z  X.  z ) )  /\  ( t  We  z  /\  A. w  e.  z 
[. ( `' t
" { w }
)  /  b ]. ( b F ( t  i^i  ( b  X.  b ) ) )  =  w ) ) }
2195adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  A  e.  _V )
220 simpr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  a W s )
221218, 219, 220fpwwe2lem3 9063 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a W s )  /\  y  e.  a )  ->  ( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
222221anasss 653 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
223 cnvimass 5191 . . . . . . . . . . . . 13  |-  ( `'
U. ran  W " {
y } )  C_  dom  U. ran  W
2245, 17ssexd 4553 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  _V )
225 xpexg 6598 . . . . . . . . . . . . . . . . 17  |-  ( ( X  e.  _V  /\  X  e.  _V )  ->  ( X  X.  X
)  e.  _V )
226224, 224, 225syl2anc 667 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  X.  X
)  e.  _V )
227226, 37ssexd 4553 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U. ran  W  e. 
_V )
228227adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  U. ran  W  e.  _V )
229 dmexg 6729 . . . . . . . . . . . . . 14  |-  ( U. ran  W  e.  _V  ->  dom  U. ran  W  e.  _V )
230228, 229syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  dom  U. ran  W  e. 
_V )
231 ssexg 4552 . . . . . . . . . . . . 13  |-  ( ( ( `' U. ran  W
" { y } )  C_  dom  U. ran  W  /\  dom  U. ran  W  e.  _V )  -> 
( `' U. ran  W
" { y } )  e.  _V )
232223, 230, 231sylancr 670 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( `' U. ran  W
" { y } )  e.  _V )
233 id 22 . . . . . . . . . . . . . . 15  |-  ( u  =  ( `' U. ran  W " { y } )  ->  u  =  ( `' U. ran  W " { y } ) )
234 olc 386 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  y  ->  (
w s y  \/  w  =  y ) )
235 df-br 4406 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z U. ran  W  w  <->  <. z ,  w >.  e. 
U. ran  W )
236 eluni2 4205 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
z ,  w >.  e. 
U. ran  W  <->  E. t  e.  ran  W <. z ,  w >.  e.  t
)
237235, 236bitri 253 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z U. ran  W  w  <->  E. t  e.  ran  W
<. z ,  w >.  e.  t )
238 df-br 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z t w  <->  <. z ,  w >.  e.  t
)
23985ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  t  C_  ( b  X.  b
) )
240239ssbrd 4447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  ( z
t w  ->  z
( b  X.  b
) w ) )
241 brxp 4868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( z ( b  X.  b
) w  <->  ( z  e.  b  /\  w  e.  b ) )
242241simplbi 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( z ( b  X.  b
) w  ->  z  e.  b )
243240, 242syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  ( z
t w  ->  z  e.  b ) )
24420adantrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  C_  (
a  X.  a ) )
245244ssbrd 4447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( w s y  ->  w (
a  X.  a ) y ) )
246245imp 431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  w (
a  X.  a ) y )
247 brxp 4868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( w ( a  X.  a
) y  <->  ( w  e.  a  /\  y  e.  a ) )
248247simplbi 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( w ( a  X.  a
) y  ->  w  e.  a )
249246, 248syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  w  e.  a )
250249a1d 26 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  ( y  e.  a  ->  w  e.  a ) )
251 elequ1 1896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( w  =  y  ->  (
w  e.  a  <->  y  e.  a ) )
252251biimprd 227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( w  =  y  ->  (
y  e.  a  ->  w  e.  a )
)
253252adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w  =  y )  ->  ( y  e.  a  ->  w  e.  a ) )
254250, 253jaodan 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( w s y  \/  w  =  y ) )  -> 
( y  e.  a  ->  w  e.  a ) )
255254impr 625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  w  e.  a )
256255adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  w  e.  a )
257243, 256jctird 547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  ( z
t w  ->  (
z  e.  b  /\  w  e.  a )
) )
258 brxp 4868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z ( b  X.  a
) w  <->  ( z  e.  b  /\  w  e.  a ) )
259257, 258syl6ibr 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  ( z
t w  ->  z
( b  X.  a
) w ) )
260259ancld 556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  ( z
t w  ->  (
z t w  /\  z ( b  X.  a ) w ) ) )
261 simprr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  s  =  ( t  i^i  (
b  X.  a ) ) )
262261breqd 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  ( z
s w  <->  z (
t  i^i  ( b  X.  a ) ) w ) )
263 brin 4455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( z ( t  i^i  (
b  X.  a ) ) w  <->  ( z
t w  /\  z
( b  X.  a
) w ) )
264262, 263syl6bb 265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  ( z
s w  <->  ( z
t w  /\  z
( b  X.  a
) w ) ) )
265260, 264sylibrd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( a  C_  b  /\  s  =  (
t  i^i  ( b  X.  a ) ) ) )  ->  ( z
t w  ->  z
s w ) )
266 simprr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( b  C_  a  /\  t  =  (
s  i^i  ( a  X.  b ) ) ) )  ->  t  =  ( s  i^i  (
a  X.  b ) ) )
267266, 119syl6eqss 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( b  C_  a  /\  t  =  (
s  i^i  ( a  X.  b ) ) ) )  ->  t  C_  s )
268267ssbrd 4447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
( w s y  \/  w  =  y )  /\  y  e.  a ) )  /\  ( b  C_  a  /\  t  =  (
s  i^i  ( a  X.  b ) ) ) )  ->  ( z
t w  ->  z
s w ) )
269128adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( (
a  C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) )  \/  ( b  C_  a  /\  t  =  (
s  i^i  ( a  X.  b ) ) ) ) )
270265, 268, 269mpjaodan 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( z
t w  ->  z
s w ) )
271238, 270syl5bir 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( <. z ,  w >.  e.  t  ->  z s w ) )
272271exp32 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( ( w s y  \/  w  =  y )  -> 
( y  e.  a  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) ) )
273272expr 620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  a W
s )  ->  (
b W t  -> 
( ( w s y  \/  w  =  y )  ->  (
y  e.  a  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
274273com24 90 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  a W
s )  ->  (
y  e.  a  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
275274impr 625 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) )
276275imp 431 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( b W t  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) )
277276exlimdv 1781 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( E. b 
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) )
27871, 277syl5bi 221 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( t  e. 
ran  W  ->  ( <.
z ,  w >.  e.  t  ->  z s
w ) ) )
279278rexlimdv 2879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( E. t  e.  ran  W <. z ,  w >.  e.  t  ->  z s w ) )
280237, 279syl5bi 221 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
281234, 280sylan2 477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w  =  y )  ->  (
z U. ran  W  w  ->  z s w ) )
282281ex 436 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( w  =  y  ->  ( z U. ran  W  w  ->  z
s w ) ) )
283282alrimiv 1775 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) ) )
284 vex 3050 . . . . . . . . . . . . . . . . . . . 20  |-  y  e. 
_V
285 breq2 4409 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z U. ran  W  w 
<->  z U. ran  W  y ) )
286 breq2 4409 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z s w  <->  z s
y ) )
287285, 286imbi12d 322 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  y  ->  (
( z U. ran  W  w  ->  z s
w )  <->  ( z U. ran  W  y  -> 
z s y ) ) )
288284, 287ceqsalv 3077 . . . . . . . . . . . . . . . . . . 19  |-  ( A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) )  <->  ( z U. ran  W  y  ->  z
s y ) )
289283, 288sylib 200 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  ->  z s
y ) )
290198ad2antrl 735 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
s  e.  ran  W
)
291290, 201syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
s  C_  U. ran  W
)
292291ssbrd 4447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z s y  ->  z U. ran  W  y ) )
293289, 292impbid 194 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  <->  z s y ) )
294 vex 3050 . . . . . . . . . . . . . . . . . . 19  |-  z  e. 
_V
295294eliniseg 5200 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  _V  ->  (
z  e.  ( `'
U. ran  W " {
y } )  <->  z U. ran  W  y ) )
296284, 295ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( `' U. ran  W " { y } )  <->  z U. ran  W  y )
297294eliniseg 5200 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  _V  ->  (
z  e.  ( `' s " { y } )  <->  z s
y ) )
298284, 297ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( `' s
" { y } )  <->  z s y )
299293, 296, 2983bitr4g 292 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z  e.  ( `' U. ran  W " { y } )  <-> 
z  e.  ( `' s " { y } ) ) )
300299eqrdv 2451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( `' U. ran  W
" { y } )  =  ( `' s " { y } ) )
301233, 300sylan9eqr 2509 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  u  =  ( `' s " {
y } ) )
302301sqxpeqd 4863 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( u  X.  u )  =  ( ( `' s " { y } )  X.  ( `' s
" { y } ) ) )
303302ineq2d 3636 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( U. ran  W  i^i  ( u  X.  u ) )  =  ( U. ran  W  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )
304 inss2 3655 . . . . . . . . . . . . . . . . . 18  |-  ( U. ran  W  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )  C_  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
305 relxp 4945 . . . . . . . . . . . . . . . . . 18  |-  Rel  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
306 relss 4925 . . . . . . . . . . . . . . . . . 18  |-  ( ( U. ran  W  i^i  ( ( `' s
" { y } )  X.  ( `' s " { y } ) ) ) 
C_  ( ( `' s " { y } )  X.  ( `' s " {
y } ) )  ->  ( Rel  (
( `' s " { y } )  X.  ( `' s
" { y } ) )  ->  Rel  ( U. ran  W  i^i  ( ( `' s
" { y } )  X.  ( `' s " { y } ) ) ) ) )
307304, 305, 306mp2 9 . . . . . . . . . . . . . . . . 17  |-  Rel  ( U. ran  W  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) )
308 inss2 3655 . . . . . . . . . . . . . . . . . 18  |-  ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) )  C_  ( ( `' s " {
y } )  X.  ( `' s " { y } ) )
309 relss 4925 . . . . . . . . . . . . . . . . . 18  |-  ( ( s  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )  C_  (
( `' s " { y } )  X.  ( `' s
" { y } ) )  ->  ( Rel  ( ( `' s
" { y } )  X.  ( `' s " { y } ) )  ->  Rel  ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) ) )
310308, 305, 309mp2 9 . . . . . . . . . . . . . . . . 17  |-  Rel  (
s  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )
311 vex 3050 . . . . . . . . . . . . . . . . . . . . . . 23  |-  w  e. 
_V
312311eliniseg 5200 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  _V  ->  (
w  e.  ( `' s " { y } )  <->  w s
y ) )
313297, 312anbi12d 718 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  _V  ->  (
( z  e.  ( `' s " {
y } )  /\  w  e.  ( `' s " { y } ) )  <->  ( z
s y  /\  w
s y ) ) )
314284, 313ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } ) )  <->  ( z s y  /\  w s y ) )
315 orc 387 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w s y  ->  (
w s y  \/  w  =  y ) )
316315, 280sylan2 477 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w s
y )  ->  (
z U. ran  W  w  ->  z s w ) )
317316adantrl 723 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
318291adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  s  C_  U. ran  W )
319318ssbrd 4447 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z s w  ->  z U. ran  W  w ) )
320317, 319impbid 194 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  <->  z s
w ) )
321314, 320sylan2b 478 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " {
y } ) ) )  ->  ( z U. ran  W  w  <->  z s
w ) )
322321pm5.32da 647 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( ( z  e.  ( `' s
" { y } )  /\  w  e.  ( `' s " { y } ) )  /\  z U. ran  W  w )  <->  ( (
z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } ) )  /\  z s w ) ) )
323 brinxp2 4899 . . . . . . . . . . . . . . . . . . 19  |-  ( z ( U. ran  W  i^i  ( ( `' s
" { y } )  X.  ( `' s " { y } ) ) ) w  <->  ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " {
y } )  /\  z U. ran  W  w ) )
324 df-br 4406 . . . . . . . . . . . . . . . . . . 19  |-  ( z ( U. ran  W  i^i  ( ( `' s
" { y } )  X.  ( `' s " { y } ) ) ) w  <->  <. z ,  w >.  e.  ( U. ran  W  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )
325 df-3an 988 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } )  /\  z U. ran  W  w )  <->  ( (
z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } ) )  /\  z U. ran  W  w ) )
326323, 324, 3253bitr3i 279 . . . . . . . . . . . . . . . . . 18  |-  ( <.
z ,  w >.  e.  ( U. ran  W  i^i  ( ( `' s
" { y } )  X.  ( `' s " { y } ) ) )  <-> 
( ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " {
y } ) )  /\  z U. ran  W  w ) )
327 brinxp2 4899 . . . . . . . . . . . . . . . . . . 19  |-  ( z ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) w  <-> 
( z  e.  ( `' s " {
y } )  /\  w  e.  ( `' s " { y } )  /\  z s w ) )
328 df-br 4406 . . . . . . . . . . . . . . . . . . 19  |-  ( z ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) w  <->  <. z ,  w >.  e.  ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) )
329 df-3an 988 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } )  /\  z s w )  <->  ( ( z  e.  ( `' s
" { y } )  /\  w  e.  ( `' s " { y } ) )  /\  z s w ) )
330327, 328, 3293bitr3i 279 . . . . . . . . . . . . . . . . . 18  |-  ( <.
z ,  w >.  e.  ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) )  <->  ( (
z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } ) )  /\  z s w ) )
331322, 326, 3303bitr4g 292 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( <. z ,  w >.  e.  ( U. ran  W  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) )  <->  <. z ,  w >.  e.  ( s  i^i  ( ( `' s
" { y } )  X.  ( `' s " { y } ) ) ) ) )
332307, 310, 331eqrelrdv 4934 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( U. ran  W  i^i  ( ( `' s
" { y } )  X.  ( `' s " { y } ) ) )  =  ( s  i^i  ( ( `' s
" { y } )  X.  ( `' s " { y } ) ) ) )
333332adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( U. ran  W  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )  =  ( s  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) ) )
334303, 333eqtrd 2487 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( U. ran  W  i^i  ( u  X.  u ) )  =  ( s  i^i  ( ( `' s
" { y } )  X.  ( `' s " { y } ) ) ) )
335301, 334oveq12d 6313 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( u F ( U. ran  W  i^i  ( u  X.  u ) ) )  =  ( ( `' s " { y } ) F ( s  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) ) ) )
336335eqeq1d 2455 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( (
u F ( U. ran  W  i^i  ( u  X.  u ) ) )  =  y  <->  ( ( `' s " {
y } ) F ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) )  =  y ) )
337232, 336sbcied 3306 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( [. ( `' U. ran  W " { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y  <->  ( ( `' s " { y } ) F ( s  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) ) )  =  y ) )
338222, 337mpbird 236 . . . . . . . . . 10  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  [. ( `' U. ran  W
" { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y )
339338exp32 610 . . . . . . . . 9  |-  ( ph  ->  ( a W s  ->  ( y  e.  a  ->  [. ( `'
U. ran  W " {
y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) ) )
340339exlimdv 1781 . . . . . . . 8  |-  ( ph  ->  ( E. s  a W s  ->  (
y  e.  a  ->  [. ( `' U. ran  W
" { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) ) )
3413, 340syl5bi 221 . . . . . . 7  |-  ( ph  ->  ( a  e.  dom  W  ->  ( y  e.  a  ->  [. ( `'
U. ran  W " {
y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) ) )
342341rexlimdv 2879 . . . . . 6  |-  ( ph  ->  ( E. a  e. 
dom  W  y  e.  a  ->  [. ( `' U. ran  W " { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) )
34344, 342syl5bi 221 . . . . 5  |-  ( ph  ->  ( y  e.  X  ->  [. ( `' U. ran  W " { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) )
344343ralrimiv 2802 . . . 4  |-  ( ph  ->  A. y  e.  X  [. ( `' U. ran  W
" { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y )
345217, 344jca 535 . . 3  |-  ( ph  ->  ( U. ran  W  We  X  /\  A. y  e.  X  [. ( `'
U. ran  W " {
y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) )
3464, 5fpwwe2lem2 9062 . . 3  |-  ( ph  ->  ( X W U. ran  W  <->  ( ( X 
C_  A  /\  U. ran  W  C_  ( X  X.  X ) )  /\  ( U. ran  W  We  X  /\  A. y  e.  X  [. ( `'
U. ran  W " {
y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) ) ) )
34738, 345, 346mpbir2and 934 . 2  |-  ( ph  ->  X W U. ran  W )
34821releldmi 5074 . 2  |-  ( X W U. ran  W  ->  X  e.  dom  W
)
349347, 348syl 17 1  |-  ( ph  ->  X  e.  dom  W
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    \/ wo 370    /\ wa 371    \/ w3o 985    /\ w3a 986   A.wal 1444    = wceq 1446   E.wex 1665    e. wcel 1889    =/= wne 2624   A.wral 2739   E.wrex 2740   _Vcvv 3047   [.wsbc 3269    i^i cin 3405    C_ wss 3406   (/)c0 3733   ~Pcpw 3953   {csn 3970   <.cop 3976   U.cuni 4201   class class class wbr 4405   {copab 4463    Or wor 4757    Fr wfr 4793    We wwe 4795    X. cxp 4835   `'ccnv 4836   dom cdm 4837   ran crn 4838   "cima 4840   Rel wrel 4842  (class class class)co 6295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-se 4797  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-isom 5594  df-riota 6257  df-ov 6298  df-wrecs 7033  df-recs 7095  df-oi 8030
This theorem is referenced by:  fpwwe2lem13  9072  fpwwe2  9073
  Copyright terms: Public domain W3C validator