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

Theorem fpwwe2lem12 8521
Description: Lemma for fpwwe2 8523. (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 2961 . . . . . . . . 9  |-  a  e. 
_V
32eldm 5070 . . . . . . . 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 8512 . . . . . . . . . . . . 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 608 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  (
a  C_  A  /\  s  C_  ( a  X.  a ) ) )
87simpld 447 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  a  C_  A )
92elpw 3807 . . . . . . . . . . 11  |-  ( a  e.  ~P A  <->  a  C_  A )
108, 9sylibr 205 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  a  e.  ~P A )
1110ex 425 . . . . . . . . 9  |-  ( ph  ->  ( a W s  ->  a  e.  ~P A ) )
1211exlimdv 1647 . . . . . . . 8  |-  ( ph  ->  ( E. s  a W s  ->  a  e.  ~P A ) )
133, 12syl5bi 210 . . . . . . 7  |-  ( ph  ->  ( a  e.  dom  W  ->  a  e.  ~P A ) )
1413ssrdv 3356 . . . . . 6  |-  ( ph  ->  dom  W  C_  ~P A )
15 sspwuni 4179 . . . . . 6  |-  ( dom 
W  C_  ~P A  <->  U.
dom  W  C_  A )
1614, 15sylib 190 . . . . 5  |-  ( ph  ->  U. dom  W  C_  A )
171, 16syl5eqss 3394 . . . 4  |-  ( ph  ->  X  C_  A )
18 vex 2961 . . . . . . . 8  |-  s  e. 
_V
1918elrn 5113 . . . . . . 7  |-  ( s  e.  ran  W  <->  E. a 
a W s )
207simprd 451 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( a  X.  a
) )
214relopabi 5003 . . . . . . . . . . . . . . . 16  |-  Rel  W
2221releldmi 5109 . . . . . . . . . . . . . . 15  |-  ( a W s  ->  a  e.  dom  W )
2322adantl 454 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a W
s )  ->  a  e.  dom  W )
24 elssuni 4045 . . . . . . . . . . . . . 14  |-  ( a  e.  dom  W  -> 
a  C_  U. dom  W
)
2523, 24syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  a  C_ 
U. dom  W )
2625, 1syl6sseqr 3397 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  a  C_  X )
27 xpss12 4984 . . . . . . . . . . . 12  |-  ( ( a  C_  X  /\  a  C_  X )  -> 
( a  X.  a
)  C_  ( X  X.  X ) )
2826, 26, 27syl2anc 644 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  (
a  X.  a ) 
C_  ( X  X.  X ) )
2920, 28sstrd 3360 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( X  X.  X
) )
3018elpw 3807 . . . . . . . . . 10  |-  ( s  e.  ~P ( X  X.  X )  <->  s  C_  ( X  X.  X
) )
3129, 30sylibr 205 . . . . . . . . 9  |-  ( (
ph  /\  a W
s )  ->  s  e.  ~P ( X  X.  X ) )
3231ex 425 . . . . . . . 8  |-  ( ph  ->  ( a W s  ->  s  e.  ~P ( X  X.  X
) ) )
3332exlimdv 1647 . . . . . . 7  |-  ( ph  ->  ( E. a  a W s  ->  s  e.  ~P ( X  X.  X ) ) )
3419, 33syl5bi 210 . . . . . 6  |-  ( ph  ->  ( s  e.  ran  W  ->  s  e.  ~P ( X  X.  X
) ) )
3534ssrdv 3356 . . . . 5  |-  ( ph  ->  ran  W  C_  ~P ( X  X.  X
) )
36 sspwuni 4179 . . . . 5  |-  ( ran 
W  C_  ~P ( X  X.  X )  <->  U. ran  W  C_  ( X  X.  X
) )
3735, 36sylib 190 . . . 4  |-  ( ph  ->  U. ran  W  C_  ( X  X.  X
) )
3817, 37jca 520 . . 3  |-  ( ph  ->  ( X  C_  A  /\  U. ran  W  C_  ( X  X.  X
) ) )
39 n0 3639 . . . . . . . . 9  |-  ( n  =/=  (/)  <->  E. y  y  e.  n )
40 ssel2 3345 . . . . . . . . . . . . . 14  |-  ( ( n  C_  X  /\  y  e.  n )  ->  y  e.  X )
4140adantl 454 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  -> 
y  e.  X )
421eleq2i 2502 . . . . . . . . . . . . . 14  |-  ( y  e.  X  <->  y  e.  U.
dom  W )
43 eluni2 4021 . . . . . . . . . . . . . 14  |-  ( y  e.  U. dom  W  <->  E. a  e.  dom  W  y  e.  a )
4442, 43bitri 242 . . . . . . . . . . . . 13  |-  ( y  e.  X  <->  E. a  e.  dom  W  y  e.  a )
4541, 44sylib 190 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  ->  E. a  e.  dom  W  y  e.  a )
462inex2 4348 . . . . . . . . . . . . . . . . . . 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 609 . . . . . . . . . . . . . . . . . . . . 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 447 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  a W
s )  ->  s  We  a )
5049ad2ant2r 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
s  We  a )
51 wefr 4575 . . . . . . . . . . . . . . . . . . 19  |-  ( s  We  a  ->  s  Fr  a )
5250, 51syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
s  Fr  a )
53 inss2 3564 . . . . . . . . . . . . . . . . . . 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 739 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  n )
56 simprr 735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  a )
57 inelcm 3684 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  n  /\  y  e.  a )  ->  ( n  i^i  a
)  =/=  (/) )
5855, 56, 57syl2anc 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( n  i^i  a
)  =/=  (/) )
59 fri 4547 . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . 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 3563 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  i^i  a )  C_  n
62 simprl 734 . . . . . . . . . . . . . . . . . . . . 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 3348 . . . . . . . . . . . . . . . . . . . 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 739 . . . . . . . . . . . . . . . . . . . . . . 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 2717 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. z  e.  ( n  i^i  a )  -.  z
s v  <->  -.  E. z  e.  ( n  i^i  a
) z s v )
6664, 65sylib 190 . . . . . . . . . . . . . . . . . . . . . 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 4216 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w U. ran  W  v  <->  <. w ,  v >.  e.  U. ran  W )
68 eluni2 4021 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
w ,  v >.  e.  U. ran  W  <->  E. t  e.  ran  W <. w ,  v >.  e.  t )
6967, 68bitri 242 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w U. ran  W  v  <->  E. t  e.  ran  W
<. w ,  v >.  e.  t )
70 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  t  e. 
_V
7170elrn 5113 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  ran  W  <->  E. b 
b W t )
72 df-br 4216 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w t v  <->  <. w ,  v >.  e.  t
)
73 simprll 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
a W s )
7877ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  b W t )
814, 5fpwwe2lem2 8512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( b  C_  A  /\  t  C_  (
b  X.  b ) ) )
8584simprd 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  C_  (
b  X.  b ) )
8676, 78, 79, 85syl12anc 1183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( w ( b  X.  b
) v  <->  ( w  e.  b  /\  v  e.  b ) )
9089simplbi 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( w ( b  X.  b
) v  ->  w  e.  b )
9188, 90syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( w ( t  i^i  (
b  X.  a ) ) v  <->  ( w  e.  b  /\  v  e.  a  /\  w
t v ) )
9792, 94, 95, 96syl3anbrc 1139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w ( a  X.  a
) v  <->  ( w  e.  a  /\  v  e.  a ) )
106105simplbi 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w ( a  X.  a
) v  ->  w  e.  a )
107104, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
108 elin 3532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  ( n  i^i  a )  <->  ( w  e.  n  /\  w  e.  a ) )
10974, 107, 108sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
110 breq1 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  w  ->  (
z s v  <->  w s
v ) )
111110rspcev 3054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( w  e.  ( n  i^i  a )  /\  w s v )  ->  E. z  e.  ( n  i^i  a ) z s v )
112109, 100, 111syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
11373adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
114 simprl 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
11591adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
116114, 115sseldd 3351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
117113, 116, 108sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
118 simplrr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
119 simprr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
120 inss1 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( s  i^i  ( a  X.  b ) )  C_  s
121119, 120syl6eqss 3400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
122121ssbrd 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
123118, 122mpd 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 )
124117, 123, 111syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
1255adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  A  e.  _V )
126 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  ( x  C_  A  /\  r  C_  ( x  X.  x
)  /\  r  We  x ) )  -> 
( x F r )  e.  A )
127126adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( x  C_  A  /\  r  C_  (
x  X.  x )  /\  r  We  x
) )  ->  (
x F r )  e.  A )
128 simprl 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  a W s )
1294, 125, 127, 128, 80fpwwe2lem10 8519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
13076, 78, 79, 129syl12anc 1183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
131112, 124, 130mpjaodan 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
132131expr 600 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
13372, 132syl5bir 211 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
134133expr 600 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
135134exlimdv 1647 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
13671, 135syl5bi 210 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
137136rexlimdv 2831 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
13869, 137syl5bi 210 . . . . . . . . . . . . . . . . . . . . . 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 ) )
13966, 138mtod 171 . . . . . . . . . . . . . . . . . . . . 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 )
140139ralrimiva 2791 . . . . . . . . . . . . . . . . . . . 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 )
14163, 140jca 520 . . . . . . . . . . . . . . . . . . 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 ) )
142141ex 425 . . . . . . . . . . . . . . . . . 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 ) ) )
143142reximdv2 2817 . . . . . . . . . . . . . . . . 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 ) )
14460, 143mpd 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 )
145144exp32 590 . . . . . . . . . . . . . . 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 ) ) )
146145exlimdv 1647 . . . . . . . . . . . . . 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 ) ) )
1473, 146syl5bi 210 . . . . . . . . . . . . 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 ) ) )
148147rexlimdv 2831 . . . . . . . . . . . 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 ) )
14945, 148mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v )
150149expr 600 . . . . . . . . . 10  |-  ( (
ph  /\  n  C_  X
)  ->  ( y  e.  n  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
151150exlimdv 1647 . . . . . . . . 9  |-  ( (
ph  /\  n  C_  X
)  ->  ( E. y  y  e.  n  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
15239, 151syl5bi 210 . . . . . . . 8  |-  ( (
ph  /\  n  C_  X
)  ->  ( n  =/=  (/)  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
153152expimpd 588 . . . . . . 7  |-  ( ph  ->  ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
154153alrimiv 1642 . . . . . 6  |-  ( ph  ->  A. n ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
155 df-fr 4544 . . . . . 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 ) )
156154, 155sylibr 205 . . . . 5  |-  ( ph  ->  U. ran  W  Fr  X )
1571eleq2i 2502 . . . . . . . . . 10  |-  ( w  e.  X  <->  w  e.  U.
dom  W )
158 eluni2 4021 . . . . . . . . . 10  |-  ( w  e.  U. dom  W  <->  E. b  e.  dom  W  w  e.  b )
159157, 158bitri 242 . . . . . . . . 9  |-  ( w  e.  X  <->  E. b  e.  dom  W  w  e.  b )
16044, 159anbi12i 680 . . . . . . . 8  |-  ( ( y  e.  X  /\  w  e.  X )  <->  ( E. a  e.  dom  W  y  e.  a  /\  E. b  e.  dom  W  w  e.  b )
)
161 reeanv 2877 . . . . . . . 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 ) )
162160, 161bitr4i 245 . . . . . . 7  |-  ( ( y  e.  X  /\  w  e.  X )  <->  E. a  e.  dom  W E. b  e.  dom  W ( y  e.  a  /\  w  e.  b ) )
163 vex 2961 . . . . . . . . . . . 12  |-  b  e. 
_V
164163eldm 5070 . . . . . . . . . . 11  |-  ( b  e.  dom  W  <->  E. t 
b W t )
1653, 164anbi12i 680 . . . . . . . . . 10  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  ( E. s 
a W s  /\  E. t  b W t ) )
166 eeanv 1938 . . . . . . . . . 10  |-  ( E. s E. t ( a W s  /\  b W t )  <->  ( E. s  a W s  /\  E. t  b W t ) )
167165, 166bitr4i 245 . . . . . . . . 9  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  E. s E. t
( a W s  /\  b W t ) )
16883simprd 451 . . . . . . . . . . . . . . . . 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 ) )
169168simpld 447 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  We  b
)
170169ad2antrr 708 . . . . . . . . . . . . . . 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 )
171 weso 4576 . . . . . . . . . . . . . . 15  |-  ( t  We  b  ->  t  Or  b )
172170, 171syl 16 . . . . . . . . . . . . . 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 )
173 simprl 734 . . . . . . . . . . . . . . 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 )
174 simplrl 738 . . . . . . . . . . . . . . 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 )
175173, 174sseldd 3351 . . . . . . . . . . . . . 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 )
176 simplrr 739 . . . . . . . . . . . . . 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 )
177 solin 4529 . . . . . . . . . . . . . 14  |-  ( ( t  Or  b  /\  ( y  e.  b  /\  w  e.  b ) )  ->  (
y t w  \/  y  =  w  \/  w t y ) )
178172, 175, 176, 177syl12anc 1183 . . . . . . . . . . . . 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 ) )
17921relelrni 5110 . . . . . . . . . . . . . . . . . 18  |-  ( b W t  ->  t  e.  ran  W )
180179ad2antll 711 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  e.  ran  W )
181180ad2antrr 708 . . . . . . . . . . . . . . . 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
)
182 elssuni 4045 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ran  W  -> 
t  C_  U. ran  W
)
183181, 182syl 16 . . . . . . . . . . . . . . 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
)
184183ssbrd 4256 . . . . . . . . . . . . . 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 ) )
185 idd 23 . . . . . . . . . . . . . 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 ) )
186183ssbrd 4256 . . . . . . . . . . . . . 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 ) )
187184, 185, 1863orim123d 1263 . . . . . . . . . . . . 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 ) ) )
188178, 187mpd 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 ) )
18949adantrr 699 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  We  a
)
190189ad2antrr 708 . . . . . . . . . . . . . . 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 )
191 weso 4576 . . . . . . . . . . . . . . 15  |-  ( s  We  a  ->  s  Or  a )
192190, 191syl 16 . . . . . . . . . . . . . 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 )
193 simplrl 738 . . . . . . . . . . . . . 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 )
194 simprl 734 . . . . . . . . . . . . . . 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 )
195 simplrr 739 . . . . . . . . . . . . . . 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 )
196194, 195sseldd 3351 . . . . . . . . . . . . . 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 )
197 solin 4529 . . . . . . . . . . . . . 14  |-  ( ( s  Or  a  /\  ( y  e.  a  /\  w  e.  a ) )  ->  (
y s w  \/  y  =  w  \/  w s y ) )
198192, 193, 196, 197syl12anc 1183 . . . . . . . . . . . . 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 ) )
19921relelrni 5110 . . . . . . . . . . . . . . . . . 18  |-  ( a W s  ->  s  e.  ran  W )
200199ad2antrl 710 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  e.  ran  W )
201200ad2antrr 708 . . . . . . . . . . . . . . . 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
)
202 elssuni 4045 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ran  W  -> 
s  C_  U. ran  W
)
203201, 202syl 16 . . . . . . . . . . . . . . 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
)
204203ssbrd 4256 . . . . . . . . . . . . . 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 ) )
205 idd 23 . . . . . . . . . . . . . 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 ) )
206203ssbrd 4256 . . . . . . . . . . . . . 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 ) )
207204, 205, 2063orim123d 1263 . . . . . . . . . . . . 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 ) ) )
208198, 207mpd 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 ) )
209129adantr 453 . . . . . . . . . . . 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
) ) ) ) )
210188, 208, 209mpjaodan 763 . . . . . . . . . . 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 ) )
211210exp31 589 . . . . . . . . . 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 ) ) ) )
212211exlimdvv 1648 . . . . . . . . 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 ) ) ) )
213167, 212syl5bi 210 . . . . . . . 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 ) ) ) )
214213rexlimdvv 2838 . . . . . . 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 ) ) )
215162, 214syl5bi 210 . . . . . 6  |-  ( ph  ->  ( ( y  e.  X  /\  w  e.  X )  ->  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) )
216215ralrimivv 2799 . . . . 5  |-  ( ph  ->  A. y  e.  X  A. w  e.  X  ( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) )
217 dfwe2 4765 . . . . 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 ) ) )
218156, 216, 217sylanbrc 647 . . . 4  |-  ( ph  ->  U. ran  W  We  X )
2194fpwwe2cbv 8510 . . . . . . . . . . . . 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 ) ) }
2205adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  A  e.  _V )
221 simpr 449 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  a W s )
222219, 220, 221fpwwe2lem3 8513 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a W s )  /\  y  e.  a )  ->  ( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
223222anasss 630 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
224 cnvimass 5227 . . . . . . . . . . . . 13  |-  ( `'
U. ran  W " {
y } )  C_  dom  U. ran  W
2255, 17ssexd 4353 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  _V )
226 xpexg 4992 . . . . . . . . . . . . . . . . 17  |-  ( ( X  e.  _V  /\  X  e.  _V )  ->  ( X  X.  X
)  e.  _V )
227225, 225, 226syl2anc 644 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  X.  X
)  e.  _V )
228227, 37ssexd 4353 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U. ran  W  e. 
_V )
229228adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  U. ran  W  e.  _V )
230 dmexg 5133 . . . . . . . . . . . . . 14  |-  ( U. ran  W  e.  _V  ->  dom  U. ran  W  e.  _V )
231229, 230syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  dom  U. ran  W  e. 
_V )
232 ssexg 4352 . . . . . . . . . . . . 13  |-  ( ( ( `' U. ran  W
" { y } )  C_  dom  U. ran  W  /\  dom  U. ran  W  e.  _V )  -> 
( `' U. ran  W
" { y } )  e.  _V )
233224, 231, 232sylancr 646 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( `' U. ran  W
" { y } )  e.  _V )
234 id 21 . . . . . . . . . . . . . . 15  |-  ( u  =  ( `' U. ran  W " { y } )  ->  u  =  ( `' U. ran  W " { y } ) )
235 olc 375 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  y  ->  (
w s y  \/  w  =  y ) )
236 df-br 4216 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z U. ran  W  w  <->  <. z ,  w >.  e. 
U. ran  W )
237 eluni2 4021 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
z ,  w >.  e. 
U. ran  W  <->  E. t  e.  ran  W <. z ,  w >.  e.  t
)
238236, 237bitri 242 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z U. ran  W  w  <->  E. t  e.  ran  W
<. z ,  w >.  e.  t )
239 df-br 4216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z t w  <->  <. z ,  w >.  e.  t
)
24085ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
241240ssbrd 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
242 brxp 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( z ( b  X.  b
) w  <->  ( z  e.  b  /\  w  e.  b ) )
243242simplbi 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( z ( b  X.  b
) w  ->  z  e.  b )
244241, 243syl6 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
24520adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  C_  (
a  X.  a ) )
246245ssbrd 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( w s y  ->  w (
a  X.  a ) y ) )
247246imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  w (
a  X.  a ) y )
248 brxp 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( w ( a  X.  a
) y  <->  ( w  e.  a  /\  y  e.  a ) )
249248simplbi 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( w ( a  X.  a
) y  ->  w  e.  a )
250247, 249syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  w  e.  a )
251250a1d 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  ( y  e.  a  ->  w  e.  a ) )
252 elequ1 1729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( w  =  y  ->  (
w  e.  a  <->  y  e.  a ) )
253252biimprd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( w  =  y  ->  (
y  e.  a  ->  w  e.  a )
)
254253adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w  =  y )  ->  ( y  e.  a  ->  w  e.  a ) )
255251, 254jaodan 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( w s y  \/  w  =  y ) )  -> 
( y  e.  a  ->  w  e.  a ) )
256255impr 604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  w  e.  a )
257256adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
258244, 257jctird 530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
259 brxp 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z ( b  X.  a
) w  <->  ( z  e.  b  /\  w  e.  a ) )
260258, 259syl6ibr 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
261260ancld 538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
262 simprr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
263262breqd 4226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
264 brin 4262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( z ( t  i^i  (
b  X.  a ) ) w  <->  ( z
t w  /\  z
( b  X.  a
) w ) )
265263, 264syl6bb 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
266261, 265sylibrd 227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
267 simprr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
268267, 120syl6eqss 3400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
269268ssbrd 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
270129adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
271266, 269, 270mpjaodan 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( z
t w  ->  z
s w ) )
272239, 271syl5bir 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( <. z ,  w >.  e.  t  ->  z s w ) )
273272exp32 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( ( w s y  \/  w  =  y )  -> 
( y  e.  a  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) ) )
274273expr 600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  a W
s )  ->  (
b W t  -> 
( ( w s y  \/  w  =  y )  ->  (
y  e.  a  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
275274com24 84 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  a W
s )  ->  (
y  e.  a  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
276275impr 604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) )
277276imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( b W t  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) )
278277exlimdv 1647 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
27971, 278syl5bi 210 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( t  e. 
ran  W  ->  ( <.
z ,  w >.  e.  t  ->  z s
w ) ) )
280279rexlimdv 2831 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
281238, 280syl5bi 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
282235, 281sylan2 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w  =  y )  ->  (
z U. ran  W  w  ->  z s w ) )
283282ex 425 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( w  =  y  ->  ( z U. ran  W  w  ->  z
s w ) ) )
284283alrimiv 1642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) ) )
285 vex 2961 . . . . . . . . . . . . . . . . . . . 20  |-  y  e. 
_V
286 breq2 4219 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z U. ran  W  w 
<->  z U. ran  W  y ) )
287 breq2 4219 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z s w  <->  z s
y ) )
288286, 287imbi12d 313 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  y  ->  (
( z U. ran  W  w  ->  z s
w )  <->  ( z U. ran  W  y  -> 
z s y ) ) )
289285, 288ceqsalv 2984 . . . . . . . . . . . . . . . . . . 19  |-  ( A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) )  <->  ( z U. ran  W  y  ->  z
s y ) )
290284, 289sylib 190 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  ->  z s
y ) )
291199ad2antrl 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
s  e.  ran  W
)
292291, 202syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
s  C_  U. ran  W
)
293292ssbrd 4256 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z s y  ->  z U. ran  W  y ) )
294290, 293impbid 185 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  <->  z s y ) )
295 vex 2961 . . . . . . . . . . . . . . . . . . 19  |-  z  e. 
_V
296295eliniseg 5236 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  _V  ->  (
z  e.  ( `'
U. ran  W " {
y } )  <->  z U. ran  W  y ) )
297285, 296ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( `' U. ran  W " { y } )  <->  z U. ran  W  y )
298295eliniseg 5236 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  _V  ->  (
z  e.  ( `' s " { y } )  <->  z s
y ) )
299285, 298ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( `' s
" { y } )  <->  z s y )
300294, 297, 2993bitr4g 281 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z  e.  ( `' U. ran  W " { y } )  <-> 
z  e.  ( `' s " { y } ) ) )
301300eqrdv 2436 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( `' U. ran  W
" { y } )  =  ( `' s " { y } ) )
302234, 301sylan9eqr 2492 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  u  =  ( `' s " {
y } ) )
303302, 302xpeq12d 4906 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( u  X.  u )  =  ( ( `' s " { y } )  X.  ( `' s
" { y } ) ) )
304303ineq2d 3544 . . . . . . . . . . . . . . 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 } ) ) ) )
305 inss2 3564 . . . . . . . . . . . . . . . . . 18  |-  ( U. ran  W  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )  C_  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
306 relxp 4986 . . . . . . . . . . . . . . . . . 18  |-  Rel  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
307 relss 4966 . . . . . . . . . . . . . . . . . 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 } ) ) ) ) )
308305, 306, 307mp2 9 . . . . . . . . . . . . . . . . 17  |-  Rel  ( U. ran  W  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) )
309 inss2 3564 . . . . . . . . . . . . . . . . . 18  |-  ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) )  C_  ( ( `' s " {
y } )  X.  ( `' s " { y } ) )
310 relss 4966 . . . . . . . . . . . . . . . . . 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 } ) ) ) ) )
311309, 306, 310mp2 9 . . . . . . . . . . . . . . . . 17  |-  Rel  (
s  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )
312 vex 2961 . . . . . . . . . . . . . . . . . . . . . . 23  |-  w  e. 
_V
313312eliniseg 5236 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  _V  ->  (
w  e.  ( `' s " { y } )  <->  w s
y ) )
314298, 313anbi12d 693 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  _V  ->  (
( z  e.  ( `' s " {
y } )  /\  w  e.  ( `' s " { y } ) )  <->  ( z
s y  /\  w
s y ) ) )
315285, 314ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } ) )  <->  ( z s y  /\  w s y ) )
316 orc 376 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w s y  ->  (
w s y  \/  w  =  y ) )
317316, 281sylan2 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w s
y )  ->  (
z U. ran  W  w  ->  z s w ) )
318317adantrl 698 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
319292adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  s  C_  U. ran  W )
320319ssbrd 4256 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z s w  ->  z U. ran  W  w ) )
321318, 320impbid 185 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  <->  z s
w ) )
322315, 321sylan2b 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " {
y } ) ) )  ->  ( z U. ran  W  w  <->  z s
w ) )
323322pm5.32da 624 . . . . . . . . . . . . . . . . . 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 ) ) )
324 brinxp2 4942 . . . . . . . . . . . . . . . . . . 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 ) )
325 df-br 4216 . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
326 df-3an 939 . . . . . . . . . . . . . . . . . . 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 ) )
327324, 325, 3263bitr3i 268 . . . . . . . . . . . . . . . . . 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 ) )
328 brinxp2 4942 . . . . . . . . . . . . . . . . . . 19  |-  ( z ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) w  <-> 
( z  e.  ( `' s " {
y } )  /\  w  e.  ( `' s " { y } )  /\  z s w ) )
329 df-br 4216 . . . . . . . . . . . . . . . . . . 19  |-  ( z ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) w  <->  <. z ,  w >.  e.  ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) )
330 df-3an 939 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } )  /\  z s w )  <->  ( ( z  e.  ( `' s
" { y } )  /\  w  e.  ( `' s " { y } ) )  /\  z s w ) )
331328, 329, 3303bitr3i 268 . . . . . . . . . . . . . . . . . 18  |-  ( <.
z ,  w >.  e.  ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) )  <->  ( (
z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } ) )  /\  z s w ) )
332323, 327, 3313bitr4g 281 . . . . . . . . . . . . . . . . 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 } ) ) ) ) )
333308, 311, 332eqrelrdv 4975 . . . . . . . . . . . . . . . 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 } ) ) ) )
334333adantr 453 . . . . . . . . . . . . . . 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 } ) ) ) )
335304, 334eqtrd 2470 . . . . . . . . . . . . . 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 } ) ) ) )
336302, 335oveq12d 6102 . . . . . . . . . . . . 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 } ) ) ) ) )
337336eqeq1d 2446 . . . . . . . . . . . 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 ) )
338233, 337sbcied 3199 . . . . . . . . . . 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 ) )
339223, 338mpbird 225 . . . . . . . . . 10  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  [. ( `' U. ran  W
" { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y )
340339exp32 590 . . . . . . . . 9  |-  ( ph  ->  ( a W s  ->  ( y  e.  a  ->  [. ( `'
U. ran  W " {
y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) ) )
341340exlimdv 1647 . . . . . . . 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 ) ) )
3423, 341syl5bi 210 . . . . . . 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 ) ) )
343342rexlimdv 2831 . . . . . 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 ) )
34444, 343syl5bi 210 . . . . 5  |-  ( ph  ->  ( y  e.  X  ->  [. ( `' U. ran  W " { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) )
345344ralrimiv 2790 . . . 4  |-  ( ph  ->  A. y  e.  X  [. ( `' U. ran  W
" { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y )
346218, 345jca 520 . . 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 ) )
3474, 5fpwwe2lem2 8512 . . 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 ) ) ) )
34838, 346, 347mpbir2and 890 . 2  |-  ( ph  ->  X W U. ran  W )
34921releldmi 5109 . 2  |-  ( X W U. ran  W  ->  X  e.  dom  W
)
350348, 349syl 16 1  |-  ( ph  ->  X  e.  dom  W
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360    \/ w3o 936    /\ w3a 937   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726    =/= wne 2601   A.wral 2707   E.wrex 2708   _Vcvv 2958   [.wsbc 3163    i^i cin 3321    C_ wss 3322   (/)c0 3630   ~Pcpw 3801   {csn 3816   <.cop 3819   U.cuni 4017   class class class wbr 4215   {copab 4268    Or wor 4505    Fr wfr 4541    We wwe 4543    X. cxp 4879   `'ccnv 4880   dom cdm 4881   ran crn 4882   "cima 4884   Rel wrel 4886  (class class class)co 6084
This theorem is referenced by:  fpwwe2lem13  8522  fpwwe2  8523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-ov 6087  df-riota 6552  df-recs 6636  df-oi 7482
  Copyright terms: Public domain W3C validator