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

Theorem fpwwe2lem13 8519
Description: Lemma for fpwwe2 8520. (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 3513 . . . 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 453 . . . . . . . . . . . . . 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 697 . . . . . . . . . . . . . 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 8518 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  e.  dom  W )
92, 4, 6, 7fpwwe2lem11 8517 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  W : dom  W --> ~P ( X  X.  X ) )
10 ffun 5595 . . . . . . . . . . . . . 14  |-  ( W : dom  W --> ~P ( X  X.  X )  ->  Fun  W )
11 funfvbrb 5845 . . . . . . . . . . . . . 14  |-  ( Fun 
W  ->  ( X  e.  dom  W  <->  X W
( W `  X
) ) )
129, 10, 113syl 19 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  e.  dom  W  <->  X W
( W `  X
) ) )
138, 12mpbid 203 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X W ( W `  X ) )
142, 4fpwwe2lem2 8509 . . . . . . . . . . . 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 203 . . . . . . . . . . 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 447 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
) ) )
1716simpld 447 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  C_  A )
1816simprd 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  C_  ( X  X.  X
) )
1915simprd 451 . . . . . . . . . . . . 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 447 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  We  X )
2117, 18, 203jca 1135 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )
222, 3, 5fpwwe2lem5 8511 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  C_  A  /\  ( W `
 X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )  ->  ( X F ( W `  X ) )  e.  A )
2321, 22syldan 458 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X F ( W `  X ) )  e.  A )
2423snssd 3945 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  { ( X F ( W `
 X ) ) }  C_  A )
2517, 24unssd 3525 . . . . . . . 8  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  u.  { ( X F ( W `  X ) ) } )  C_  A )
26 ssun1 3512 . . . . . . . . . . 11  |-  X  C_  ( X  u.  { ( X F ( W `
 X ) ) } )
27 xpss12 4983 . . . . . . . . . . 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 655 . . . . . . . . . 10  |-  ( X  X.  X )  C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  {
( X F ( W `  X ) ) } ) )
2918, 28syl6ss 3362 . . . . . . . . 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 4983 . . . . . . . . . . 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 655 . . . . . . . . . 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 3525 . . . . . . . 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 520 . . . . . . 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 3688 . . . . . . . . . . . . . 14  |-  ( x 
C_  { ( X F ( W `  X ) ) }  <-> 
( x  \  {
( X F ( W `  X ) ) } )  =  (/) )
36 simpllr 737 . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . 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 4255 . . . . . . . . . . . . . . . . . . 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 4911 . . . . . . . . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) ( X F ( W `  X
) )  ->  ( X F ( W `  X ) )  e.  X )
4138, 40syl6 32 . . . . . . . . . . . . . . . . . 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 171 . . . . . . . . . . . . . . . . 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 4911 . . . . . . . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) ( X F ( W `
 X ) )  ->  ( X F ( W `  X
) )  e.  X
)
4536, 44nsyl 116 . . . . . . . . . . . . . . . . 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 6108 . . . . . . . . . . . . . . . . . . 19  |-  ( X F ( W `  X ) )  e. 
_V
47 breq2 4218 . . . . . . . . . . . . . . . . . . . . 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 4260 . . . . . . . . . . . . . . . . . . . . 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 254 . . . . . . . . . . . . . . . . . . . 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 287 . . . . . . . . . . . . . . . . . . 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 3852 . . . . . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . . . . . 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 647 . . . . . . . . . . . . . . . 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 739 . . . . . . . . . . . . . . . . . . 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 2619 . . . . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . . . . . . 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 3959 . . . . . . . . . . . . . . . . . . . 20  |-  ( x 
C_  { ( X F ( W `  X ) ) }  <-> 
( x  =  (/)  \/  x  =  { ( X F ( W `
 X ) ) } ) )
5957, 58sylib 190 . . . . . . . . . . . . . . . . . . 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 368 . . . . . . . . . . . . . . . . . 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 2912 . . . . . . . . . . . . . . . . . 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 4217 . . . . . . . . . . . . . . . . . . . 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 287 . . . . . . . . . . . . . . . . . . 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 3851 . . . . . . . . . . . . . . . . . 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 254 . . . . . . . . . . . . . . . . 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 2919 . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . 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 425 . . . . . . . . . . . . . 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 211 . . . . . . . . . . . . 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 2961 . . . . . . . . . . . . . . . . 17  |-  x  e. 
_V
72 difexg 4353 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  _V  ->  (
x  \  { ( X F ( W `  X ) ) } )  e.  _V )
7371, 72mp1i 12 . . . . . . . . . . . . . . . 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 4574 . . . . . . . . . . . . . . . . . 18  |-  ( ( W `  X )  We  X  ->  ( W `  X )  Fr  X )
7520, 74syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  Fr  X )
7675ad2antrr 708 . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . . 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 3493 . . . . . . . . . . . . . . . . . 18  |-  ( X  u.  { ( X F ( W `  X ) ) } )  =  ( { ( X F ( W `  X ) ) }  u.  X
)
7977, 78syl6sseq 3396 . . . . . . . . . . . . . . . . 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 3713 . . . . . . . . . . . . . . . . 17  |-  ( x 
C_  ( { ( X F ( W `
 X ) ) }  u.  X )  <-> 
( x  \  {
( X F ( W `  X ) ) } )  C_  X )
8179, 80sylib 190 . . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . . 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 4546 . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . 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 4260 . . . . . . . . . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . . . . . . . . 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 4911 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( z  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
8887simprbi 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  e.  {
( X F ( W `  X ) ) } )
89 eldifn 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  -.  y  e.  { ( X F ( W `  X ) ) } )
9089adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . 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 101 . . . . . . . . . . . . . . . . . . . . . . . . 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 31 . . . . . . . . . . . . . . . . . . . . . . . 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 371 . . . . . . . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . . . . . . . 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 128 . . . . . . . . . . . . . . . . . . . . 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 2787 . . . . . . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  -.  ( X F ( W `
 X ) )  e.  X )
9897ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . . . . . . . . . . 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 4255 . . . . . . . . . . . . . . . . . . . . . . 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 4911 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) y  <->  ( ( X F ( W `  X ) )  e.  X  /\  y  e.  X ) )
102101simplbi 448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) y  ->  ( X F ( W `  X ) )  e.  X )
103100, 102syl6 32 . . . . . . . . . . . . . . . . . . . . . 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 171 . . . . . . . . . . . . . . . . . . . . 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 4911 . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  e.  {
( X F ( W `  X ) ) } )
10790, 106nsyl 116 . . . . . . . . . . . . . . . . . . . . 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 4260 . . . . . . . . . . . . . . . . . . . . . . . . 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 254 . . . . . . . . . . . . . . . . . . . . . . . 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 287 . . . . . . . . . . . . . . . . . . . . . . 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 3851 . . . . . . . . . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . . . . . . . . . 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 647 . . . . . . . . . . . . . . . . . . . 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 530 . . . . . . . . . . . . . . . . . . 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 3512 . . . . . . . . . . . . . . . . . . . . 21  |-  x  C_  ( x  u.  { ( X F ( W `
 X ) ) } )
117 undif1 3705 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  \  { ( X F ( W `
 X ) ) } )  u.  {
( X F ( W `  X ) ) } )  =  ( x  u.  {
( X F ( W `  X ) ) } )
118116, 117sseqtr4i 3383 . . . . . . . . . . . . . . . . . . . 20  |-  x  C_  ( ( x  \  { ( X F ( W `  X
) ) } )  u.  { ( X F ( W `  X ) ) } )
119 ralun 3531 . . . . . . . . . . . . . . . . . . . 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 3409 . . . . . . . . . . . . . . . . . . . 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 62 . . . . . . . . . . . . . . . . . . 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 32 . . . . . . . . . . . . . . . . . 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 3471 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  y  e.  x
)
124123adantl 454 . . . . . . . . . . . . . . . . . 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 529 . . . . . . . . . . . . . . . . 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 588 . . . . . . . . . . . . . . . 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 2817 . . . . . . . . . . . . . . 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 425 . . . . . . . . . . . . 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 2683 . . . . . . . . . . . 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 425 . . . . . . . . . . 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 1642 . . . . . . . . . 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 4543 . . . . . . . . . 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 205 . . . . . . . . 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 3490 . . . . . . . . . . . 12  |-  ( x  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( x  e.  X  \/  x  e.  { ( X F ( W `  X
) ) } ) )
136 elun 3490 . . . . . . . . . . . 12  |-  ( y  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( y  e.  X  \/  y  e.  { ( X F ( W `  X
) ) } ) )
137135, 136anbi12i 680 . . . . . . . . . . 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 4575 . . . . . . . . . . . . . . . 16  |-  ( ( W `  X )  We  X  ->  ( W `  X )  Or  X )
13920, 138syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  Or  X )
140 solin 4528 . . . . . . . . . . . . . . 15  |-  ( ( ( W `  X
)  Or  X  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x ( W `  X ) y  \/  x  =  y  \/  y ( W `  X ) x ) )
141139, 140sylan 459 . . . . . . . . . . . . . 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 3512 . . . . . . . . . . . . . . . . 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 4255 . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x  =  y  ->  x  =  y )
)
146143ssbrd 4255 . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . 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 425 . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . . 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 440 . . . . . . . . . . . . . . 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 4911 . . . . . . . . . . . . . . 15  |-  ( y ( X  X.  {
( X F ( W `  X ) ) } ) x  <-> 
( y  e.  X  /\  x  e.  { ( X F ( W `
 X ) ) } ) )
153151, 152sylibr 205 . . . . . . . . . . . . . 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 3513 . . . . . . . . . . . . . . 15  |-  ( X  X.  { ( X F ( W `  X ) ) } )  C_  ( ( W `  X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
155154ssbri 4256 . . . . . . . . . . . . . 14  |-  ( y ( X  X.  {
( X F ( W `  X ) ) } ) x  ->  y ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) x )
156 3mix3 1129 . . . . . . . . . . . . . 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 19 . . . . . . . . . . . . 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 425 . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . 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 4911 . . . . . . . . . . . . . . 15  |-  ( x ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
161159, 160sylibr 205 . . . . . . . . . . . . . 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 4256 . . . . . . . . . . . . . 14  |-  ( x ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y )
163 3mix1 1127 . . . . . . . . . . . . . 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 19 . . . . . . . . . . . . 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 425 . . . . . . . . . . . 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 3840 . . . . . . . . . . . . . . 15  |-  ( x  e.  { ( X F ( W `  X ) ) }  ->  x  =  ( X F ( W `
 X ) ) )
167 elsni 3840 . . . . . . . . . . . . . . 15  |-  ( y  e.  { ( X F ( W `  X ) ) }  ->  y  =  ( X F ( W `
 X ) ) )
168 eqtr3 2457 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( X F ( W `  X ) )  /\  y  =  ( X F ( W `  X ) ) )  ->  x  =  y )
169166, 167, 168syl2an 465 . . . . . . . . . . . . . 14  |-  ( ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e. 
{ ( X F ( W `  X
) ) } )  ->  x  =  y )
170 3mix2 1128 . . . . . . . . . . . . . 14  |-  ( 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 ) )
171169, 170syl 16 . . . . . . . . . . . . 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 ) )
172171a1i 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 ) ) )
173149, 158, 165, 172ccased 915 . . . . . . . . . . 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 ) ) )
174137, 173syl5bi 210 . . . . . . . . . 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 ) ) )
175174ralrimivv 2799 . . . . . . . . 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 ) )
176 dfwe2 4764 . . . . . . . . 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 ) ) )
177134, 175, 176sylanbrc 647 . . . . . . . 8  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  We  ( X  u.  { ( X F ( W `  X ) ) } ) )
1782fpwwe2cbv 8507 . . . . . . . . . . . . 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 ) ) }
179178, 4, 13fpwwe2lem3 8510 . . . . . . . . . . . 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 )
180 cnvimass 5226 . . . . . . . . . . . . . . 15  |-  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  C_  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )
181 fvex 5744 . . . . . . . . . . . . . . . . 17  |-  ( W `
 X )  e. 
_V
182 snex 4407 . . . . . . . . . . . . . . . . . 18  |-  { ( X F ( W `
 X ) ) }  e.  _V
183 xpexg 4991 . . . . . . . . . . . . . . . . . 18  |-  ( ( X  e.  dom  W  /\  { ( X F ( W `  X
) ) }  e.  _V )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
1848, 182, 183sylancl 645 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
185 unexg 4712 . . . . . . . . . . . . . . . . 17  |-  ( ( ( W `  X
)  e.  _V  /\  ( X  X.  { ( X F ( W `
 X ) ) } )  e.  _V )  ->  ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  e.  _V )
186181, 184, 185sylancr 646 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )
187 dmexg 5132 . . . . . . . . . . . . . . . 16  |-  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V  ->  dom  ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  e.  _V )
188186, 187syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )
189 ssexg 4351 . . . . . . . . . . . . . . 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 )
190180, 188, 189sylancr 646 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } )  e.  _V )
191190adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) " { y } )  e.  _V )
192 id 21 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( `' ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  ->  u  =  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } ) )
193 simpr 449 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  y  e.  X )
194 simplr 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  X
)
195 nelne2 2696 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  X  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  y  =/=  ( X F ( W `  X ) ) )
196193, 194, 195syl2anc 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  y  =/=  ( X F ( W `  X ) ) )
19788, 167syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  =  ( X F ( W `
 X ) ) )
198197necon3ai 2646 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =/=  ( X F ( W `  X
) )  ->  -.  z ( X  X.  { ( X F ( W `  X
) ) } ) y )
199 biorf 396 . . . . . . . . . . . . . . . . . . . 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 ) ) )
200196, 198, 1993syl 19 . . . . . . . . . . . . . . . . . . 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 ) ) )
201 orcom 378 . . . . . . . . . . . . . . . . . . . 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 ) )
202201, 85bitr4i 245 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z ( X  X.  { ( X F ( W `  X
) ) } ) y  \/  z ( W `  X ) y )  <->  z (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )
203200, 202syl6rbb 255 . . . . . . . . . . . . . . . . . 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 ) )
204 vex 2961 . . . . . . . . . . . . . . . . . . 19  |-  y  e. 
_V
205 vex 2961 . . . . . . . . . . . . . . . . . . . 20  |-  z  e. 
_V
206205eliniseg 5235 . . . . . . . . . . . . . . . . . . 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 ) )
207204, 206ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( `' ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  <->  z (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )
208205eliniseg 5235 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  _V  ->  (
z  e.  ( `' ( W `  X
) " { y } )  <->  z ( W `  X )
y ) )
209204, 208ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( `' ( W `  X )
" { y } )  <->  z ( W `
 X ) y )
210203, 207, 2093bitr4g 281 . . . . . . . . . . . . . . . . 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 } ) ) )
211210eqrdv 2436 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) " { y } )  =  ( `' ( W `  X ) " {
y } ) )
212192, 211sylan9eqr 2492 . . . . . . . . . . . . . . 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 } ) )
213212, 212xpeq12d 4905 . . . . . . . . . . . . . . . . 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 } ) ) )
214213ineq2d 3544 . . . . . . . . . . . . . . . 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 } ) ) ) )
215 indir 3591 . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
216 inxp 5009 . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
217 incom 3535 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X ) " {
y } ) )  =  ( ( `' ( W `  X
) " { y } )  i^i  {
( X F ( W `  X ) ) } )
218 cnvimass 5226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( `' ( W `  X
) " { y } )  C_  dom  ( W `  X )
21918adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( W `  X
)  C_  ( X  X.  X ) )
220 dmss 5071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( W `  X ) 
C_  ( X  X.  X )  ->  dom  ( W `  X ) 
C_  dom  ( X  X.  X ) )
221219, 220syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  dom  ( W `  X )  C_  dom  ( X  X.  X
) )
222 dmxpid 5091 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  dom  ( X  X.  X )  =  X
223221, 222syl6sseq 3396 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  dom  ( W `  X )  C_  X
)
224218, 223syl5ss 3361 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( W `
 X ) " { y } ) 
C_  X )
225224, 194ssneldd 3353 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  ( `' ( W `  X ) " {
y } ) )
226 disjsn 3870 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( `' ( W `
 X ) " { y } )  i^i  { ( X F ( W `  X ) ) } )  =  (/)  <->  -.  ( X F ( W `  X ) )  e.  ( `' ( W `
 X ) " { y } ) )
227225, 226sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( `' ( W `  X )
" { y } )  i^i  { ( X F ( W `
 X ) ) } )  =  (/) )
228217, 227syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X )
" { y } ) )  =  (/) )
229228xpeq2d 4904 . . . . . . . . . . . . . . . . . . . . . 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.  (/) ) )
230 xp0 5293 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  i^i  ( `' ( W `  X
) " { y } ) )  X.  (/) )  =  (/)
231229, 230syl6eq 2486 . . . . . . . . . . . . . . . . . . . . 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 } ) ) )  =  (/) )
232216, 231syl5eq 2482 . . . . . . . . . . . . . . . . . . . 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 } ) ) )  =  (/) )
233232uneq2d 3503 . . . . . . . . . . . . . . . . . . 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.  (/) ) )
234215, 233syl5eq 2482 . . . . . . . . . . . . . . . . . 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.  (/) ) )
235 un0 3654 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( W `  X
)  i^i  ( ( `' ( W `  X ) " {
y } )  X.  ( `' ( W `
 X ) " { y } ) ) )  u.  (/) )  =  ( ( W `  X )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) )
236234, 235syl6eq 2486 . . . . . . . . . . . . . . . . 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 } ) ) ) )
237236adantr 453 . . . . . . . . . . . . . . . 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 } ) ) ) )
238214, 237eqtrd 2470 . . . . . . . . . . . . . . 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 (