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

Theorem fpwwe2lem12 8508
Description: Lemma for fpwwe2 8510. (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 2951 . . . . . . . . 9  |-  a  e. 
_V
32eldm 5059 . . . . . . . 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 8499 . . . . . . . . . . . . 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 607 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  (
a  C_  A  /\  s  C_  ( a  X.  a ) ) )
87simpld 446 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  a  C_  A )
92elpw 3797 . . . . . . . . . . 11  |-  ( a  e.  ~P A  <->  a  C_  A )
108, 9sylibr 204 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  a  e.  ~P A )
1110ex 424 . . . . . . . . 9  |-  ( ph  ->  ( a W s  ->  a  e.  ~P A ) )
1211exlimdv 1646 . . . . . . . 8  |-  ( ph  ->  ( E. s  a W s  ->  a  e.  ~P A ) )
133, 12syl5bi 209 . . . . . . 7  |-  ( ph  ->  ( a  e.  dom  W  ->  a  e.  ~P A ) )
1413ssrdv 3346 . . . . . 6  |-  ( ph  ->  dom  W  C_  ~P A )
15 sspwuni 4168 . . . . . 6  |-  ( dom 
W  C_  ~P A  <->  U.
dom  W  C_  A )
1614, 15sylib 189 . . . . 5  |-  ( ph  ->  U. dom  W  C_  A )
171, 16syl5eqss 3384 . . . 4  |-  ( ph  ->  X  C_  A )
18 vex 2951 . . . . . . . 8  |-  s  e. 
_V
1918elrn 5102 . . . . . . 7  |-  ( s  e.  ran  W  <->  E. a 
a W s )
207simprd 450 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( a  X.  a
) )
214relopabi 4992 . . . . . . . . . . . . . . . 16  |-  Rel  W
2221releldmi 5098 . . . . . . . . . . . . . . 15  |-  ( a W s  ->  a  e.  dom  W )
2322adantl 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a W
s )  ->  a  e.  dom  W )
24 elssuni 4035 . . . . . . . . . . . . . 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 3387 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  a  C_  X )
27 xpss12 4973 . . . . . . . . . . . 12  |-  ( ( a  C_  X  /\  a  C_  X )  -> 
( a  X.  a
)  C_  ( X  X.  X ) )
2826, 26, 27syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  (
a  X.  a ) 
C_  ( X  X.  X ) )
2920, 28sstrd 3350 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( X  X.  X
) )
3018elpw 3797 . . . . . . . . . 10  |-  ( s  e.  ~P ( X  X.  X )  <->  s  C_  ( X  X.  X
) )
3129, 30sylibr 204 . . . . . . . . 9  |-  ( (
ph  /\  a W
s )  ->  s  e.  ~P ( X  X.  X ) )
3231ex 424 . . . . . . . 8  |-  ( ph  ->  ( a W s  ->  s  e.  ~P ( X  X.  X
) ) )
3332exlimdv 1646 . . . . . . 7  |-  ( ph  ->  ( E. a  a W s  ->  s  e.  ~P ( X  X.  X ) ) )
3419, 33syl5bi 209 . . . . . 6  |-  ( ph  ->  ( s  e.  ran  W  ->  s  e.  ~P ( X  X.  X
) ) )
3534ssrdv 3346 . . . . 5  |-  ( ph  ->  ran  W  C_  ~P ( X  X.  X
) )
36 sspwuni 4168 . . . . 5  |-  ( ran 
W  C_  ~P ( X  X.  X )  <->  U. ran  W  C_  ( X  X.  X
) )
3735, 36sylib 189 . . . 4  |-  ( ph  ->  U. ran  W  C_  ( X  X.  X
) )
3817, 37jca 519 . . 3  |-  ( ph  ->  ( X  C_  A  /\  U. ran  W  C_  ( X  X.  X
) ) )
39 n0 3629 . . . . . . . . 9  |-  ( n  =/=  (/)  <->  E. y  y  e.  n )
40 ssel2 3335 . . . . . . . . . . . . . 14  |-  ( ( n  C_  X  /\  y  e.  n )  ->  y  e.  X )
4140adantl 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  -> 
y  e.  X )
421eleq2i 2499 . . . . . . . . . . . . . 14  |-  ( y  e.  X  <->  y  e.  U.
dom  W )
43 eluni2 4011 . . . . . . . . . . . . . 14  |-  ( y  e.  U. dom  W  <->  E. a  e.  dom  W  y  e.  a )
4442, 43bitri 241 . . . . . . . . . . . . 13  |-  ( y  e.  X  <->  E. a  e.  dom  W  y  e.  a )
4541, 44sylib 189 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  ->  E. a  e.  dom  W  y  e.  a )
462inex2 4337 . . . . . . . . . . . . . . . . . . 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 608 . . . . . . . . . . . . . . . . . . . . 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 446 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  a W
s )  ->  s  We  a )
5049ad2ant2r 728 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
s  We  a )
51 wefr 4564 . . . . . . . . . . . . . . . . . . 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 3554 . . . . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  n )
56 simprr 734 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  a )
57 inelcm 3674 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  n  /\  y  e.  a )  ->  ( n  i^i  a
)  =/=  (/) )
5855, 56, 57syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( n  i^i  a
)  =/=  (/) )
59 fri 4536 . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . 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 3553 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  i^i  a )  C_  n
62 simprl 733 . . . . . . . . . . . . . . . . . . . . 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 3338 . . . . . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . . . . . . . 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 2707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. z  e.  ( n  i^i  a )  -.  z
s v  <->  -.  E. z  e.  ( n  i^i  a
) z s v )
6664, 65sylib 189 . . . . . . . . . . . . . . . . . . . . . 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 4205 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w U. ran  W  v  <->  <. w ,  v >.  e.  U. ran  W )
68 eluni2 4011 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
w ,  v >.  e.  U. ran  W  <->  E. t  e.  ran  W <. w ,  v >.  e.  t )
6967, 68bitri 241 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w U. ran  W  v  <->  E. t  e.  ran  W
<. w ,  v >.  e.  t )
70 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  t  e. 
_V
7170elrn 5102 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  ran  W  <->  E. b 
b W t )
72 df-br 4205 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w t v  <->  <. w ,  v >.  e.  t
)
73 simprll 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
a W s )
7877ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  b W t )
814, 5fpwwe2lem2 8499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( b  C_  A  /\  t  C_  (
b  X.  b ) ) )
8584simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  C_  (
b  X.  b ) )
8676, 78, 79, 85syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( w ( b  X.  b
) v  <->  ( w  e.  b  /\  v  e.  b ) )
9089simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( w ( t  i^i  (
b  X.  a ) ) v  <->  ( w  e.  b  /\  v  e.  a  /\  w
t v ) )
9792, 94, 95, 96syl3anbrc 1138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w ( a  X.  a
) v  <->  ( w  e.  a  /\  v  e.  a ) )
106105simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  ( n  i^i  a )  <->  ( w  e.  n  /\  w  e.  a ) )
10974, 107, 108sylanbrc 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  w  ->  (
z s v  <->  w s
v ) )
111110rspcev 3044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( w  e.  ( n  i^i  a )  /\  w s v )  ->  E. z  e.  ( n  i^i  a ) z s v )
112109, 100, 111syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( s  i^i  ( a  X.  b ) )  C_  s
121119, 120syl6eqss 3390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  a W s )
1294, 125, 127, 128, 80fpwwe2lem10 8506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 599 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1646 . . . . . . . . . . . . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . . . . . . . . . . . . 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 2821 . . . . . . . . . . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . . . . . . . . . . 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 170 . . . . . . . . . . . . . . . . . . . . 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 2781 . . . . . . . . . . . . . . . . . . . 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 519 . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . . 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 2807 . . . . . . . . . . . . . . . . 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 589 . . . . . . . . . . . . . . 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 1646 . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . 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 2821 . . . . . . . . . . . 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 599 . . . . . . . . . 10  |-  ( (
ph  /\  n  C_  X
)  ->  ( y  e.  n  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
151150exlimdv 1646 . . . . . . . . 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 209 . . . . . . . 8  |-  ( (
ph  /\  n  C_  X
)  ->  ( n  =/=  (/)  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
153152expimpd 587 . . . . . . 7  |-  ( ph  ->  ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
154153alrimiv 1641 . . . . . 6  |-  ( ph  ->  A. n ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
155 df-fr 4533 . . . . . 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 204 . . . . 5  |-  ( ph  ->  U. ran  W  Fr  X )
1571eleq2i 2499 . . . . . . . . . 10  |-  ( w  e.  X  <->  w  e.  U.
dom  W )
158 eluni2 4011 . . . . . . . . . 10  |-  ( w  e.  U. dom  W  <->  E. b  e.  dom  W  w  e.  b )
159157, 158bitri 241 . . . . . . . . 9  |-  ( w  e.  X  <->  E. b  e.  dom  W  w  e.  b )
16044, 159anbi12i 679 . . . . . . . 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 2867 . . . . . . . 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 244 . . . . . . 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 2951 . . . . . . . . . . . 12  |-  b  e. 
_V
164163eldm 5059 . . . . . . . . . . 11  |-  ( b  e.  dom  W  <->  E. t 
b W t )
1653, 164anbi12i 679 . . . . . . . . . 10  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  ( E. s 
a W s  /\  E. t  b W t ) )
166 eeanv 1937 . . . . . . . . . 10  |-  ( E. s E. t ( a W s  /\  b W t )  <->  ( E. s  a W s  /\  E. t  b W t ) )
167165, 166bitr4i 244 . . . . . . . . 9  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  E. s E. t
( a W s  /\  b W t ) )
16883simprd 450 . . . . . . . . . . . . . . . . 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 446 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  We  b
)
170169ad2antrr 707 . . . . . . . . . . . . . . 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 4565 . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( a  C_  b  /\  s  =  ( t  i^i  (
b  X.  a ) ) ) )  -> 
a  C_  b )
174 simplrl 737 . . . . . . . . . . . . . . 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 3341 . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . 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 4518 . . . . . . . . . . . . . 14  |-  ( ( t  Or  b  /\  ( y  e.  b  /\  w  e.  b ) )  ->  (
y t w  \/  y  =  w  \/  w t y ) )
178172, 175, 176, 177syl12anc 1182 . . . . . . . . . . . . 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 5099 . . . . . . . . . . . . . . . . . 18  |-  ( b W t  ->  t  e.  ran  W )
180179ad2antll 710 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  e.  ran  W )
181180ad2antrr 707 . . . . . . . . . . . . . . . 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 4035 . . . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . 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 22 . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . 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 1262 . . . . . . . . . . . . 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 698 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  We  a
)
190189ad2antrr 707 . . . . . . . . . . . . . . 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 4565 . . . . . . . . . . . . . . 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 737 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( a W s  /\  b W t ) )  /\  (
y  e.  a  /\  w  e.  b )
)  /\  ( b  C_  a  /\  t  =  ( s  i^i  (
a  X.  b ) ) ) )  -> 
b  C_  a )
195 simplrr 738 . . . . . . . . . . . . . . 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 3341 . . . . . . . . . . . . . 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 4518 . . . . . . . . . . . . . 14  |-  ( ( s  Or  a  /\  ( y  e.  a  /\  w  e.  a ) )  ->  (
y s w  \/  y  =  w  \/  w s y ) )
198192, 193, 196, 197syl12anc 1182 . . . . . . . . . . . . 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 5099 . . . . . . . . . . . . . . . . . 18  |-  ( a W s  ->  s  e.  ran  W )
200199ad2antrl 709 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  e.  ran  W )
201200ad2antrr 707 . . . . . . . . . . . . . . . 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 4035 . . . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . 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 22 . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . 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 1262 . . . . . . . . . . . . 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 452 . . . . . . . . . . . 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 762 . . . . . . . . . . 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 588 . . . . . . . . . 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 1647 . . . . . . . . 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 209 . . . . . . . 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 2828 . . . . . . 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 209 . . . . . 6  |-  ( ph  ->  ( ( y  e.  X  /\  w  e.  X )  ->  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) )
216215ralrimivv 2789 . . . . 5  |-  ( ph  ->  A. y  e.  X  A. w  e.  X  ( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) )
217 dfwe2 4754 . . . . 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 646 . . . 4  |-  ( ph  ->  U. ran  W  We  X )
2194fpwwe2cbv 8497 . . . . . . . . . . . . 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 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  A  e.  _V )
221 simpr 448 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  a W s )
222219, 220, 221fpwwe2lem3 8500 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a W s )  /\  y  e.  a )  ->  ( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
223222anasss 629 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
224 cnvimass 5216 . . . . . . . . . . . . 13  |-  ( `'
U. ran  W " {
y } )  C_  dom  U. ran  W
2255, 17ssexd 4342 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  _V )
226 xpexg 4981 . . . . . . . . . . . . . . . . 17  |-  ( ( X  e.  _V  /\  X  e.  _V )  ->  ( X  X.  X
)  e.  _V )
227225, 225, 226syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  X.  X
)  e.  _V )
228227, 37ssexd 4342 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U. ran  W  e. 
_V )
229228adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  U. ran  W  e.  _V )
230 dmexg 5122 . . . . . . . . . . . . . 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 4341 . . . . . . . . . . . . 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 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( `' U. ran  W
" { y } )  e.  _V )
234 id 20 . . . . . . . . . . . . . . 15  |-  ( u  =  ( `' U. ran  W " { y } )  ->  u  =  ( `' U. ran  W " { y } ) )
235 olc 374 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  y  ->  (
w s y  \/  w  =  y ) )
236 df-br 4205 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z U. ran  W  w  <->  <. z ,  w >.  e. 
U. ran  W )
237 eluni2 4011 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
z ,  w >.  e. 
U. ran  W  <->  E. t  e.  ran  W <. z ,  w >.  e.  t
)
238236, 237bitri 241 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z U. ran  W  w  <->  E. t  e.  ran  W
<. z ,  w >.  e.  t )
239 df-br 4205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z t w  <->  <. z ,  w >.  e.  t
)
24085ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( z ( b  X.  b
) w  <->  ( z  e.  b  /\  w  e.  b ) )
243242simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( z ( b  X.  b
) w  ->  z  e.  b )
244241, 243syl6 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 ) )
24520adantrr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  C_  (
a  X.  a ) )
246245ssbrd 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( w s y  ->  w (
a  X.  a ) y ) )
247246imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  w (
a  X.  a ) y )
248 brxp 4901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( w ( a  X.  a
) y  <->  ( w  e.  a  /\  y  e.  a ) )
249248simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  ( y  e.  a  ->  w  e.  a ) )
252 elequ1 1728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( w  =  y  ->  (
w  e.  a  <->  y  e.  a ) )
253252biimprd 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( w  =  y  ->  (
y  e.  a  ->  w  e.  a )
)
254253adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w  =  y )  ->  ( y  e.  a  ->  w  e.  a ) )
255251, 254jaodan 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( w s y  \/  w  =  y ) )  -> 
( y  e.  a  ->  w  e.  a ) )
256255impr 603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  w  e.  a )
257256adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z ( b  X.  a
) w  <->  ( z  e.  b  /\  w  e.  a ) )
260258, 259syl6ibr 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( z ( t  i^i  (
b  X.  a ) ) w  <->  ( z
t w  /\  z
( b  X.  a
) w ) )
265263, 264syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( z
t w  ->  z
s w ) )
272239, 271syl5bir 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( <. z ,  w >.  e.  t  ->  z s w ) )
273272exp32 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( ( w s y  \/  w  =  y )  -> 
( y  e.  a  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) ) )
274273expr 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  a W
s )  ->  (
b W t  -> 
( ( w s y  \/  w  =  y )  ->  (
y  e.  a  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
275274com24 83 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  a W
s )  ->  (
y  e.  a  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
276275impr 603 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) )
277276imp 419 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( b W t  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) )
278277exlimdv 1646 . . . . . . . . . . . . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . . . . . . . . . . . . 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 2821 . . . . . . . . . . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
282235, 281sylan2 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w  =  y )  ->  (
z U. ran  W  w  ->  z s w ) )
283282ex 424 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( w  =  y  ->  ( z U. ran  W  w  ->  z
s w ) ) )
284283alrimiv 1641 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) ) )
285 vex 2951 . . . . . . . . . . . . . . . . . . . 20  |-  y  e. 
_V
286 breq2 4208 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z U. ran  W  w 
<->  z U. ran  W  y ) )
287 breq2 4208 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z s w  <->  z s
y ) )
288286, 287imbi12d 312 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  y  ->  (
( z U. ran  W  w  ->  z s
w )  <->  ( z U. ran  W  y  -> 
z s y ) ) )
289285, 288ceqsalv 2974 . . . . . . . . . . . . . . . . . . 19  |-  ( A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) )  <->  ( z U. ran  W  y  ->  z
s y ) )
290284, 289sylib 189 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  ->  z s
y ) )
291199ad2antrl 709 . . . . . . . . . . . . . . . . . . . 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 4245 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z s y  ->  z U. ran  W  y ) )
294290, 293impbid 184 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  <->  z s y ) )
295 vex 2951 . . . . . . . . . . . . . . . . . . 19  |-  z  e. 
_V
296295eliniseg 5225 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  _V  ->  (
z  e.  ( `'
U. ran  W " {
y } )  <->  z U. ran  W  y ) )
297285, 296ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( `' U. ran  W " { y } )  <->  z U. ran  W  y )
298295eliniseg 5225 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  _V  ->  (
z  e.  ( `' s " { y } )  <->  z s
y ) )
299285, 298ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( `' s
" { y } )  <->  z s y )
300294, 297, 2993bitr4g 280 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z  e.  ( `' U. ran  W " { y } )  <-> 
z  e.  ( `' s " { y } ) ) )
301300eqrdv 2433 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( `' U. ran  W
" { y } )  =  ( `' s " { y } ) )
302234, 301sylan9eqr 2489 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  u  =  ( `' s " {
y } ) )
303302, 302xpeq12d 4895 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( u  X.  u )  =  ( ( `' s " { y } )  X.  ( `' s
" { y } ) ) )
304303ineq2d 3534 . . . . . . . . . . . . . . 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 3554 . . . . . . . . . . . . . . . . . 18  |-  ( U. ran  W  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )  C_  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
306 relxp 4975 . . . . . . . . . . . . . . . . . 18  |-  Rel  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
307 relss 4955 . . . . . . . . . . . . . . . . . 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 3554 . . . . . . . . . . . . . . . . . 18  |-  ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) )  C_  ( ( `' s " {
y } )  X.  ( `' s " { y } ) )
310 relss 4955 . . . . . . . . . . . . . . . . . 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 2951 . . . . . . . . . . . . . . . . . . . . . . 23  |-  w  e. 
_V
313312eliniseg 5225 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  _V  ->  (
w  e.  ( `' s " { y } )  <->  w s
y ) )
314298, 313anbi12d 692 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  _V  ->  (
( z  e.  ( `' s " {
y } )  /\  w  e.  ( `' s " { y } ) )  <->  ( z
s y  /\  w
s y ) ) )
315285, 314ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } ) )  <->  ( z s y  /\  w s y ) )
316 orc 375 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w s y  ->  (
w s y  \/  w  =  y ) )
317316, 281sylan2 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w s
y )  ->  (
z U. ran  W  w  ->  z s w ) )
318317adantrl 697 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
319292adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  s  C_  U. ran  W )
320319ssbrd 4245 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z s w  ->  z U. ran  W  w ) )
321318, 320impbid 184 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  <->  z s
w ) )
322315, 321sylan2b 462 . . . . . . . . . . . . . . . . . . 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 623 . . . . . . . . . . . . . . . . . 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 4931 . . . . . . . . . . . . . . . . . . 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 4205 . . . . . . . . . . . . . . . . . . 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 938 . . . . . . . . . . . . . . . . . . 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 267 . . . . . . . . . . . . . . . . . 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 4931 . . . . . . . . . . . . . . . . . . 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 4205 . . . . . . . . . . . . . . . . . . 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 938 . . . . . . . . . . . . . . . . . . 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 267 . . . . . . . . . . . . . . . . . 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 280 . . . . . . . . . . . . . . . . 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 4964 . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . 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 6091 . . . . . . . . . . . . 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 2443 . . . . . . . . . . . 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 3189 . . . . . . . . . . 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 224 . . . . . . . . . 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 589 . . . . . . . . 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 1646 . . . . . . . 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 209 . . . . . . 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 2821 . . . . . 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 209 . . . . 5  |-  ( ph  ->  ( y  e.  X  ->  [. ( `' U. ran  W " { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) )
345344ralrimiv 2780 . . . 4  |-  ( ph  ->  A. y  e.  X  [. ( `' U. ran  W
" { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y )
346218, 345jca 519 . . 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 8499 . . 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 889 . 2  |-  ( ph  ->  X W U. ran  W )
34921releldmi 5098 . 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 177    \/ wo 358    /\ wa 359    \/ w3o 935    /\ w3a 936   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725    =/= wne 2598   A.wral 2697   E.wrex 2698   _Vcvv 2948   [.wsbc 3153    i^i cin 3311    C_ wss 3312   (/)c0 3620   ~Pcpw 3791   {csn 3806   <.cop 3809   U.cuni 4007   class class class wbr 4204   {copab 4257    Or wor 4494    Fr wfr 4530    We wwe 4532    X. cxp 4868   `'ccnv 4869   dom cdm 4870   ran crn 4871   "cima 4873   Rel wrel 4875  (class class class)co 6073
This theorem is referenced by:  fpwwe2lem13  8509  fpwwe2  8510
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-riota 6541  df-recs 6625  df-oi 7471
  Copyright terms: Public domain W3C validator