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

Theorem fpwwe2lem13 9016
Description: Lemma for fpwwe2 9017. (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 3668 . . . 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 465 . . . . . . . . . . . . . 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 714 . . . . . . . . . . . . . 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 9015 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  e.  dom  W )
92, 4, 6, 7fpwwe2lem11 9014 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  W : dom  W --> ~P ( X  X.  X ) )
10 ffun 5731 . . . . . . . . . . . . . 14  |-  ( W : dom  W --> ~P ( X  X.  X )  ->  Fun  W )
11 funfvbrb 5992 . . . . . . . . . . . . . 14  |-  ( Fun 
W  ->  ( X  e.  dom  W  <->  X W
( W `  X
) ) )
129, 10, 113syl 20 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  e.  dom  W  <->  X W
( W `  X
) ) )
138, 12mpbid 210 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X W ( W `  X ) )
142, 4fpwwe2lem2 9006 . . . . . . . . . . . 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 210 . . . . . . . . . . 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 459 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
) ) )
1716simpld 459 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  C_  A )
1816simprd 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  C_  ( X  X.  X
) )
1915simprd 463 . . . . . . . . . . . . 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 459 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  We  X )
2117, 18, 203jca 1176 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )
222, 3, 5fpwwe2lem5 9008 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  C_  A  /\  ( W `
 X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )  ->  ( X F ( W `  X ) )  e.  A )
2321, 22syldan 470 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X F ( W `  X ) )  e.  A )
2423snssd 4172 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  { ( X F ( W `
 X ) ) }  C_  A )
2517, 24unssd 3680 . . . . . . . 8  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  u.  { ( X F ( W `  X ) ) } )  C_  A )
26 ssun1 3667 . . . . . . . . . . 11  |-  X  C_  ( X  u.  { ( X F ( W `
 X ) ) } )
27 xpss12 5106 . . . . . . . . . . 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 672 . . . . . . . . . 10  |-  ( X  X.  X )  C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  {
( X F ( W `  X ) ) } ) )
2918, 28syl6ss 3516 . . . . . . . . 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 5106 . . . . . . . . . . 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 672 . . . . . . . . . 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 3680 . . . . . . . 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 532 . . . . . . 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 3885 . . . . . . . . . . . . . 14  |-  ( x 
C_  { ( X F ( W `  X ) ) }  <-> 
( x  \  {
( X F ( W `  X ) ) } )  =  (/) )
36 simpllr 758 . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . 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 4488 . . . . . . . . . . . . . . . . . . 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 5029 . . . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) ( X F ( W `  X
) )  ->  ( X F ( W `  X ) )  e.  X )
4138, 40syl6 33 . . . . . . . . . . . . . . . . . 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 177 . . . . . . . . . . . . . . . . 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 5029 . . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . . 18  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) ( X F ( W `
 X ) )  ->  ( X F ( W `  X
) )  e.  X
)
4536, 44nsyl 121 . . . . . . . . . . . . . . . . 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 6307 . . . . . . . . . . . . . . . . . . 19  |-  ( X F ( W `  X ) )  e. 
_V
47 breq2 4451 . . . . . . . . . . . . . . . . . . . . 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 4495 . . . . . . . . . . . . . . . . . . . . 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 261 . . . . . . . . . . . . . . . . . . . 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 294 . . . . . . . . . . . . . . . . . . 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 4067 . . . . . . . . . . . . . . . . . 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 490 . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . 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 664 . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . 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 2669 . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . 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 4185 . . . . . . . . . . . . . . . . . . . 20  |-  ( x 
C_  { ( X F ( W `  X ) ) }  <-> 
( x  =  (/)  \/  x  =  { ( X F ( W `
 X ) ) } ) )
5957, 58sylib 196 . . . . . . . . . . . . . . . . . . 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 377 . . . . . . . . . . . . . . . . . 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 3064 . . . . . . . . . . . . . . . . . 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 4450 . . . . . . . . . . . . . . . . . . . 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 294 . . . . . . . . . . . . . . . . . . 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 4066 . . . . . . . . . . . . . . . . . 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 261 . . . . . . . . . . . . . . . . 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 3073 . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . 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 218 . . . . . . . . . . . . 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 3116 . . . . . . . . . . . . . . . . 17  |-  x  e. 
_V
72 difexg 4595 . . . . . . . . . . . . . . . . 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 4869 . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . 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 759 . . . . . . . . . . . . . . . . . 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 3648 . . . . . . . . . . . . . . . . . 18  |-  ( X  u.  { ( X F ( W `  X ) ) } )  =  ( { ( X F ( W `  X ) ) }  u.  X
)
7977, 78syl6sseq 3550 . . . . . . . . . . . . . . . . 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 3910 . . . . . . . . . . . . . . . . 17  |-  ( x 
C_  ( { ( X F ( W `
 X ) ) }  u.  X )  <-> 
( x  \  {
( X F ( W `  X ) ) } )  C_  X )
8179, 80sylib 196 . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . 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 4841 . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . 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 4495 . . . . . . . . . . . . . . . . . . . . . . 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 24 . . . . . . . . . . . . . . . . . . . . . . . 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 5029 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( z  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
8887simprbi 464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  e.  {
( X F ( W `  X ) ) } )
89 eldifn 3627 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  -.  y  e.  { ( X F ( W `  X ) ) } )
9089adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 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 106 . . . . . . . . . . . . . . . . . . . . . . . . 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 32 . . . . . . . . . . . . . . . . . . . . . . . 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 380 . . . . . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . . . . . 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 133 . . . . . . . . . . . . . . . . . . . . 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 2874 . . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  -.  ( X F ( W `
 X ) )  e.  X )
9897ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . . . . . . . . . . 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 4488 . . . . . . . . . . . . . . . . . . . . . . 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 5029 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) y  <->  ( ( X F ( W `  X ) )  e.  X  /\  y  e.  X ) )
102101simplbi 460 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) y  ->  ( X F ( W `  X ) )  e.  X )
103100, 102syl6 33 . . . . . . . . . . . . . . . . . . . . . 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 177 . . . . . . . . . . . . . . . . . . . . 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 5029 . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  e.  {
( X F ( W `  X ) ) } )
10790, 106nsyl 121 . . . . . . . . . . . . . . . . . . . . 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 4495 . . . . . . . . . . . . . . . . . . . . . . . . 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 261 . . . . . . . . . . . . . . . . . . . . . . . 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 294 . . . . . . . . . . . . . . . . . . . . . . 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 4066 . . . . . . . . . . . . . . . . . . . . . 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 490 . . . . . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . . . . . 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 664 . . . . . . . . . . . . . . . . . . . 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 544 . . . . . . . . . . . . . . . . . . 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 3667 . . . . . . . . . . . . . . . . . . . . 21  |-  x  C_  ( x  u.  { ( X F ( W `
 X ) ) } )
117 undif1 3902 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  \  { ( X F ( W `
 X ) ) } )  u.  {
( X F ( W `  X ) ) } )  =  ( x  u.  {
( X F ( W `  X ) ) } )
118116, 117sseqtr4i 3537 . . . . . . . . . . . . . . . . . . . 20  |-  x  C_  ( ( x  \  { ( X F ( W `  X
) ) } )  u.  { ( X F ( W `  X ) ) } )
119 ralun 3686 . . . . . . . . . . . . . . . . . . . 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 3564 . . . . . . . . . . . . . . . . . . . 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 63 . . . . . . . . . . . . . . . . . . 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 33 . . . . . . . . . . . . . . . . . 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 3626 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  y  e.  x
)
124123adantl 466 . . . . . . . . . . . . . . . . . 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 543 . . . . . . . . . . . . . . . . 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 603 . . . . . . . . . . . . . . . 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 2934 . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . 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 2784 . . . . . . . . . . . 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 434 . . . . . . . . . . 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 1695 . . . . . . . . . 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 4838 . . . . . . . . . 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 212 . . . . . . . . 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 3645 . . . . . . . . . . . 12  |-  ( x  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( x  e.  X  \/  x  e.  { ( X F ( W `  X
) ) } ) )
136 elun 3645 . . . . . . . . . . . 12  |-  ( y  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( y  e.  X  \/  y  e.  { ( X F ( W `  X
) ) } ) )
137135, 136anbi12i 697 . . . . . . . . . . 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 4870 . . . . . . . . . . . . . . . 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 4823 . . . . . . . . . . . . . . 15  |-  ( ( ( W `  X
)  Or  X  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x ( W `  X ) y  \/  x  =  y  \/  y ( W `  X ) x ) )
141139, 140sylan 471 . . . . . . . . . . . . . 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 3667 . . . . . . . . . . . . . . . . 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 4488 . . . . . . . . . . . . . . 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 24 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x  =  y  ->  x  =  y )
)
146143ssbrd 4488 . . . . . . . . . . . . . . 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 1307 . . . . . . . . . . . . . 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 434 . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . 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 5029 . . . . . . . . . . . . . . 15  |-  ( y ( X  X.  {
( X F ( W `  X ) ) } ) x  <-> 
( y  e.  X  /\  x  e.  { ( X F ( W `
 X ) ) } ) )
153151, 152sylibr 212 . . . . . . . . . . . . . 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 3668 . . . . . . . . . . . . . . 15  |-  ( X  X.  { ( X F ( W `  X ) ) } )  C_  ( ( W `  X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
155154ssbri 4489 . . . . . . . . . . . . . 14  |-  ( y ( X  X.  {
( X F ( W `  X ) ) } ) x  ->  y ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) x )
156 3mix3 1167 . . . . . . . . . . . . . 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 20 . . . . . . . . . . . . 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 434 . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . 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 5029 . . . . . . . . . . . . . . 15  |-  ( x ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
161159, 160sylibr 212 . . . . . . . . . . . . . 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 4489 . . . . . . . . . . . . . 14  |-  ( x ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y )
163 3mix1 1165 . . . . . . . . . . . . . 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 20 . . . . . . . . . . . . 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 434 . . . . . . . . . . . 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 4052 . . . . . . . . . . . . . . 15  |-  ( x  e.  { ( X F ( W `  X ) ) }  ->  x  =  ( X F ( W `
 X ) ) )
167 elsni 4052 . . . . . . . . . . . . . . 15  |-  ( y  e.  { ( X F ( W `  X ) ) }  ->  y  =  ( X F ( W `
 X ) ) )
168 eqtr3 2495 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( X F ( W `  X ) )  /\  y  =  ( X F ( W `  X ) ) )  ->  x  =  y )
169166, 167, 168syl2an 477 . . . . . . . . . . . . . 14  |-  ( ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e. 
{ ( X F ( W `  X
) ) } )  ->  x  =  y )
170 3mix2 1166 . . . . . . . . . . . . . 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 945 . . . . . . . . . . 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 217 . . . . . . . . . 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 2884 . . . . . . . . 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 6595 . . . . . . . . 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 664 . . . . . . . 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 9004 . . . . . . . . . . . . 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 9007 . . . . . . . . . . . 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 5355 . . . . . . . . . . . . . . 15  |-  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  C_  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )
181 fvex 5874 . . . . . . . . . . . . . . . . 17  |-  ( W `
 X )  e. 
_V
182 snex 4688 . . . . . . . . . . . . . . . . . 18  |-  { ( X F ( W `
 X ) ) }  e.  _V
183 xpexg 6709 . . . . . . . . . . . . . . . . . 18  |-  ( ( X  e.  dom  W  /\  { ( X F ( W `  X
) ) }  e.  _V )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
1848, 182, 183sylancl 662 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
185 unexg 6583 . . . . . . . . . . . . . . . . 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 663 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )
187 dmexg 6712 . . . . . . . . . . . . . . . 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 4593 . . . . . . . . . . . . . . 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 663 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } )  e.  _V )
191190adantr 465 . . . . . . . . . . . . 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 22 . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  y  e.  X )
194 simplr 754 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  X
)
195 nelne2 2797 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  X  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  y  =/=  ( X F ( W `  X ) ) )
196193, 194, 195syl2anc 661 . . . . . . . . . . . . . . . . . . . 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 2695 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =/=  ( X F ( W `  X
) )  ->  -.  z ( X  X.  { ( X F ( W `  X
) ) } ) y )
199 biorf 405 . . . . . . . . . . . . . . . . . . . 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 20 . . . . . . . . . . . . . . . . . . 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 387 . . . . . . . . . . . . . . . . . . . 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 252 . . . . . . . . . . . . . . . . . . 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 262 . . . . . . . . . . . . . . . . . 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 3116 . . . . . . . . . . . . . . . . . . 19  |-  y  e. 
_V
205 vex 3116 . . . . . . . . . . . . . . . . . . . 20  |-  z  e. 
_V
206205eliniseg 5364 . . . . . . . . . . . . . . . . . . 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 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 )
208205eliniseg 5364 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  _V  ->  (
z  e.  ( `' ( W `  X
) " { y } )  <->  z ( W `  X )
y ) )
209204, 208ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( `' ( W `  X )
" { y } )  <->  z ( W `
 X ) y )
210203, 207, 2093bitr4g 288 . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . 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 2530 . . . . . . . . . . . . . . 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 5024 . . . . . . . . . . . . . . . . 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 3700 . . . . . . . . . . . . . . . 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 3746 . . . . . . . . . . . . . . . . . . 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 5133 . . . . . . . . . . . . . . . . . . . . 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 3691 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X ) " {
y } ) )  =  ( ( `' ( W `  X
) " { y } )  i^i  {
( X F ( W `  X ) ) } )
218 cnvimass 5355 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( `' ( W `  X
) " { y } )  C_  dom  ( W `  X )
21918adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( W `  X
)  C_  ( X  X.  X ) )
220 dmss 5200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  dom  ( X  X.  X )  =  X
223221, 222syl6sseq 3550 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  dom  ( W `  X )  C_  X
)
224218, 223syl5ss 3515 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( W `
 X ) " { y } ) 
C_  X )
225224, 194ssneldd 3507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  ( `' ( W `  X ) " {
y } ) )
226 disjsn 4088 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( `' ( W `
 X ) " { y } )  i^i  { ( X F ( W `  X ) ) } )  =  (/)  <->  -.  ( X F ( W `  X ) )  e.  ( `' ( W `
 X ) " { y } ) )
227225, 226sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( `' ( W `  X )
" { y } )  i^i  { ( X F ( W `
 X ) ) } )  =  (/) )
228217, 227syl5eq 2520 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X )
" { y } ) )  =  (/) )
229228xpeq2d 5023 . . . . . . . . . . . . . . . . . . . . . 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 5423 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  i^i  ( `' ( W `  X
) " { y } ) )  X.  (/) )  =  (/)
231229, 230syl6eq 2524 . . . . . . . . . . . . . . . . . . . . 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 2520 . . . . . . . . . . . . . . . . . . . 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 3658 . . . . . . . . . . . . . . . . . . 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 2520 . . . . . . . . . . . . . . . . . 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 3810 . . . . . . . . . . . . . . . . . 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 2524 . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . 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 2508 . . . . . . . . . . . . . . 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