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

Theorem fpwwe2lem13 9068
Description: Lemma for fpwwe2 9069. (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
fpwwe2lem13  |-  ( ph  ->  ( X F ( W `  X ) )  e.  X )
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 fpwwe2lem13
Dummy variables  a 
b  s  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssun2 3630 . . . 4  |-  { ( X F ( W `
 X ) ) }  C_  ( X  u.  { ( X F ( W `  X
) ) } )
2 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 ) ) }
3 fpwwe2.2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  _V )
43adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  A  e.  _V )
5 fpwwe2.3 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  C_  A  /\  r  C_  ( x  X.  x
)  /\  r  We  x ) )  -> 
( x F r )  e.  A )
65adantlr 719 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  C_  A  /\  r  C_  ( x  X.  x )  /\  r  We  x ) )  -> 
( x F r )  e.  A )
7 fpwwe2.4 . . . . . . . . . . . . . 14  |-  X  = 
U. dom  W
82, 4, 6, 7fpwwe2lem12 9067 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  e.  dom  W )
92, 4, 6, 7fpwwe2lem11 9066 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  W : dom  W --> ~P ( X  X.  X ) )
10 ffun 5745 . . . . . . . . . . . . . 14  |-  ( W : dom  W --> ~P ( X  X.  X )  ->  Fun  W )
11 funfvbrb 6007 . . . . . . . . . . . . . 14  |-  ( Fun 
W  ->  ( X  e.  dom  W  <->  X W
( W `  X
) ) )
129, 10, 113syl 18 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  e.  dom  W  <->  X W
( W `  X
) ) )
138, 12mpbid 213 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X W ( W `  X ) )
142, 4fpwwe2lem2 9058 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X W ( W `  X )  <->  ( ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
) )  /\  (
( W `  X
)  We  X  /\  A. y  e.  X  [. ( `' ( W `  X ) " {
y } )  /  u ]. ( u F ( ( W `  X )  i^i  (
u  X.  u ) ) )  =  y ) ) ) )
1513, 14mpbid 213 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( X  C_  A  /\  ( W `  X
)  C_  ( X  X.  X ) )  /\  ( ( W `  X )  We  X  /\  A. y  e.  X  [. ( `' ( W `
 X ) " { y } )  /  u ]. (
u F ( ( W `  X )  i^i  ( u  X.  u ) ) )  =  y ) ) )
1615simpld 460 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
) ) )
1716simpld 460 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  C_  A )
1816simprd 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  C_  ( X  X.  X
) )
1915simprd 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  We  X  /\  A. y  e.  X  [. ( `' ( W `  X ) " {
y } )  /  u ]. ( u F ( ( W `  X )  i^i  (
u  X.  u ) ) )  =  y ) )
2019simpld 460 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  We  X )
2117, 18, 203jca 1185 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )
222, 3, 5fpwwe2lem5 9060 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  C_  A  /\  ( W `
 X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )  ->  ( X F ( W `  X ) )  e.  A )
2321, 22syldan 472 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X F ( W `  X ) )  e.  A )
2423snssd 4142 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  { ( X F ( W `
 X ) ) }  C_  A )
2517, 24unssd 3642 . . . . . . . 8  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  u.  { ( X F ( W `  X ) ) } )  C_  A )
26 ssun1 3629 . . . . . . . . . . 11  |-  X  C_  ( X  u.  { ( X F ( W `
 X ) ) } )
27 xpss12 4956 . . . . . . . . . . 11  |-  ( ( X  C_  ( X  u.  { ( X F ( W `  X
) ) } )  /\  X  C_  ( X  u.  { ( X F ( W `  X ) ) } ) )  ->  ( X  X.  X )  C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  {
( X F ( W `  X ) ) } ) ) )
2826, 26, 27mp2an 676 . . . . . . . . . 10  |-  ( X  X.  X )  C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  {
( X F ( W `  X ) ) } ) )
2918, 28syl6ss 3476 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  {
( X F ( W `  X ) ) } ) ) )
30 xpss12 4956 . . . . . . . . . . 11  |-  ( ( X  C_  ( X  u.  { ( X F ( W `  X
) ) } )  /\  { ( X F ( W `  X ) ) } 
C_  ( X  u.  { ( X F ( W `  X ) ) } ) )  ->  ( X  X.  { ( X F ( W `  X
) ) } ) 
C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  { ( X F ( W `  X ) ) } ) ) )
3126, 1, 30mp2an 676 . . . . . . . . . 10  |-  ( X  X.  { ( X F ( W `  X ) ) } )  C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  { ( X F ( W `  X ) ) } ) )
3231a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  { ( X F ( W `  X ) ) } ) ) )
3329, 32unssd 3642 . . . . . . . 8  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  C_  (
( X  u.  {
( X F ( W `  X ) ) } )  X.  ( X  u.  {
( X F ( W `  X ) ) } ) ) )
3425, 33jca 534 . . . . . . 7  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( X  u.  {
( X F ( W `  X ) ) } )  C_  A  /\  ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) 
C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  { ( X F ( W `  X ) ) } ) ) ) )
35 ssdif0 3851 . . . . . . . . . . . . . 14  |-  ( x 
C_  { ( X F ( W `  X ) ) }  <-> 
( x  \  {
( X F ( W `  X ) ) } )  =  (/) )
36 simpllr 767 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  -.  ( X F ( W `  X ) )  e.  X )
3718ad2antrr 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  ( W `  X )  C_  ( X  X.  X ) )
3837ssbrd 4462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  ( ( X F ( W `  X ) ) ( W `  X ) ( X F ( W `  X ) )  ->  ( X F ( W `  X ) ) ( X  X.  X ) ( X F ( W `  X ) ) ) )
39 brxp 4881 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) ( X F ( W `  X
) )  <->  ( ( X F ( W `  X ) )  e.  X  /\  ( X F ( W `  X ) )  e.  X ) )
4039simplbi 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) ( X F ( W `  X
) )  ->  ( X F ( W `  X ) )  e.  X )
4138, 40syl6 34 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  ( ( X F ( W `  X ) ) ( W `  X ) ( X F ( W `  X ) )  ->  ( X F ( W `  X ) )  e.  X ) )
4236, 41mtod 180 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  -.  ( X F ( W `  X ) ) ( W `  X ) ( X F ( W `  X ) ) )
43 brxp 4881 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) ( X F ( W `
 X ) )  <-> 
( ( X F ( W `  X
) )  e.  X  /\  ( X F ( W `  X ) )  e.  { ( X F ( W `
 X ) ) } ) )
4443simplbi 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) ( X F ( W `
 X ) )  ->  ( X F ( W `  X
) )  e.  X
)
4536, 44nsyl 124 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  -.  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `
 X ) ) } ) ( X F ( W `  X ) ) )
46 ovex 6330 . . . . . . . . . . . . . . . . . . 19  |-  ( X F ( W `  X ) )  e. 
_V
47 breq2 4424 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( X F ( W `  X
) )  ->  (
( X F ( W `  X ) ) ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  ( X F ( W `  X
) ) ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) ( X F ( W `  X
) ) ) )
48 brun 4469 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( X F ( W `
 X ) ) ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) ( X F ( W `  X ) )  <->  ( ( X F ( W `  X ) ) ( W `  X ) ( X F ( W `  X ) )  \/  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `
 X ) ) } ) ( X F ( W `  X ) ) ) )
4947, 48syl6bb 264 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( X F ( W `  X
) )  ->  (
( X F ( W `  X ) ) ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  ( ( X F ( W `  X ) ) ( W `  X ) ( X F ( W `  X ) )  \/  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `
 X ) ) } ) ( X F ( W `  X ) ) ) ) )
5049notbid 295 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( X F ( W `  X
) )  ->  ( -.  ( X F ( W `  X ) ) ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  -.  ( ( X F ( W `  X ) ) ( W `  X ) ( X F ( W `  X ) )  \/  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `
 X ) ) } ) ( X F ( W `  X ) ) ) ) )
5146, 50rexsn 4036 . . . . . . . . . . . . . . . . . 18  |-  ( E. y  e.  { ( X F ( W `
 X ) ) }  -.  ( X F ( W `  X ) ) ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  <->  -.  (
( X F ( W `  X ) ) ( W `  X ) ( X F ( W `  X ) )  \/  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `  X
) ) } ) ( X F ( W `  X ) ) ) )
52 ioran 492 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( X F ( W `  X
) ) ( W `
 X ) ( X F ( W `
 X ) )  \/  ( X F ( W `  X
) ) ( X  X.  { ( X F ( W `  X ) ) } ) ( X F ( W `  X
) ) )  <->  ( -.  ( X F ( W `
 X ) ) ( W `  X
) ( X F ( W `  X
) )  /\  -.  ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) ( X F ( W `
 X ) ) ) )
5351, 52bitri 252 . . . . . . . . . . . . . . . . 17  |-  ( E. y  e.  { ( X F ( W `
 X ) ) }  -.  ( X F ( W `  X ) ) ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  <->  ( -.  ( X F ( W `
 X ) ) ( W `  X
) ( X F ( W `  X
) )  /\  -.  ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) ( X F ( W `
 X ) ) ) )
5442, 45, 53sylanbrc 668 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  E. y  e.  { ( X F ( W `  X
) ) }  -.  ( X F ( W `
 X ) ) ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )
55 simplrr 769 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  x  =/=  (/) )
5655neneqd 2625 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  -.  x  =  (/) )
57 simpr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  x  C_  { ( X F ( W `
 X ) ) } )
58 sssn 4155 . . . . . . . . . . . . . . . . . . . 20  |-  ( x 
C_  { ( X F ( W `  X ) ) }  <-> 
( x  =  (/)  \/  x  =  { ( X F ( W `
 X ) ) } ) )
5957, 58sylib 199 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  ( x  =  (/)  \/  x  =  { ( X F ( W `  X
) ) } ) )
6059ord 378 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  ( -.  x  =  (/)  ->  x  =  { ( X F ( W `  X
) ) } ) )
6156, 60mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  x  =  { ( X F ( W `  X
) ) } )
6261raleqdv 3031 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  ( A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  A. z  e.  {
( X F ( W `  X ) ) }  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
63 breq1 4423 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  ( X F ( W `  X
) )  ->  (
z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  ( X F ( W `  X
) ) ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y ) )
6463notbid 295 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  ( X F ( W `  X
) )  ->  ( -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  -.  ( X F ( W `  X ) ) ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
6546, 64ralsn 4035 . . . . . . . . . . . . . . . . . 18  |-  ( A. z  e.  { ( X F ( W `  X ) ) }  -.  z ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  <->  -.  ( X F ( W `  X ) ) ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )
6662, 65syl6bb 264 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  ( A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  -.  ( X F ( W `  X ) ) ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
6761, 66rexeqbidv 3040 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  ( E. y  e.  x  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  E. y  e.  {
( X F ( W `  X ) ) }  -.  ( X F ( W `  X ) ) ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
6854, 67mpbird 235 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  x  C_  { ( X F ( W `  X ) ) } )  ->  E. y  e.  x  A. z  e.  x  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )
6968ex 435 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  ->  (
x  C_  { ( X F ( W `  X ) ) }  ->  E. y  e.  x  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) )
7035, 69syl5bir 221 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  ->  (
( x  \  {
( X F ( W `  X ) ) } )  =  (/)  ->  E. y  e.  x  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) )
71 vex 3084 . . . . . . . . . . . . . . . . 17  |-  x  e. 
_V
72 difexg 4569 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  _V  ->  (
x  \  { ( X F ( W `  X ) ) } )  e.  _V )
7371, 72mp1i 13 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  -> 
( x  \  {
( X F ( W `  X ) ) } )  e. 
_V )
74 wefr 4840 . . . . . . . . . . . . . . . . . 18  |-  ( ( W `  X )  We  X  ->  ( W `  X )  Fr  X )
7520, 74syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  Fr  X )
7675ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  -> 
( W `  X
)  Fr  X )
77 simplrl 768 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  ->  x  C_  ( X  u.  { ( X F ( W `  X ) ) } ) )
78 uncom 3610 . . . . . . . . . . . . . . . . . 18  |-  ( X  u.  { ( X F ( W `  X ) ) } )  =  ( { ( X F ( W `  X ) ) }  u.  X
)
7977, 78syl6sseq 3510 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  ->  x  C_  ( { ( X F ( W `
 X ) ) }  u.  X ) )
80 ssundif 3879 . . . . . . . . . . . . . . . . 17  |-  ( x 
C_  ( { ( X F ( W `
 X ) ) }  u.  X )  <-> 
( x  \  {
( X F ( W `  X ) ) } )  C_  X )
8179, 80sylib 199 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  -> 
( x  \  {
( X F ( W `  X ) ) } )  C_  X )
82 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  -> 
( x  \  {
( X F ( W `  X ) ) } )  =/=  (/) )
83 fri 4812 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( x  \  { ( X F ( W `  X
) ) } )  e.  _V  /\  ( W `  X )  Fr  X )  /\  (
( x  \  {
( X F ( W `  X ) ) } )  C_  X  /\  ( x  \  { ( X F ( W `  X
) ) } )  =/=  (/) ) )  ->  E. y  e.  (
x  \  { ( X F ( W `  X ) ) } ) A. z  e.  ( x  \  {
( X F ( W `  X ) ) } )  -.  z ( W `  X ) y )
8473, 76, 81, 82, 83syl22anc 1265 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  ->  E. y  e.  (
x  \  { ( X F ( W `  X ) ) } ) A. z  e.  ( x  \  {
( X F ( W `  X ) ) } )  -.  z ( W `  X ) y )
85 brun 4469 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  <->  ( z
( W `  X
) y  \/  z
( X  X.  {
( X F ( W `  X ) ) } ) y ) )
86 idd 25 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( z
( W `  X
) y  ->  z
( W `  X
) y ) )
87 brxp 4881 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( z  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
8887simprbi 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  e.  {
( X F ( W `  X ) ) } )
89 eldifn 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  -.  y  e.  { ( X F ( W `  X ) ) } )
9089adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  -.  y  e.  { ( X F ( W `  X
) ) } )
9190pm2.21d 109 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( y  e.  { ( X F ( W `  X
) ) }  ->  z ( W `  X
) y ) )
9288, 91syl5 33 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( z
( X  X.  {
( X F ( W `  X ) ) } ) y  ->  z ( W `
 X ) y ) )
9386, 92jaod 381 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( (
z ( W `  X ) y  \/  z ( X  X.  { ( X F ( W `  X
) ) } ) y )  ->  z
( W `  X
) y ) )
9485, 93syl5bi 220 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  -> 
z ( W `  X ) y ) )
9594con3d 138 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( -.  z ( W `  X ) y  ->  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) )
9695ralimdv 2835 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( A. z  e.  ( x  \  { ( X F ( W `  X
) ) } )  -.  z ( W `
 X ) y  ->  A. z  e.  ( x  \  { ( X F ( W `
 X ) ) } )  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
97 simpr 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  -.  ( X F ( W `
 X ) )  e.  X )
9897ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  -.  ( X F ( W `  X ) )  e.  X )
9918ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( W `  X )  C_  ( X  X.  X ) )
10099ssbrd 4462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( ( X F ( W `  X ) ) ( W `  X ) y  ->  ( X F ( W `  X ) ) ( X  X.  X ) y ) )
101 brxp 4881 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) y  <->  ( ( X F ( W `  X ) )  e.  X  /\  y  e.  X ) )
102101simplbi 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) y  ->  ( X F ( W `  X ) )  e.  X )
103100, 102syl6 34 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( ( X F ( W `  X ) ) ( W `  X ) y  ->  ( X F ( W `  X ) )  e.  X ) )
10498, 103mtod 180 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  -.  ( X F ( W `  X ) ) ( W `  X ) y )
105 brxp 4881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( ( X F ( W `  X
) )  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
106105simprbi 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  e.  {
( X F ( W `  X ) ) } )
10790, 106nsyl 124 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  -.  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `
 X ) ) } ) y )
108 brun 4469 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( X F ( W `
 X ) ) ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  <->  ( ( X F ( W `  X ) ) ( W `  X ) y  \/  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `
 X ) ) } ) y ) )
10963, 108syl6bb 264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  ( X F ( W `  X
) )  ->  (
z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  ( ( X F ( W `  X ) ) ( W `  X ) y  \/  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `
 X ) ) } ) y ) ) )
110109notbid 295 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  ( X F ( W `  X
) )  ->  ( -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  <->  -.  ( ( X F ( W `  X ) ) ( W `  X ) y  \/  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `
 X ) ) } ) y ) ) )
11146, 110ralsn 4035 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. z  e.  { ( X F ( W `  X ) ) }  -.  z ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  <->  -.  (
( X F ( W `  X ) ) ( W `  X ) y  \/  ( X F ( W `  X ) ) ( X  X.  { ( X F ( W `  X
) ) } ) y ) )
112 ioran 492 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  ( ( X F ( W `  X
) ) ( W `
 X ) y  \/  ( X F ( W `  X
) ) ( X  X.  { ( X F ( W `  X ) ) } ) y )  <->  ( -.  ( X F ( W `
 X ) ) ( W `  X
) y  /\  -.  ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) y ) )
113111, 112bitri 252 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. z  e.  { ( X F ( W `  X ) ) }  -.  z ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  <->  ( -.  ( X F ( W `
 X ) ) ( W `  X
) y  /\  -.  ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) y ) )
114104, 107, 113sylanbrc 668 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  A. z  e.  { ( X F ( W `  X
) ) }  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y )
11596, 114jctird 546 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( A. z  e.  ( x  \  { ( X F ( W `  X
) ) } )  -.  z ( W `
 X ) y  ->  ( A. z  e.  ( x  \  {
( X F ( W `  X ) ) } )  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  /\  A. z  e.  { ( X F ( W `  X
) ) }  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) ) )
116 ssun1 3629 . . . . . . . . . . . . . . . . . . . . 21  |-  x  C_  ( x  u.  { ( X F ( W `
 X ) ) } )
117 undif1 3870 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  \  { ( X F ( W `
 X ) ) } )  u.  {
( X F ( W `  X ) ) } )  =  ( x  u.  {
( X F ( W `  X ) ) } )
118116, 117sseqtr4i 3497 . . . . . . . . . . . . . . . . . . . 20  |-  x  C_  ( ( x  \  { ( X F ( W `  X
) ) } )  u.  { ( X F ( W `  X ) ) } )
119 ralun 3648 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. z  e.  ( x  \  { ( X F ( W `
 X ) ) } )  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  /\  A. z  e.  { ( X F ( W `
 X ) ) }  -.  z ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )  ->  A. z  e.  ( ( x  \  {
( X F ( W `  X ) ) } )  u. 
{ ( X F ( W `  X
) ) } )  -.  z ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y )
120 ssralv 3525 . . . . . . . . . . . . . . . . . . . 20  |-  ( x 
C_  ( ( x 
\  { ( X F ( W `  X ) ) } )  u.  { ( X F ( W `
 X ) ) } )  ->  ( A. z  e.  (
( x  \  {
( X F ( W `  X ) ) } )  u. 
{ ( X F ( W `  X
) ) } )  -.  z ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  ->  A. z  e.  x  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
121118, 119, 120mpsyl 65 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A. z  e.  ( x  \  { ( X F ( W `
 X ) ) } )  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  /\  A. z  e.  { ( X F ( W `
 X ) ) }  -.  z ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )  ->  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y )
122115, 121syl6 34 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( A. z  e.  ( x  \  { ( X F ( W `  X
) ) } )  -.  z ( W `
 X ) y  ->  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) )
123 eldifi 3587 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  y  e.  x
)
124123adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  y  e.  x )
125122, 124jctild 545 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( A. z  e.  ( x  \  { ( X F ( W `  X
) ) } )  -.  z ( W `
 X ) y  ->  ( y  e.  x  /\  A. z  e.  x  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) ) )
126125expimpd 606 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  -> 
( ( y  e.  ( x  \  {
( X F ( W `  X ) ) } )  /\  A. z  e.  ( x 
\  { ( X F ( W `  X ) ) } )  -.  z ( W `  X ) y )  ->  (
y  e.  x  /\  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) ) )
127126reximdv2 2896 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  -> 
( E. y  e.  ( x  \  {
( X F ( W `  X ) ) } ) A. z  e.  ( x  \  { ( X F ( W `  X
) ) } )  -.  z ( W `
 X ) y  ->  E. y  e.  x  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) )
12884, 127mpd 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y )
129128ex 435 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  ->  (
( x  \  {
( X F ( W `  X ) ) } )  =/=  (/)  ->  E. y  e.  x  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) )
13070, 129pm2.61dne 2741 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  ->  E. y  e.  x  A. z  e.  x  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )
131130ex 435 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( x  C_  ( X  u.  { ( X F ( W `  X ) ) } )  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
132131alrimiv 1763 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  A. x
( ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
133 df-fr 4809 . . . . . . . . . 10  |-  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  Fr  ( X  u.  { ( X F ( W `  X ) ) } )  <->  A. x ( ( x  C_  ( X  u.  { ( X F ( W `  X
) ) } )  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) )
134132, 133sylibr 215 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  Fr  ( X  u.  { ( X F ( W `  X ) ) } ) )
135 elun 3606 . . . . . . . . . . . 12  |-  ( x  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( x  e.  X  \/  x  e.  { ( X F ( W `  X
) ) } ) )
136 elun 3606 . . . . . . . . . . . 12  |-  ( y  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( y  e.  X  \/  y  e.  { ( X F ( W `  X
) ) } ) )
137135, 136anbi12i 701 . . . . . . . . . . 11  |-  ( ( x  e.  ( X  u.  { ( X F ( W `  X ) ) } )  /\  y  e.  ( X  u.  {
( X F ( W `  X ) ) } ) )  <-> 
( ( x  e.  X  \/  x  e. 
{ ( X F ( W `  X
) ) } )  /\  ( y  e.  X  \/  y  e. 
{ ( X F ( W `  X
) ) } ) ) )
138 weso 4841 . . . . . . . . . . . . . . . 16  |-  ( ( W `  X )  We  X  ->  ( W `  X )  Or  X )
13920, 138syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  Or  X )
140 solin 4794 . . . . . . . . . . . . . . 15  |-  ( ( ( W `  X
)  Or  X  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x ( W `  X ) y  \/  x  =  y  \/  y ( W `  X ) x ) )
141139, 140sylan 473 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x ( W `  X ) y  \/  x  =  y  \/  y ( W `  X ) x ) )
142 ssun1 3629 . . . . . . . . . . . . . . . . 17  |-  ( W `
 X )  C_  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )
143142a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  X
) )  ->  ( W `  X )  C_  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) )
144143ssbrd 4462 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x ( W `  X ) y  ->  x ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y ) )
145 idd 25 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x  =  y  ->  x  =  y )
)
146143ssbrd 4462 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
y ( W `  X ) x  -> 
y ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) x ) )
147144, 145, 1463orim123d 1343 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
( x ( W `
 X ) y  \/  x  =  y  \/  y ( W `
 X ) x )  ->  ( x
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) x ) ) )
148141, 147mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
149148ex 435 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( x  e.  X  /\  y  e.  X
)  ->  ( x
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) x ) ) )
150 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e.  X ) )  -> 
( x  e.  {
( X F ( W `  X ) ) }  /\  y  e.  X ) )
151150ancomd 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e.  X ) )  -> 
( y  e.  X  /\  x  e.  { ( X F ( W `
 X ) ) } ) )
152 brxp 4881 . . . . . . . . . . . . . . 15  |-  ( y ( X  X.  {
( X F ( W `  X ) ) } ) x  <-> 
( y  e.  X  /\  x  e.  { ( X F ( W `
 X ) ) } ) )
153151, 152sylibr 215 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e.  X ) )  -> 
y ( X  X.  { ( X F ( W `  X
) ) } ) x )
154 ssun2 3630 . . . . . . . . . . . . . . 15  |-  ( X  X.  { ( X F ( W `  X ) ) } )  C_  ( ( W `  X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
155154ssbri 4463 . . . . . . . . . . . . . 14  |-  ( y ( X  X.  {
( X F ( W `  X ) ) } ) x  ->  y ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) x )
156 3mix3 1176 . . . . . . . . . . . . . 14  |-  ( y ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x  -> 
( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
157153, 155, 1563syl 18 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e.  X ) )  -> 
( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
158157ex 435 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( x  e.  {
( X F ( W `  X ) ) }  /\  y  e.  X )  ->  (
x ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) ) )
159 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )  -> 
( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
160 brxp 4881 . . . . . . . . . . . . . . 15  |-  ( x ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
161159, 160sylibr 215 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )  ->  x ( X  X.  { ( X F ( W `  X
) ) } ) y )
162154ssbri 4463 . . . . . . . . . . . . . 14  |-  ( x ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y )
163 3mix1 1174 . . . . . . . . . . . . . 14  |-  ( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  -> 
( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
164161, 162, 1633syl 18 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )  -> 
( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
165164ex 435 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } )  ->  (
x ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) ) )
166 elsni 4021 . . . . . . . . . . . . . . 15  |-  ( x  e.  { ( X F ( W `  X ) ) }  ->  x  =  ( X F ( W `
 X ) ) )
167 elsni 4021 . . . . . . . . . . . . . . 15  |-  ( y  e.  { ( X F ( W `  X ) ) }  ->  y  =  ( X F ( W `
 X ) ) )
168 eqtr3 2450 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( X F ( W `  X ) )  /\  y  =  ( X F ( W `  X ) ) )  ->  x  =  y )
169166, 167, 168syl2an 479 . . . . . . . . . . . . . 14  |-  ( ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e. 
{ ( X F ( W `  X
) ) } )  ->  x  =  y )
1701693mix2d 1181 . . . . . . . . . . . . 13  |-  ( ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e. 
{ ( X F ( W `  X
) ) } )  ->  ( x ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) x ) )
171170a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( x  e.  {
( X F ( W `  X ) ) }  /\  y  e.  { ( X F ( W `  X
) ) } )  ->  ( x ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) x ) ) )
172149, 158, 165, 171ccased 955 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( ( x  e.  X  \/  x  e. 
{ ( X F ( W `  X
) ) } )  /\  ( y  e.  X  \/  y  e. 
{ ( X F ( W `  X
) ) } ) )  ->  ( x
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) x ) ) )
173137, 172syl5bi 220 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( x  e.  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  y  e.  ( X  u.  {
( X F ( W `  X ) ) } ) )  ->  ( x ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) x ) ) )
174173ralrimivv 2845 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  A. x  e.  ( X  u.  {
( X F ( W `  X ) ) } ) A. y  e.  ( X  u.  { ( X F ( W `  X
) ) } ) ( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
175 dfwe2 6619 . . . . . . . . 9  |-  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  We  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) )  Fr  ( X  u.  { ( X F ( W `  X ) ) } )  /\  A. x  e.  ( X  u.  {
( X F ( W `  X ) ) } ) A. y  e.  ( X  u.  { ( X F ( W `  X
) ) } ) ( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) ) )
176134, 174, 175sylanbrc 668 . . . . . . . 8  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  We  ( X  u.  { ( X F ( W `  X ) ) } ) )
1772fpwwe2cbv 9056 . . . . . . . . . . . . 13  |-  W  =  { <. a ,  s
>.  |  ( (
a  C_  A  /\  s  C_  ( a  X.  a ) )  /\  ( s  We  a  /\  A. z  e.  a 
[. ( `' s
" { z } )  /  b ]. ( b F ( s  i^i  ( b  X.  b ) ) )  =  z ) ) }
178177, 4, 13fpwwe2lem3 9059 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( `' ( W `  X )
" { y } ) F ( ( W `  X )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) ) )  =  y )
179 cnvimass 5204 . . . . . . . . . . . . . . 15  |-  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  C_  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )
180 fvex 5888 . . . . . . . . . . . . . . . . 17  |-  ( W `
 X )  e. 
_V
181 snex 4659 . . . . . . . . . . . . . . . . . 18  |-  { ( X F ( W `
 X ) ) }  e.  _V
182 xpexg 6604 . . . . . . . . . . . . . . . . . 18  |-  ( ( X  e.  dom  W  /\  { ( X F ( W `  X
) ) }  e.  _V )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
1838, 181, 182sylancl 666 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
184 unexg 6603 . . . . . . . . . . . . . . . . 17  |-  ( ( ( W `  X
)  e.  _V  /\  ( X  X.  { ( X F ( W `
 X ) ) } )  e.  _V )  ->  ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  e.  _V )
185180, 183, 184sylancr 667 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )
186 dmexg 6735 . . . . . . . . . . . . . . . 16  |-  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V  ->  dom  ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  e.  _V )
187185, 186syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )
188 ssexg 4567 . . . . . . . . . . . . . . 15  |-  ( ( ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) " { y } )  C_  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  /\  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )  ->  ( `' ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  e. 
_V )
189179, 187, 188sylancr 667 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } )  e.  _V )
190189adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) " { y } )  e.  _V )
191 id 23 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( `' ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  ->  u  =  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } ) )
192 simpr 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  y  e.  X )
193 simplr 760 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  X
)
194 nelne2 2754 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  X  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  y  =/=  ( X F ( W `  X ) ) )
195192, 193, 194syl2anc 665 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  y  =/=  ( X F ( W `  X ) ) )
19688, 167syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  =  ( X F ( W `
 X ) ) )
197196necon3ai 2652 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =/=  ( X F ( W `  X
) )  ->  -.  z ( X  X.  { ( X F ( W `  X
) ) } ) y )
198 biorf 406 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  z ( X  X.  { ( X F ( W `  X
) ) } ) y  ->  ( z
( W `  X
) y  <->  ( z
( X  X.  {
( X F ( W `  X ) ) } ) y  \/  z ( W `
 X ) y ) ) )
199195, 197, 1983syl 18 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( z ( W `
 X ) y  <-> 
( z ( X  X.  { ( X F ( W `  X ) ) } ) y  \/  z
( W `  X
) y ) ) )
200 orcom 388 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z ( X  X.  { ( X F ( W `  X
) ) } ) y  \/  z ( W `  X ) y )  <->  ( z
( W `  X
) y  \/  z
( X  X.  {
( X F ( W `  X ) ) } ) y ) )
201200, 85bitr4i 255 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z ( X  X.  { ( X F ( W `  X
) ) } ) y  \/  z ( W `  X ) y )  <->  z (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )
202199, 201syl6rbb 265 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( z ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  <->  z ( W `  X )
y ) )
203 vex 3084 . . . . . . . . . . . . . . . . . . 19  |-  y  e. 
_V
204 vex 3084 . . . . . . . . . . . . . . . . . . . 20  |-  z  e. 
_V
205204eliniseg 5213 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  _V  ->  (
z  e.  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  <->  z (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
206203, 205ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( `' ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  <->  z (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )
207204eliniseg 5213 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  _V  ->  (
z  e.  ( `' ( W `  X
) " { y } )  <->  z ( W `  X )
y ) )
208203, 207ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( `' ( W `  X )
" { y } )  <->  z ( W `
 X ) y )
209202, 206, 2083bitr4g 291 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( z  e.  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } )  <->  z  e.  ( `' ( W `  X ) " {
y } ) ) )
210209eqrdv 2419 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) " { y } )  =  ( `' ( W `  X ) " {
y } ) )
211191, 210sylan9eqr 2485 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  u  =  ( `' ( W `  X )
" { y } ) )
212211sqxpeqd 4876 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  (
u  X.  u )  =  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) )
213212ineq2d 3664 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  (
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
u  X.  u ) )  =  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) ) )
214 indir 3721 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) )  =  ( ( ( W `
 X )  i^i  ( ( `' ( W `  X )
" { y } )  X.  ( `' ( W `  X
) " { y } ) ) )  u.  ( ( X  X.  { ( X F ( W `  X ) ) } )  i^i  ( ( `' ( W `  X ) " {
y } )  X.  ( `' ( W `
 X ) " { y } ) ) ) )
215 inxp 4983 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( X  X.  { ( X F ( W `
 X ) ) } )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) )  =  ( ( X  i^i  ( `' ( W `  X ) " {
y } ) )  X.  ( { ( X F ( W `
 X ) ) }  i^i  ( `' ( W `  X
) " { y } ) ) )
216 incom 3655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X ) " {
y } ) )  =  ( ( `' ( W `  X
) " { y } )  i^i  {
( X F ( W `  X ) ) } )
217 cnvimass 5204 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( `' ( W `  X
) " { y } )  C_  dom  ( W `  X )
21818adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( W `  X
)  C_  ( X  X.  X ) )
219 dmss 5050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( W `  X ) 
C_  ( X  X.  X )  ->  dom  ( W `  X ) 
C_  dom  ( X  X.  X ) )
220218, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  dom  ( W `  X )  C_  dom  ( X  X.  X
) )
221 dmxpid 5070 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  dom  ( X  X.  X )  =  X
222220, 221syl6sseq 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  dom  ( W `  X )  C_  X
)
223217, 222syl5ss 3475 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( W `
 X ) " { y } ) 
C_  X )
224223, 193ssneldd 3467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  ( `' ( W `  X ) " {
y } ) )
225 disjsn 4057 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( `' ( W `
 X ) " { y } )  i^i  { ( X F ( W `  X ) ) } )  =  (/)  <->  -.  ( X F ( W `  X ) )  e.  ( `' ( W `
 X ) " { y } ) )
226224, 225sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( `' ( W `  X )
" { y } )  i^i  { ( X F ( W `
 X ) ) } )  =  (/) )
227216, 226syl5eq 2475 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X )
" { y } ) )  =  (/) )
228227xpeq2d 4874 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( X  i^i  ( `' ( W `  X ) " {
y } ) )  X.  ( { ( X F ( W `
 X ) ) }  i^i  ( `' ( W `  X
) " { y } ) ) )  =  ( ( X  i^i  ( `' ( W `  X )
" { y } ) )  X.  (/) ) )
229 xp0 5271 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  i^i  ( `' ( W `  X
) " { y } ) )  X.  (/) )  =  (/)
230228, 229syl6eq 2479 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( X  i^i  ( `' ( W `  X ) " {
y } ) )  X.  ( { ( X F ( W `
 X ) ) }  i^i  ( `' ( W `  X
) " { y } ) ) )  =  (/) )
231215, 230syl5eq 2475 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( X  X.  { ( X F ( W `  X
) ) } )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) )  =  (/) )
232231uneq2d 3620 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( ( W `
 X )  i^i  ( ( `' ( W `  X )
" { y } )  X.  ( `' ( W `  X
) " { y } ) ) )  u.  ( ( X  X.  { ( X F ( W `  X ) ) } )  i^i  ( ( `' ( W `  X ) " {
y } )  X.  ( `' ( W `
 X ) " { y } ) ) ) )  =  ( ( ( W `
 X )  i^i  ( ( `' ( W `  X )
" { y } )  X.  ( `' ( W `  X
) " { y } ) ) )  u.  (/) ) )
233214, 232syl5eq 2475 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) )  =  ( ( ( W `  X
)  i^i  ( ( `' ( W `  X ) " {
y } )  X.  ( `' ( W `
 X ) " { y } ) ) )  u.  (/) ) )
234 un0 3787 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( W `  X
)  i^i  ( ( `' ( W `  X ) " {
y } )  X.  ( `' ( W `
 X ) " { y } ) ) )  u.  (/) )  =  ( ( W `  X )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) )
235233, 234syl6eq 2479 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) )  =  ( ( W `  X )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) ) )
236235adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  (
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) )  =  ( ( W `  X )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) ) )
237213, 236eqtrd 2463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  (
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
u  X.  u ) )  =  ( ( W `  X )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) ) )
238211, 237oveq12d 6320 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  -.  (