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

Theorem fpwwe2lem12 8279
Description: Lemma for fpwwe2 8281. (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 2804 . . . . . . . . 9  |-  a  e. 
_V
32eldm 4892 . . . . . . . 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 8270 . . . . . . . . . . . . 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 606 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  (
a  C_  A  /\  s  C_  ( a  X.  a ) ) )
87simpld 445 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  a  C_  A )
92elpw 3644 . . . . . . . . . . 11  |-  ( a  e.  ~P A  <->  a  C_  A )
108, 9sylibr 203 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  a  e.  ~P A )
1110ex 423 . . . . . . . . 9  |-  ( ph  ->  ( a W s  ->  a  e.  ~P A ) )
1211exlimdv 1626 . . . . . . . 8  |-  ( ph  ->  ( E. s  a W s  ->  a  e.  ~P A ) )
133, 12syl5bi 208 . . . . . . 7  |-  ( ph  ->  ( a  e.  dom  W  ->  a  e.  ~P A ) )
1413ssrdv 3198 . . . . . 6  |-  ( ph  ->  dom  W  C_  ~P A )
15 sspwuni 4003 . . . . . 6  |-  ( dom 
W  C_  ~P A  <->  U.
dom  W  C_  A )
1614, 15sylib 188 . . . . 5  |-  ( ph  ->  U. dom  W  C_  A )
171, 16syl5eqss 3235 . . . 4  |-  ( ph  ->  X  C_  A )
18 vex 2804 . . . . . . . 8  |-  s  e. 
_V
1918elrn 4935 . . . . . . 7  |-  ( s  e.  ran  W  <->  E. a 
a W s )
207simprd 449 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( a  X.  a
) )
214relopabi 4827 . . . . . . . . . . . . . . . 16  |-  Rel  W
2221releldmi 4931 . . . . . . . . . . . . . . 15  |-  ( a W s  ->  a  e.  dom  W )
2322adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a W
s )  ->  a  e.  dom  W )
24 elssuni 3871 . . . . . . . . . . . . . 14  |-  ( a  e.  dom  W  -> 
a  C_  U. dom  W
)
2523, 24syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  a  C_ 
U. dom  W )
2625, 1syl6sseqr 3238 . . . . . . . . . . . 12  |-  ( (
ph  /\  a W
s )  ->  a  C_  X )
27 xpss12 4808 . . . . . . . . . . . 12  |-  ( ( a  C_  X  /\  a  C_  X )  -> 
( a  X.  a
)  C_  ( X  X.  X ) )
2826, 26, 27syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  a W
s )  ->  (
a  X.  a ) 
C_  ( X  X.  X ) )
2920, 28sstrd 3202 . . . . . . . . . 10  |-  ( (
ph  /\  a W
s )  ->  s  C_  ( X  X.  X
) )
3018elpw 3644 . . . . . . . . . 10  |-  ( s  e.  ~P ( X  X.  X )  <->  s  C_  ( X  X.  X
) )
3129, 30sylibr 203 . . . . . . . . 9  |-  ( (
ph  /\  a W
s )  ->  s  e.  ~P ( X  X.  X ) )
3231ex 423 . . . . . . . 8  |-  ( ph  ->  ( a W s  ->  s  e.  ~P ( X  X.  X
) ) )
3332exlimdv 1626 . . . . . . 7  |-  ( ph  ->  ( E. a  a W s  ->  s  e.  ~P ( X  X.  X ) ) )
3419, 33syl5bi 208 . . . . . 6  |-  ( ph  ->  ( s  e.  ran  W  ->  s  e.  ~P ( X  X.  X
) ) )
3534ssrdv 3198 . . . . 5  |-  ( ph  ->  ran  W  C_  ~P ( X  X.  X
) )
36 sspwuni 4003 . . . . 5  |-  ( ran 
W  C_  ~P ( X  X.  X )  <->  U. ran  W  C_  ( X  X.  X
) )
3735, 36sylib 188 . . . 4  |-  ( ph  ->  U. ran  W  C_  ( X  X.  X
) )
3817, 37jca 518 . . 3  |-  ( ph  ->  ( X  C_  A  /\  U. ran  W  C_  ( X  X.  X
) ) )
39 n0 3477 . . . . . . . . 9  |-  ( n  =/=  (/)  <->  E. y  y  e.  n )
40 ssel2 3188 . . . . . . . . . . . . . 14  |-  ( ( n  C_  X  /\  y  e.  n )  ->  y  e.  X )
4140adantl 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  -> 
y  e.  X )
421eleq2i 2360 . . . . . . . . . . . . . 14  |-  ( y  e.  X  <->  y  e.  U.
dom  W )
43 eluni2 3847 . . . . . . . . . . . . . 14  |-  ( y  e.  U. dom  W  <->  E. a  e.  dom  W  y  e.  a )
4442, 43bitri 240 . . . . . . . . . . . . 13  |-  ( y  e.  X  <->  E. a  e.  dom  W  y  e.  a )
4541, 44sylib 188 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  ->  E. a  e.  dom  W  y  e.  a )
462inex2 4172 . . . . . . . . . . . . . . . . . . 19  |-  ( n  i^i  a )  e. 
_V
4746a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( n  i^i  a
)  e.  _V )
486simplbda 607 . . . . . . . . . . . . . . . . . . . . 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 445 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  a W
s )  ->  s  We  a )
5049ad2ant2r 727 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
s  We  a )
51 wefr 4399 . . . . . . . . . . . . . . . . . . 19  |-  ( s  We  a  ->  s  Fr  a )
5250, 51syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
s  Fr  a )
53 inss2 3403 . . . . . . . . . . . . . . . . . . 19  |-  ( n  i^i  a )  C_  a
5453a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( n  i^i  a
)  C_  a )
55 simplrr 737 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  n )
56 simprr 733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
y  e.  a )
57 inelcm 3522 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  n  /\  y  e.  a )  ->  ( n  i^i  a
)  =/=  (/) )
5855, 56, 57syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
( n  i^i  a
)  =/=  (/) )
59 fri 4371 . . . . . . . . . . . . . . . . . 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 1183 . . . . . . . . . . . . . . . . 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 3402 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  i^i  a )  C_  n
62 simprl 732 . . . . . . . . . . . . . . . . . . . . 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 3191 . . . . . . . . . . . . . . . . . . . 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 737 . . . . . . . . . . . . . . . . . . . . . . 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 2566 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. z  e.  ( n  i^i  a )  -.  z
s v  <->  -.  E. z  e.  ( n  i^i  a
) z s v )
6664, 65sylib 188 . . . . . . . . . . . . . . . . . . . . . 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 4040 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w U. ran  W  v  <->  <. w ,  v >.  e.  U. ran  W )
68 eluni2 3847 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
w ,  v >.  e.  U. ran  W  <->  E. t  e.  ran  W <. w ,  v >.  e.  t )
6967, 68bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w U. ran  W  v  <->  E. t  e.  ran  W
<. w ,  v >.  e.  t )
70 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  t  e. 
_V
7170elrn 4935 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  ran  W  <->  E. b 
b W t )
72 df-br 4040 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w t v  <->  <. w ,  v >.  e.  t
)
73 simprll 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  ->  ph )
7776ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
78 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
n  C_  X  /\  y  e.  n )
)  /\  ( a W s  /\  y  e.  a ) )  -> 
a W s )
7978ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
80 simprlr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
81 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  b W t )
824, 5fpwwe2lem2 8270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
8382adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
8481, 83mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
8584simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( b  C_  A  /\  t  C_  (
b  X.  b ) ) )
8685simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  C_  (
b  X.  b ) )
8777, 79, 80, 86syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
8887ssbrd 4080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
8975, 88mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
90 brxp 4736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( w ( b  X.  b
) v  <->  ( w  e.  b  /\  v  e.  b ) )
9190simplbi 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( w ( b  X.  b
) v  ->  w  e.  b )
9289, 91syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
9392adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
9453, 62sseldi 3191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
9594ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
96 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
97 brinxp2 4767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( w ( t  i^i  (
b  X.  a ) ) v  <->  ( w  e.  b  /\  v  e.  a  /\  w
t v ) )
9893, 95, 96, 97syl3anbrc 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
99 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  /\  ( a W s  /\  y  e.  a ) )  /\  (
v  e.  ( n  i^i  a )  /\  A. z  e.  ( n  i^i  a )  -.  z s v ) )  /\  ( ( w  e.  n  /\  b W t )  /\  w t v ) )  /\  ( a 
C_  b  /\  s  =  ( t  i^i  ( b  X.  a
) ) ) )  ->  s  =  ( t  i^i  ( b  X.  a ) ) )
10099breqd 4050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
10198, 100mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
10277, 79, 20syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
103102adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
104103ssbrd 4080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
105101, 104mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
106 brxp 4736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w ( a  X.  a
) v  <->  ( w  e.  a  /\  v  e.  a ) )
107106simplbi 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w ( a  X.  a
) v  ->  w  e.  a )
108105, 107syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
109 elin 3371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  ( n  i^i  a )  <->  ( w  e.  n  /\  w  e.  a ) )
11074, 108, 109sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
111 breq1 4042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  w  ->  (
z s v  <->  w s
v ) )
112111rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( w  e.  ( n  i^i  a )  /\  w s v )  ->  E. z  e.  ( n  i^i  a ) z s v )
113110, 101, 112syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
11473adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
115 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
11692adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
117115, 116sseldd 3194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
118114, 117, 109sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
119 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
120 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
121 inss1 3402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( s  i^i  ( a  X.  b ) )  C_  s
122121a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )  ->  ( s  i^i  ( a  X.  b
) )  C_  s
)
123120, 122eqsstrd 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
124123ssbrd 4080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
125119, 124mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
126118, 125, 112syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
1275adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  A  e.  _V )
128 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  ( x  C_  A  /\  r  C_  ( x  X.  x
)  /\  r  We  x ) )  -> 
( x F r )  e.  A )
129128adantlr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( x  C_  A  /\  r  C_  (
x  X.  x )  /\  r  We  x
) )  ->  (
x F r )  e.  A )
130 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  a W s )
1314, 127, 129, 130, 81fpwwe2lem10 8277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
13277, 79, 80, 131syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
133113, 126, 132mpjaodan 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
134133expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
13572, 134syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
136135expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
137136exlimdv 1626 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
13871, 137syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
139138rexlimdv 2679 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
14069, 139syl5bi 208 . . . . . . . . . . . . . . . . . . . . . 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 ) )
14166, 140mtod 168 . . . . . . . . . . . . . . . . . . . . 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 )
142141ralrimiva 2639 . . . . . . . . . . . . . . . . . . . 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 )
14363, 142jca 518 . . . . . . . . . . . . . . . . . . 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 ) )
144143ex 423 . . . . . . . . . . . . . . . . . 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 ) ) )
145144reximdv2 2665 . . . . . . . . . . . . . . . . 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 ) )
14660, 145mpd 14 . . . . . . . . . . . . . . . 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 )
147146exp32 588 . . . . . . . . . . . . . . 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 ) ) )
148147exlimdv 1626 . . . . . . . . . . . . . 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 ) ) )
1493, 148syl5bi 208 . . . . . . . . . . . . 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 ) ) )
150149rexlimdv 2679 . . . . . . . . . . . 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 ) )
15145, 150mpd 14 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  C_  X  /\  y  e.  n ) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v )
152151expr 598 . . . . . . . . . 10  |-  ( (
ph  /\  n  C_  X
)  ->  ( y  e.  n  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
153152exlimdv 1626 . . . . . . . . 9  |-  ( (
ph  /\  n  C_  X
)  ->  ( E. y  y  e.  n  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
15439, 153syl5bi 208 . . . . . . . 8  |-  ( (
ph  /\  n  C_  X
)  ->  ( n  =/=  (/)  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
155154expimpd 586 . . . . . . 7  |-  ( ph  ->  ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
156155alrimiv 1621 . . . . . 6  |-  ( ph  ->  A. n ( ( n  C_  X  /\  n  =/=  (/) )  ->  E. v  e.  n  A. w  e.  n  -.  w U. ran  W  v ) )
157 df-fr 4368 . . . . . 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 ) )
158156, 157sylibr 203 . . . . 5  |-  ( ph  ->  U. ran  W  Fr  X )
1591eleq2i 2360 . . . . . . . . . 10  |-  ( w  e.  X  <->  w  e.  U.
dom  W )
160 eluni2 3847 . . . . . . . . . 10  |-  ( w  e.  U. dom  W  <->  E. b  e.  dom  W  w  e.  b )
161159, 160bitri 240 . . . . . . . . 9  |-  ( w  e.  X  <->  E. b  e.  dom  W  w  e.  b )
16244, 161anbi12i 678 . . . . . . . 8  |-  ( ( y  e.  X  /\  w  e.  X )  <->  ( E. a  e.  dom  W  y  e.  a  /\  E. b  e.  dom  W  w  e.  b )
)
163 reeanv 2720 . . . . . . . 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 ) )
164162, 163bitr4i 243 . . . . . . 7  |-  ( ( y  e.  X  /\  w  e.  X )  <->  E. a  e.  dom  W E. b  e.  dom  W ( y  e.  a  /\  w  e.  b ) )
165 vex 2804 . . . . . . . . . . . 12  |-  b  e. 
_V
166165eldm 4892 . . . . . . . . . . 11  |-  ( b  e.  dom  W  <->  E. t 
b W t )
1673, 166anbi12i 678 . . . . . . . . . 10  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  ( E. s 
a W s  /\  E. t  b W t ) )
168 eeanv 1866 . . . . . . . . . 10  |-  ( E. s E. t ( a W s  /\  b W t )  <->  ( E. s  a W s  /\  E. t  b W t ) )
169167, 168bitr4i 243 . . . . . . . . 9  |-  ( ( a  e.  dom  W  /\  b  e.  dom  W )  <->  E. s E. t
( a W s  /\  b W t ) )
17084simprd 449 . . . . . . . . . . . . . . . . 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 ) )
171170simpld 445 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  We  b
)
172171ad2antrr 706 . . . . . . . . . . . . . . 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 )
173 weso 4400 . . . . . . . . . . . . . . 15  |-  ( t  We  b  ->  t  Or  b )
174172, 173syl 15 . . . . . . . . . . . . . 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 )
175 simprl 732 . . . . . . . . . . . . . . 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 )
176 simplrl 736 . . . . . . . . . . . . . . 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 )
177175, 176sseldd 3194 . . . . . . . . . . . . . 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 )
178 simplrr 737 . . . . . . . . . . . . . 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 )
179 solin 4353 . . . . . . . . . . . . . 14  |-  ( ( t  Or  b  /\  ( y  e.  b  /\  w  e.  b ) )  ->  (
y t w  \/  y  =  w  \/  w t y ) )
180174, 177, 178, 179syl12anc 1180 . . . . . . . . . . . . 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 ) )
18121relelrni 4932 . . . . . . . . . . . . . . . . . 18  |-  ( b W t  ->  t  e.  ran  W )
182181ad2antll 709 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  t  e.  ran  W )
183182ad2antrr 706 . . . . . . . . . . . . . . . 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
)
184 elssuni 3871 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ran  W  -> 
t  C_  U. ran  W
)
185183, 184syl 15 . . . . . . . . . . . . . . 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
)
186185ssbrd 4080 . . . . . . . . . . . . . 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 ) )
187 idd 21 . . . . . . . . . . . . . 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 ) )
188185ssbrd 4080 . . . . . . . . . . . . . 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 ) )
189186, 187, 1883orim123d 1260 . . . . . . . . . . . . 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 ) ) )
190180, 189mpd 14 . . . . . . . . . . . 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 ) )
19149adantrr 697 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  We  a
)
192191ad2antrr 706 . . . . . . . . . . . . . . 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 )
193 weso 4400 . . . . . . . . . . . . . . 15  |-  ( s  We  a  ->  s  Or  a )
194192, 193syl 15 . . . . . . . . . . . . . 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 )
195 simplrl 736 . . . . . . . . . . . . . 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 )
196 simprl 732 . . . . . . . . . . . . . . 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 )
197 simplrr 737 . . . . . . . . . . . . . . 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 )
198196, 197sseldd 3194 . . . . . . . . . . . . . 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 )
199 solin 4353 . . . . . . . . . . . . . 14  |-  ( ( s  Or  a  /\  ( y  e.  a  /\  w  e.  a ) )  ->  (
y s w  \/  y  =  w  \/  w s y ) )
200194, 195, 198, 199syl12anc 1180 . . . . . . . . . . . . 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 ) )
20121relelrni 4932 . . . . . . . . . . . . . . . . . 18  |-  ( a W s  ->  s  e.  ran  W )
202201ad2antrl 708 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  e.  ran  W )
203202ad2antrr 706 . . . . . . . . . . . . . . . 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
)
204 elssuni 3871 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ran  W  -> 
s  C_  U. ran  W
)
205203, 204syl 15 . . . . . . . . . . . . . . 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
)
206205ssbrd 4080 . . . . . . . . . . . . . 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 ) )
207 idd 21 . . . . . . . . . . . . . 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 ) )
208205ssbrd 4080 . . . . . . . . . . . . . 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 ) )
209206, 207, 2083orim123d 1260 . . . . . . . . . . . . 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 ) ) )
210200, 209mpd 14 . . . . . . . . . . . 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 ) )
211131adantr 451 . . . . . . . . . . . 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
) ) ) ) )
212190, 210, 211mpjaodan 761 . . . . . . . . . . 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 ) )
213212exp31 587 . . . . . . . . . 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 ) ) ) )
214213exlimdvv 1627 . . . . . . . . 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 ) ) ) )
215169, 214syl5bi 208 . . . . . . . 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 ) ) ) )
216215rexlimdvv 2686 . . . . . . 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 ) ) )
217164, 216syl5bi 208 . . . . . 6  |-  ( ph  ->  ( ( y  e.  X  /\  w  e.  X )  ->  (
y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) ) )
218217ralrimivv 2647 . . . . 5  |-  ( ph  ->  A. y  e.  X  A. w  e.  X  ( y U. ran  W  w  \/  y  =  w  \/  w U. ran  W  y ) )
219 dfwe2 4589 . . . . 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 ) ) )
220158, 218, 219sylanbrc 645 . . . 4  |-  ( ph  ->  U. ran  W  We  X )
2214fpwwe2cbv 8268 . . . . . . . . . . . . 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 ) ) }
2225adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  A  e.  _V )
223 simpr 447 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a W
s )  ->  a W s )
224221, 222, 223fpwwe2lem3 8271 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a W s )  /\  y  e.  a )  ->  ( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
225224anasss 628 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( `' s
" { y } ) F ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) ) )  =  y )
226 cnvimass 5049 . . . . . . . . . . . . 13  |-  ( `'
U. ran  W " {
y } )  C_  dom  U. ran  W
227 ssexg 4176 . . . . . . . . . . . . . . . . . 18  |-  ( ( X  C_  A  /\  A  e.  _V )  ->  X  e.  _V )
22817, 5, 227syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  _V )
229 xpexg 4816 . . . . . . . . . . . . . . . . 17  |-  ( ( X  e.  _V  /\  X  e.  _V )  ->  ( X  X.  X
)  e.  _V )
230228, 228, 229syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  X.  X
)  e.  _V )
231 ssexg 4176 . . . . . . . . . . . . . . . 16  |-  ( ( U. ran  W  C_  ( X  X.  X
)  /\  ( X  X.  X )  e.  _V )  ->  U. ran  W  e. 
_V )
23237, 230, 231syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U. ran  W  e. 
_V )
233232adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  U. ran  W  e.  _V )
234 dmexg 4955 . . . . . . . . . . . . . 14  |-  ( U. ran  W  e.  _V  ->  dom  U. ran  W  e.  _V )
235233, 234syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  dom  U. ran  W  e. 
_V )
236 ssexg 4176 . . . . . . . . . . . . 13  |-  ( ( ( `' U. ran  W
" { y } )  C_  dom  U. ran  W  /\  dom  U. ran  W  e.  _V )  -> 
( `' U. ran  W
" { y } )  e.  _V )
237226, 235, 236sylancr 644 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( `' U. ran  W
" { y } )  e.  _V )
238 id 19 . . . . . . . . . . . . . . 15  |-  ( u  =  ( `' U. ran  W " { y } )  ->  u  =  ( `' U. ran  W " { y } ) )
239 olc 373 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  y  ->  (
w s y  \/  w  =  y ) )
240 df-br 4040 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z U. ran  W  w  <->  <. z ,  w >.  e. 
U. ran  W )
241 eluni2 3847 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
z ,  w >.  e. 
U. ran  W  <->  E. t  e.  ran  W <. z ,  w >.  e.  t
)
242240, 241bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z U. ran  W  w  <->  E. t  e.  ran  W
<. z ,  w >.  e.  t )
243 df-br 4040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z t w  <->  <. z ,  w >.  e.  t
)
24486ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
245244ssbrd 4080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
246 brxp 4736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( z ( b  X.  b
) w  <->  ( z  e.  b  /\  w  e.  b ) )
247246simplbi 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( z ( b  X.  b
) w  ->  z  e.  b )
248245, 247syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
24920adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  s  C_  (
a  X.  a ) )
250249ssbrd 4080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( w s y  ->  w (
a  X.  a ) y ) )
251250imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  w (
a  X.  a ) y )
252 brxp 4736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( w ( a  X.  a
) y  <->  ( w  e.  a  /\  y  e.  a ) )
253252simplbi 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( w ( a  X.  a
) y  ->  w  e.  a )
254251, 253syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  w  e.  a )
255254a1d 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w s y )  ->  ( y  e.  a  ->  w  e.  a ) )
256 elequ1 1699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( w  =  y  ->  (
w  e.  a  <->  y  e.  a ) )
257256biimprd 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( w  =  y  ->  (
y  e.  a  ->  w  e.  a )
)
258257adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  w  =  y )  ->  ( y  e.  a  ->  w  e.  a ) )
259255, 258jaodan 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( w s y  \/  w  =  y ) )  -> 
( y  e.  a  ->  w  e.  a ) )
260259impr 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  w  e.  a )
261260adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
262248, 261jctird 528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
263 brxp 4736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z ( b  X.  a
) w  <->  ( z  e.  b  /\  w  e.  a ) )
264262, 263syl6ibr 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
265264ancld 536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
266 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
267266breqd 4050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
268 brin 4086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( z ( t  i^i  (
b  X.  a ) ) w  <->  ( z
t w  /\  z
( b  X.  a
) w ) )
269267, 268syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
270265, 269sylibrd 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
271 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
272121a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )  ->  ( s  i^i  ( a  X.  b
) )  C_  s
)
273271, 272eqsstrd 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
274273ssbrd 4080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
275131adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
276270, 274, 275mpjaodan 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( z
t w  ->  z
s w ) )
277243, 276syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  (
a W s  /\  b W t ) )  /\  ( ( w s y  \/  w  =  y )  /\  y  e.  a )
)  ->  ( <. z ,  w >.  e.  t  ->  z s w ) )
278277exp32 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( a W s  /\  b W t ) )  ->  ( ( w s y  \/  w  =  y )  -> 
( y  e.  a  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) ) )
279278expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  a W
s )  ->  (
b W t  -> 
( ( w s y  \/  w  =  y )  ->  (
y  e.  a  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
280279com24 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  a W
s )  ->  (
y  e.  a  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) ) )
281280impr 602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( ( w s y  \/  w  =  y )  ->  (
b W t  -> 
( <. z ,  w >.  e.  t  ->  z
s w ) ) ) )
282281imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( b W t  ->  ( <. z ,  w >.  e.  t  ->  z s w ) ) )
283282exlimdv 1626 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
28471, 283syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( t  e. 
ran  W  ->  ( <.
z ,  w >.  e.  t  ->  z s
w ) ) )
285284rexlimdv 2679 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
286242, 285syl5bi 208 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( w
s y  \/  w  =  y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
287239, 286sylan2 460 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w  =  y )  ->  (
z U. ran  W  w  ->  z s w ) )
288287ex 423 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( w  =  y  ->  ( z U. ran  W  w  ->  z
s w ) ) )
289288alrimiv 1621 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) ) )
290 vex 2804 . . . . . . . . . . . . . . . . . . . 20  |-  y  e. 
_V
291 breq2 4043 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z U. ran  W  w 
<->  z U. ran  W  y ) )
292 breq2 4043 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  y  ->  (
z s w  <->  z s
y ) )
293291, 292imbi12d 311 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  y  ->  (
( z U. ran  W  w  ->  z s
w )  <->  ( z U. ran  W  y  -> 
z s y ) ) )
294290, 293ceqsalv 2827 . . . . . . . . . . . . . . . . . . 19  |-  ( A. w ( w  =  y  ->  ( z U. ran  W  w  -> 
z s w ) )  <->  ( z U. ran  W  y  ->  z
s y ) )
295289, 294sylib 188 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  ->  z s
y ) )
296201ad2antrl 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
s  e.  ran  W
)
297296, 204syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
s  C_  U. ran  W
)
298297ssbrd 4080 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z s y  ->  z U. ran  W  y ) )
299295, 298impbid 183 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z U. ran  W  y  <->  z s y ) )
300 vex 2804 . . . . . . . . . . . . . . . . . . 19  |-  z  e. 
_V
301300eliniseg 5058 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  _V  ->  (
z  e.  ( `'
U. ran  W " {
y } )  <->  z U. ran  W  y ) )
302290, 301ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( `' U. ran  W " { y } )  <->  z U. ran  W  y )
303300eliniseg 5058 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  _V  ->  (
z  e.  ( `' s " { y } )  <->  z s
y ) )
304290, 303ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( `' s
" { y } )  <->  z s y )
305299, 302, 3043bitr4g 279 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( z  e.  ( `' U. ran  W " { y } )  <-> 
z  e.  ( `' s " { y } ) ) )
306305eqrdv 2294 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  -> 
( `' U. ran  W
" { y } )  =  ( `' s " { y } ) )
307238, 306sylan9eqr 2350 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  u  =  ( `' s " {
y } ) )
308307, 307xpeq12d 4730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  u  =  ( `' U. ran  W " { y } ) )  ->  ( u  X.  u )  =  ( ( `' s " { y } )  X.  ( `' s
" { y } ) ) )
309308ineq2d 3383 . . . . . . . . . . . . . . 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 } ) ) ) )
310 inss2 3403 . . . . . . . . . . . . . . . . . 18  |-  ( U. ran  W  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )  C_  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
311 relxp 4810 . . . . . . . . . . . . . . . . . 18  |-  Rel  (
( `' s " { y } )  X.  ( `' s
" { y } ) )
312 relss 4791 . . . . . . . . . . . . . . . . . 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 } ) ) ) ) )
313310, 311, 312mp2 17 . . . . . . . . . . . . . . . . 17  |-  Rel  ( U. ran  W  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) )
314 inss2 3403 . . . . . . . . . . . . . . . . . 18  |-  ( s  i^i  ( ( `' s " { y } )  X.  ( `' s " {
y } ) ) )  C_  ( ( `' s " {
y } )  X.  ( `' s " { y } ) )
315 relss 4791 . . . . . . . . . . . . . . . . . 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 } ) ) ) ) )
316314, 311, 315mp2 17 . . . . . . . . . . . . . . . . 17  |-  Rel  (
s  i^i  ( ( `' s " {
y } )  X.  ( `' s " { y } ) ) )
317 vex 2804 . . . . . . . . . . . . . . . . . . . . . . 23  |-  w  e. 
_V
318317eliniseg 5058 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  _V  ->  (
w  e.  ( `' s " { y } )  <->  w s
y ) )
319303, 318anbi12d 691 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  _V  ->  (
( z  e.  ( `' s " {
y } )  /\  w  e.  ( `' s " { y } ) )  <->  ( z
s y  /\  w
s y ) ) )
320290, 319ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } ) )  <->  ( z s y  /\  w s y ) )
321 orc 374 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w s y  ->  (
w s y  \/  w  =  y ) )
322321, 286sylan2 460 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  w s
y )  ->  (
z U. ran  W  w  ->  z s w ) )
323322adantrl 696 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  ->  z
s w ) )
324297adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  s  C_  U. ran  W )
325324ssbrd 4080 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z s w  ->  z U. ran  W  w ) )
326323, 325impbid 183 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z
s y  /\  w
s y ) )  ->  ( z U. ran  W  w  <->  z s
w ) )
327320, 326sylan2b 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
a W s  /\  y  e.  a )
)  /\  ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " {
y } ) ) )  ->  ( z U. ran  W  w  <->  z s
w ) )
328327pm5.32da 622 . . . . . . . . . . . . . . . . . 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 ) ) )
329 brinxp2 4767 . . . . . . . . . . . . . . . . . . 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 ) )
330 df-br 4040 . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
331 df-3an 936 . . . . . . . . . . . . . . . . . . 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 ) )
332329, 330, 3313bitr3i 266 . . . . . . . . . . . . . . . . . 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 ) )
333 brinxp2 4767 . . . . . . . . . . . . . . . . . . 19  |-  ( z ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) w  <-> 
( z  e.  ( `' s " {
y } )  /\  w  e.  ( `' s " { y } )  /\  z s w ) )
334 df-br 4040 . . . . . . . . . . . . . . . . . . 19  |-  ( z ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) w  <->  <. z ,  w >.  e.  ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) ) )
335 df-3an 936 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } )  /\  z s w )  <->  ( ( z  e.  ( `' s
" { y } )  /\  w  e.  ( `' s " { y } ) )  /\  z s w ) )
336333, 334, 3353bitr3i 266 . . . . . . . . . . . . . . . . . 18  |-  ( <.
z ,  w >.  e.  ( s  i^i  (
( `' s " { y } )  X.  ( `' s
" { y } ) ) )  <->  ( (
z  e.  ( `' s " { y } )  /\  w  e.  ( `' s " { y } ) )  /\  z s w ) )
337328, 332, 3363bitr4g 279 . . . . . . . . . . . . . . . . 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 } ) ) ) ) )
338313, 316, 337eqrelrdv 4799 . . . . . . . . . . . . . . . 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 } ) ) ) )
339338adantr 451 . . . . . . . . . . . . . . 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 } ) ) ) )
340309, 339eqtrd 2328 . . . . . . . . . . . . . 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 } ) ) ) )
341307, 340oveq12d 5892 . . . . . . . . . . . . 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 } ) ) ) ) )
342341eqeq1d 2304 . . . . . . . . . . . 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 ) )
343237, 342sbcied 3040 . . . . . . . . . . 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 ) )
344225, 343mpbird 223 . . . . . . . . . 10  |-  ( (
ph  /\  ( a W s  /\  y  e.  a ) )  ->  [. ( `' U. ran  W
" { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y )
345344exp32 588 . . . . . . . . 9  |-  ( ph  ->  ( a W s  ->  ( y  e.  a  ->  [. ( `'
U. ran  W " {
y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) ) )
346345exlimdv 1626 . . . . . . . 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 ) ) )
3473, 346syl5bi 208 . . . . . . 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 ) ) )
348347rexlimdv 2679 . . . . . 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 ) )
34944, 348syl5bi 208 . . . . 5  |-  ( ph  ->  ( y  e.  X  ->  [. ( `' U. ran  W " { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y ) )
350349ralrimiv 2638 . . . 4  |-  ( ph  ->  A. y  e.  X  [. ( `' U. ran  W
" { y } )  /  u ]. ( u F ( U. ran  W  i^i  ( u  X.  u
) ) )  =  y )
351220, 350jca 518 . . 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 ) )
3524, 5fpwwe2lem2 8270 . . 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 ) ) ) )
35338, 351, 352mpbir2and 888 . 2  |-  ( ph  ->  X W U. ran  W )
35421releldmi 4931 . 2  |-  ( X W U. ran  W  ->  X  e.  dom  W
)
355353, 354syl 15 1  |-  ( ph  ->  X  e.  dom  W
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    \/ w3o 933    /\ w3a 934   A.wal 1530   E.wex 1531    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556   E.wrex 2557   _Vcvv 2801   [.wsbc 3004    i^i cin 3164    C_ wss 3165   (/)c0 3468   ~Pcpw 3638   {csn 3653   <.cop 3656   U.cuni 3843   class class class wbr 4039   {copab 4092    Or wor 4329    Fr wfr 4365    We wwe 4367    X. cxp 4703   `'ccnv 4704   dom cdm 4705   ran crn 4706   "cima 4708   Rel wrel 4710  (class class class)co 5874
This theorem is referenced by:  fpwwe2lem13  8280  fpwwe2  8281
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-riota 6320  df-recs 6404  df-oi 7241
  Copyright terms: Public domain W3C validator