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

Theorem fpwwe2lem12 9048
Description: Lemma for fpwwe2 9050. (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 3061 . . . . . . . . 9  |-  a  e. 
_V
32eldm 5020 . . . . . . . 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 9039 . . . . . . . . . . . . 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 621 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  (
a  C_  A  /\  s  C_  ( a  X.  a ) ) )
87simpld 457 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  a  C_  A )
9 selpw 3961 . . . . . . . . . . 11  |-  ( a  e.  ~P A  <->  a  C_  A )
108, 9sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  a  e.  ~P A )
1110ex 432 . . . . . . . . 9  |-  ( ph  ->  ( a W s  ->  a  e.  ~P A ) )
1211exlimdv 1745 . . . . . . . 8  |-  ( ph  ->  ( E. s  a W s  ->  a  e.  ~P A ) )
133, 12syl5bi 217 . . . . . . 7  |-  ( ph  ->  ( a  e.  dom  W  ->  a  e.  ~P A ) )
1413ssrdv 3447 . . . . . 6  |-  ( ph  ->  dom  W  C_  ~P A )
15 sspwuni 4359 . . . . . 6  |-  ( dom 
W  C_  ~P A  <->  U.
dom  W  C_  A )
1614, 15sylib 196 . . . . 5  |-  ( ph  ->  U. dom  W  C_  A )
171, 16syl5eqss 3485 . . . 4  |-  ( ph  ->  X  C_  A )
18 vex 3061 . . . . . . . 8  |-  s  e. 
_V
1918elrn 5063 . . . . . . 7  |-  ( s  e.  ran  W  <->  E. a 
a W s )
207simprd 461 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( a  X.  a
) )
214relopabi 4947 . . . . . . . . . . . . . . . 16  |-  Rel  W
2221releldmi 5059 . . . . . . . . . . . . . . 15  |-  ( a W s  ->  a  e.  dom  W )
2322adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a W
s )  ->  a  e.  dom  W )
24 elssuni 4219 . . . . . . . . . . . . . 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 3488 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  a  C_  X )
27 xpss12 4928 . . . . . . . . . . . 12  |-  ( ( a  C_  X  /\  a  C_  X )  -> 
( a  X.  a
)  C_  ( X  X.  X ) )
2826, 26, 27syl2anc 659 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  (
a  X.  a ) 
C_  ( X  X.  X ) )
2920, 28sstrd 3451 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( X  X.  X
) )
30 selpw 3961 . . . . . . . . . 10  |-  ( s  e.  ~P ( X  X.  X )  <->  s  C_  ( X  X.  X
) )
3129, 30sylibr 212 . . . . . . . . 9  |-  ( (
ph  /\  a W
s )  ->  s  e.  ~P ( X  X.  X ) )
3231ex 432 . . . . . . . 8  |-  ( ph  ->  ( a W s  ->  s  e.  ~P ( X  X.  X
) ) )
3332exlimdv 1745 . . . . . . 7  |-  ( ph  ->  ( E. a  a W s  ->  s  e.  ~P ( X  X.  X ) ) )
3419, 33syl5bi 217 . . . . . 6  |-  ( ph  ->  ( s  e.  ran  W  ->  s  e.  ~P ( X  X.  X
) ) )
3534ssrdv 3447 . . . . 5  |-  ( ph  ->  ran  W  C_  ~P ( X  X.  X
) )
36 sspwuni 4359 . . . . 5  |-  ( ran 
W  C_  ~P ( X  X.  X )  <->  U. ran  W  C_  ( X  X.  X
) )
3735, 36sylib 196 . . . 4  |-  ( ph  ->  U. ran  W  C_  ( X  X.  X
) )
3817, 37jca 530 . . 3  |-  ( ph  ->  ( X  C_  A  /\  U. ran  W  C_  ( X  X.  X
) ) )
39 n0 3747 . . . . . . . . 9  |-  ( n  =/=  (/)  <->  E. y  y  e.  n )
40 ssel2 3436 . . . . . . . . . . . . . 14  |-  ( ( n  C_  X  /\  y  e.  n )  ->  y  e.  X )
4140adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  -> 
y  e.  X )
421eleq2i 2480 . . . . . . . . . . . . . 14  |-  ( y  e.  X  <->  y  e.  U.
dom  W )
43 eluni2 4194 . . . . . . . . . . . . . 14  |-  ( y  e.  U. dom  W  <->  E. a  e.  dom  W  y  e.  a )
4442, 43bitri 249 . . . . . . . . . . . . 13  |-  ( y  e.  X  <->  E. a  e.  dom  W  y  e.  a )
4541, 44sylib 196 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  ->  E. a  e.  dom  W  y  e.  a )
462inex2 4535 . . . . . . . . . . . . . . . . . . 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 622 . . . . . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  a W
s )  ->  s  We  a )
5049ad2ant2r 745 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
s  We  a )
51 wefr 4812 . . . . . . . . . . . . . . . . . . 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 3659 . . . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  n )
56 simprr 758 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  a )
57 inelcm 3823 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  n  /\  y  e.  a )  ->  ( n  i^i  a
)  =/=  (/) )
5855, 56, 57syl2anc 659 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( n  i^i  a
)  =/=  (/) )
59 fri 4784 . . . . . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . . . . . 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 3658 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  i^i  a )  C_  n
62 simprl 756 . . . . . . . . . . . . . . . . . . . . 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 3439 . . . . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . . . . . . . . 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 2849 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. z  e.  ( n  i^i  a )  -.  z
s v  <->  -.  E. z  e.  ( n  i^i  a
) z s v )
6664, 65sylib 196 . . . . . . . . . . . . . . . . . . . . . 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 4395 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w U. ran  W  v  <->  <. w ,  v >.  e.  U. ran  W )
68 eluni2 4194 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
w ,  v >.  e.  U. ran  W  <->  E. t  e.  ran  W <. w ,  v >.  e.  t )
6967, 68bitri 249 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w U. ran  W  v  <->  E. t  e.  ran  W
<. w ,  v >.  e.  t )
70 vex 3061 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  t  e. 
_V
7170elrn 5063 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  ran  W  <->  E. b 
b W t )
72 df-br 4395 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w t v  <->  <. w ,  v >.  e.  t
)
73 simprll 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
a W s )
7877ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  b W t )
814, 5fpwwe2lem2 9039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( b  C_  A  /\  t  C_  (
b  X.  b ) ) )
8584simprd 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  C_  (
b  X.  b ) )
8676, 78, 79, 85syl12anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( w ( b  X.  b
) v  <->  ( w  e.  b  /\  v  e.  b ) )
9089simplbi 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( w ( t  i^i  (
b  X.  a ) ) v  <->  ( w  e.  b  /\  v  e.  a  /\  w
t v ) )
9792, 94, 95, 96syl3anbrc 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w ( a  X.  a
) v  <->  ( w  e.  a  /\  v  e.  a ) )
106105simplbi 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  w  ->  (
z s v  <->  w s
v ) )
110109rspcev 3159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( w  e.  ( n  i^i  a )  /\  w s v )  ->  E. z  e.  ( n  i^i  a ) z s v )
111108, 100, 110syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( s  i^i  ( a  X.  b ) )  C_  s
120118, 119syl6eqss 3491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  a W s )
1284, 124, 126, 127, 80fpwwe2lem10 9046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 218 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 613 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1745 . . . . . . . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . . . . . 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 177 . . . . . . . . . . . . . . . . . . . . 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 2817 . . . . . . . . . . . . . . . . . . . 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 530 . . . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . . . . 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 2874 . . . . . . . . . . . . . . . . 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 603 . . . . . . . . . . . . . . 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 1745 . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . 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 2893 . . . . . . . . . . . 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 613 . . . . . . . . . 10  |-  ( (
ph  /\  n  C_  X
)  ->  ( y  e.  n  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
150149exlimdv 1745 . . . . . . . . 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 217 . . . . . . . 8  |-  ( (
ph  /\  n  C_  X
)  ->  ( n  =/=  (/)  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
152151expimpd 601 . . . . . . 7  |-  ( ph  ->  ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
153152alrimiv 1740 . . . . . 6  |-  ( ph  ->  A. n ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
154 df-fr 4781 . . . . . 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 212 . . . . 5  |-  ( ph  ->  U. ran  W  Fr  X )
1561eleq2i 2480 . . . . . . . . . 10  |-  ( w  e.  X  <->  w  e.  U.
dom  W )
157 eluni2 4194 . . . . . . . . . 10  |-  ( w  e.  U. dom  W  <->  E. b  e.  dom  W  w  e.  b )
158156, 157bitri 249 . . . . . . . . 9  |-  ( w  e.  X  <->  E. b  e.  dom  W  w  e.  b )
15944, 158anbi12i 695 . . . . . . . 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 2974 . . . . . . . 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 252 . . . . . . 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 3061 . . . . . . . . . . . 12  |-  b  e. 
_V
163162eldm 5020 . . . . . . . . . . 11  |-  ( b  e.  dom  W  <->  E. t 
b W t )
1643, 163anbi12i 695 . . . . . . . . . 10  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  ( E. s 
a W s  /\  E. t  b W t ) )
165 eeanv 2016 . . . . . . . . . 10  |-  ( E. s E. t ( a W s  /\  b W t )  <->  ( E. s  a W s  /\  E. t  b W t ) )
166164, 165bitr4i 252 . . . . . . . . 9  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  E. s E. t
( a W s  /\  b W t ) )
16783simprd 461 . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  We  b
)
169168ad2antrr 724 . . . . . . . . . . . . . . 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 4813 . . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . 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 3442 . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . 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 4766 . . . . . . . . . . . . . 14  |-  ( ( t  Or  b  /\  ( y  e.  b  /\  w  e.  b ) )  ->  (
y t w  \/  y  =  w  \/  w t y ) )
177171, 174, 175, 176syl12anc 1228 . . . . . . . . . . . . 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 5060 . . . . . . . . . . . . . . . . . 18  |-  ( b W t  ->  t  e.  ran  W )
179178ad2antll 727 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  e.  ran  W )
180179ad2antrr 724 . . . . . . . . . . . . . . . 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 4219 . . . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . 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 24 . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . 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 1309 . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  We  a
)
189188ad2antrr 724 . . . . . . . . . . . . . . 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 4813 . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . 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 3442 . . . . . . . . . . . . . 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 4766 . . . . . . . . . . . . . 14  |-  ( ( s  Or  a  /\  ( y  e.  a  /\  w  e.  a ) )  ->  (
y s w  \/  y  =  w  \/  w s y ) )
197191, 192, 195, 196syl12anc 1228 . . . . . . . . . . . . 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 5060 . . . . . . . . . . . . . . . . . 18  |-  ( a W s  ->  s  e.  ran  W )
199198ad2antrl 726 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  e.  ran  W )
200199ad2antrr 724 . . . . . . . . . . . . . . . 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 4219 . . . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . 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 24 . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . 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 1309 . . . . . . . . . . . . 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 463 . . . . . . . . . . . 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 787 . . . . . . . . . . 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 602 . . . . . . . . . 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 1746 . . . . . . . . 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 217 . . . . . . . 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 2901 . . . . . . 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 217 . . . . . 6  |-  ( ph  ->  ( ( y  e.  X  /\  w  e.  X )  ->  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) )
215214ralrimivv 2823 . . . . 5  |-  ( ph  ->  A. y  e.  X  A. w  e.  X  ( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) )
216 dfwe2 6598 . . . . 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 662 . . . 4  |-  ( ph  ->  U. ran  W  We  X )
2184fpwwe2cbv 9037 . . . . . . . . . . . . 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 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  A  e.  _V )
220 simpr 459 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  a W s )
221218, 219, 220fpwwe2lem3 9040 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a W s )  /\  y  e.  a )  ->  ( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
222221anasss 645 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
223 cnvimass 5176 . . . . . . . . . . . . 13  |-  ( `'
U. ran  W " {
y } )  C_  dom  U. ran  W
2245, 17ssexd 4540 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  _V )
225 xpexg 6583 . . . . . . . . . . . . . . . . 17  |-  ( ( X  e.  _V  /\  X  e.  _V )  ->  ( X  X.  X
)  e.  _V )
226224, 224, 225syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  X.  X
)  e.  _V )
227226, 37ssexd 4540 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U. ran  W  e. 
_V )
228227adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  U. ran  W  e.  _V )
229 dmexg 6714 . . . . . . . . . . . . . 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 4539 . . . . . . . . . . . . 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 661 . . . . . . . . . . . 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 382 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  y  ->  (
w s y  \/  w  =  y ) )
235 df-br 4395 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z U. ran  W  w  <->  <. z ,  w >.  e. 
U. ran  W )
236 eluni2 4194 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
z ,  w >.  e. 
U. ran  W  <->  E. t  e.  ran  W <. z ,  w >.  e.  t
)
237235, 236bitri 249 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z U. ran  W  w  <->  E. t  e.  ran  W
<. z ,  w >.  e.  t )
238 df-br 4395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z t w  <->  <. z ,  w >.  e.  t
)
23985ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( z ( b  X.  b
) w  <->  ( z  e.  b  /\  w  e.  b ) )
242241simplbi 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( z ( b  X.  b
) w  ->  z  e.  b )
243240, 242syl6 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  C_  (
a  X.  a ) )
245244ssbrd 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( w s y  ->  w (
a  X.  a ) y ) )
246245imp 427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  w (
a  X.  a ) y )
247 brxp 4853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( w ( a  X.  a
) y  <->  ( w  e.  a  /\  y  e.  a ) )
248247simplbi 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  ( y  e.  a  ->  w  e.  a ) )
251 elequ1 1845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( w  =  y  ->  (
w  e.  a  <->  y  e.  a ) )
252251biimprd 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( w  =  y  ->  (
y  e.  a  ->  w  e.  a )
)
253252adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w  =  y )  ->  ( y  e.  a  ->  w  e.  a ) )
254250, 253jaodan 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( w s y  \/  w  =  y ) )  -> 
( y  e.  a  ->  w  e.  a ) )
255254impr 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  w  e.  a )
256255adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z ( b  X.  a
) w  <->  ( z  e.  b  /\  w  e.  a ) )
259257, 258syl6ibr 227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( z ( t  i^i  (
b  X.  a ) ) w  <->  ( z
t w  /\  z
( b  X.  a
) w ) )
264262, 263syl6bb 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( z
t w  ->  z
s w ) )
271238, 270syl5bir 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( <. z ,  w >.  e.  t  ->  z s w ) )
272271exp32 603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( ( w s y  \/  w  =  y )  -> 
( y  e.  a  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) ) )
273272expr 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  a W
s )  ->  (
b W t  -> 
( ( w s y  \/  w  =  y )  ->  (
y  e.  a  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
274273com24 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  a W
s )  ->  (
y  e.  a  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
275274impr 617 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) )
276275imp 427 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( b W t  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) )
277276exlimdv 1745 . . . . . . . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
281234, 280sylan2 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w  =  y )  ->  (
z U. ran  W  w  ->  z s w ) )
282281ex 432 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( w  =  y  ->  ( z U. ran  W  w  ->  z
s w ) ) )
283282alrimiv 1740 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) ) )
284 vex 3061 . . . . . . . . . . . . . . . . . . . 20  |-  y  e. 
_V
285 breq2 4398 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z U. ran  W  w 
<->  z U. ran  W  y ) )
286 breq2 4398 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z s w  <->  z s
y ) )
287285, 286imbi12d 318 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  y  ->  (
( z U. ran  W  w  ->  z s
w )  <->  ( z U. ran  W  y  -> 
z s y ) ) )
288284, 287ceqsalv 3086 . . . . . . . . . . . . . . . . . . 19  |-  ( A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) )  <->  ( z U. ran  W  y  ->  z
s y ) )
289283, 288sylib 196 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  ->  z s
y ) )
290198ad2antrl 726 . . . . . . . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z s y  ->  z U. ran  W  y ) )
293289, 292impbid 191 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  <->  z s y ) )
294 vex 3061 . . . . . . . . . . . . . . . . . . 19  |-  z  e. 
_V
295294eliniseg 5185 . . . . . . . . . . . . . . . . . 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 5185 . . . . . . . . . . . . . . . . . 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 288 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z  e.  ( `' U. ran  W " { y } )  <-> 
z  e.  ( `' s " { y } ) ) )
300299eqrdv 2399 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( `' U. ran  W
" { y } )  =  ( `' s " { y } ) )
301233, 300sylan9eqr 2465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  u  =  ( `' s " {
y } ) )
302301sqxpeqd 4848 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( u  X.  u )  =  ( ( `' s " { y } )  X.  ( `' s
" { y } ) ) )
303302ineq2d 3640 . . . . . . . . . . . . . . 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 3659 . . . . . . . . . . . . . . . . . 18  |-  ( U. ran  W  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )  C_  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
305 relxp 4930 . . . . . . . . . . . . . . . . . 18  |-  Rel  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
306 relss 4910 . . . . . . . . . . . . . . . . . 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 3659 . . . . . . . . . . . . . . . . . 18  |-  ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) )  C_  ( ( `' s " {
y } )  X.  ( `' s " { y } ) )
309 relss 4910 . . . . . . . . . . . . . . . . . 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 3061 . . . . . . . . . . . . . . . . . . . . . . 23  |-  w  e. 
_V
312311eliniseg 5185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  _V  ->  (
w  e.  ( `' s " { y } )  <->  w s
y ) )
313297, 312anbi12d 709 . . . . . . . . . . . . . . . . . . . . 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 383 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w s y  ->  (
w s y  \/  w  =  y ) )
316315, 280sylan2 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w s
y )  ->  (
z U. ran  W  w  ->  z s w ) )
317316adantrl 714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
318291adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  s  C_  U. ran  W )
319318ssbrd 4435 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z s w  ->  z U. ran  W  w ) )
320317, 319impbid 191 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  <->  z s
w ) )
321314, 320sylan2b 473 . . . . . . . . . . . . . . . . . . 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 639 . . . . . . . . . . . . . . . . . 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 4884 . . . . . . . . . . . . . . . . . . 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 4395 . . . . . . . . . . . . . . . . . . 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 976 . . . . . . . . . . . . . . . . . . 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 275 . . . . . . . . . . . . . . . . . 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 4884 . . . . . . . . . . . . . . . . . . 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 4395 . . . . . . . . . . . . . . . . . . 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 976 . . . . . . . . . . . . . . . . . . 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 275 . . . . . . . . . . . . . . . . . 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 288 . . . . . . . . . . . . . . . . 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 4919 . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . 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 6295 . . . . . . . . . . . . 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 2404 . . . . . . . . . . . 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 3313 . . . . . . . . . . 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 232 . . . . . . . . . 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 603 . . . . . . . . 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 1745 . . . . . . . 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 217 . . . . . . 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 2893 . . . . . 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 217 . . . . 5  |-  ( ph  ->  ( y  e.  X  ->  [. ( `' U. ran  W " { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) )
344343ralrimiv 2815 . . . 4  |-  ( ph  ->  A. y  e.  X  [. ( `' U. ran  W
" { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y )
345217, 344jca 530 . . 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 9039 . . 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 923 . 2  |-  ( ph  ->  X W U. ran  W )
34821releldmi 5059 . 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 184    \/ wo 366    /\ wa 367    \/ w3o 973    /\ w3a 974   A.wal 1403    = wceq 1405   E.wex 1633    e. wcel 1842    =/= wne 2598   A.wral 2753   E.wrex 2754   _Vcvv 3058   [.wsbc 3276    i^i cin 3412    C_ wss 3413   (/)c0 3737   ~Pcpw 3954   {csn 3971   <.cop 3977   U.cuni 4190   class class class wbr 4394   {copab 4451    Or wor 4742    Fr wfr 4778    We wwe 4780    X. cxp 4820   `'ccnv 4821   dom cdm 4822   ran crn 4823   "cima 4825   Rel wrel 4827  (class class class)co 6277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-isom 5577  df-riota 6239  df-ov 6280  df-wrecs 7012  df-recs 7074  df-oi 7968
This theorem is referenced by:  fpwwe2lem13  9049  fpwwe2  9050
  Copyright terms: Public domain W3C validator