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

Theorem fpwwe2lem13 9009
Description: Lemma for fpwwe2 9010. (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 3654 . . . 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 463 . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . 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 9008 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  e.  dom  W )
92, 4, 6, 7fpwwe2lem11 9007 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  W : dom  W --> ~P ( X  X.  X ) )
10 ffun 5715 . . . . . . . . . . . . . 14  |-  ( W : dom  W --> ~P ( X  X.  X )  ->  Fun  W )
11 funfvbrb 5976 . . . . . . . . . . . . . 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 8999 . . . . . . . . . . . 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 457 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
) ) )
1716simpld 457 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  C_  A )
1816simprd 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  C_  ( X  X.  X
) )
1915simprd 461 . . . . . . . . . . . . 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 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  We  X )
2117, 18, 203jca 1174 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )
222, 3, 5fpwwe2lem5 9001 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  C_  A  /\  ( W `
 X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )  ->  ( X F ( W `  X ) )  e.  A )
2321, 22syldan 468 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X F ( W `  X ) )  e.  A )
2423snssd 4161 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  { ( X F ( W `
 X ) ) }  C_  A )
2517, 24unssd 3666 . . . . . . . 8  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  u.  { ( X F ( W `  X ) ) } )  C_  A )
26 ssun1 3653 . . . . . . . . . . 11  |-  X  C_  ( X  u.  { ( X F ( W `
 X ) ) } )
27 xpss12 5096 . . . . . . . . . . 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 670 . . . . . . . . . 10  |-  ( X  X.  X )  C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  {
( X F ( W `  X ) ) } ) )
2918, 28syl6ss 3501 . . . . . . . . 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 5096 . . . . . . . . . . 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 670 . . . . . . . . . 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 3666 . . . . . . . 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 530 . . . . . . 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 3873 . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . . 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 4480 . . . . . . . . . . . . . . . . . . 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 5019 . . . . . . . . . . . . . . . . . . . 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 458 . . . . . . . . . . . . . . . . . . 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 5019 . . . . . . . . . . . . . . . . . . 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 458 . . . . . . . . . . . . . . . . . 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 6298 . . . . . . . . . . . . . . . . . . 19  |-  ( X F ( W `  X ) )  e. 
_V
47 breq2 4443 . . . . . . . . . . . . . . . . . . . . 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 4487 . . . . . . . . . . . . . . . . . . . . 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 292 . . . . . . . . . . . . . . . . . . 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 4056 . . . . . . . . . . . . . . . . . 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 488 . . . . . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . . . . 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 2656 . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . 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 4174 . . . . . . . . . . . . . . . . . . . 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 375 . . . . . . . . . . . . . . . . . 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 3057 . . . . . . . . . . . . . . . . . 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 4442 . . . . . . . . . . . . . . . . . . . 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 292 . . . . . . . . . . . . . . . . . . 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 4055 . . . . . . . . . . . . . . . . . 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 3066 . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . 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 3109 . . . . . . . . . . . . . . . . 17  |-  x  e. 
_V
72 difexg 4585 . . . . . . . . . . . . . . . . 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 4858 . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . 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 3634 . . . . . . . . . . . . . . . . . 18  |-  ( X  u.  { ( X F ( W `  X ) ) } )  =  ( { ( X F ( W `  X ) ) }  u.  X
)
7977, 78syl6sseq 3535 . . . . . . . . . . . . . . . . 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 3899 . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . 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 4830 . . . . . . . . . . . . . . . 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 1227 . . . . . . . . . . . . . . 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 4487 . . . . . . . . . . . . . . . . . . . . . . 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 5019 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( z  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
8887simprbi 462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  e.  {
( X F ( W `  X ) ) } )
89 eldifn 3613 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  -.  y  e.  { ( X F ( W `  X ) ) } )
9089adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . 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 378 . . . . . . . . . . . . . . . . . . . . . . 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 2864 . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  -.  ( X F ( W `
 X ) )  e.  X )
9897ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 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 727 . . . . . . . . . . . . . . . . . . . . . . . 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 4480 . . . . . . . . . . . . . . . . . . . . . . 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 5019 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) y  <->  ( ( X F ( W `  X ) )  e.  X  /\  y  e.  X ) )
102101simplbi 458 . . . . . . . . . . . . . . . . . . . . . . 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 5019 . . . . . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . 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 4487 . . . . . . . . . . . . . . . . . . . . . . . . 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 292 . . . . . . . . . . . . . . . . . . . . . . 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 4055 . . . . . . . . . . . . . . . . . . . . . 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 488 . . . . . . . . . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . . . . . . . . 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 542 . . . . . . . . . . . . . . . . . . 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 3653 . . . . . . . . . . . . . . . . . . . . 21  |-  x  C_  ( x  u.  { ( X F ( W `
 X ) ) } )
117 undif1 3891 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  \  { ( X F ( W `
 X ) ) } )  u.  {
( X F ( W `  X ) ) } )  =  ( x  u.  {
( X F ( W `  X ) ) } )
118116, 117sseqtr4i 3522 . . . . . . . . . . . . . . . . . . . 20  |-  x  C_  ( ( x  \  { ( X F ( W `  X
) ) } )  u.  { ( X F ( W `  X ) ) } )
119 ralun 3672 . . . . . . . . . . . . . . . . . . . 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 3550 . . . . . . . . . . . . . . . . . . . 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 3612 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  y  e.  x
)
124123adantl 464 . . . . . . . . . . . . . . . . . 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 541 . . . . . . . . . . . . . . . . 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 601 . . . . . . . . . . . . . . . 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 2925 . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . 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 2771 . . . . . . . . . . . 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 432 . . . . . . . . . . 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 1724 . . . . . . . . . 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 4827 . . . . . . . . . 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 3631 . . . . . . . . . . . 12  |-  ( x  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( x  e.  X  \/  x  e.  { ( X F ( W `  X
) ) } ) )
136 elun 3631 . . . . . . . . . . . 12  |-  ( y  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( y  e.  X  \/  y  e.  { ( X F ( W `  X
) ) } ) )
137135, 136anbi12i 695 . . . . . . . . . . 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 4859 . . . . . . . . . . . . . . . 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 4812 . . . . . . . . . . . . . . 15  |-  ( ( ( W `  X
)  Or  X  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x ( W `  X ) y  \/  x  =  y  \/  y ( W `  X ) x ) )
141139, 140sylan 469 . . . . . . . . . . . . . 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 3653 . . . . . . . . . . . . . . . . 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 4480 . . . . . . . . . . . . . . 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 4480 . . . . . . . . . . . . . . 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 1305 . . . . . . . . . . . . . 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 432 . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . 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 5019 . . . . . . . . . . . . . . 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 3654 . . . . . . . . . . . . . . 15  |-  ( X  X.  { ( X F ( W `  X ) ) } )  C_  ( ( W `  X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
155154ssbri 4481 . . . . . . . . . . . . . 14  |-  ( y ( X  X.  {
( X F ( W `  X ) ) } ) x  ->  y ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) x )
156 3mix3 1165 . . . . . . . . . . . . . 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 432 . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . 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 5019 . . . . . . . . . . . . . . 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 4481 . . . . . . . . . . . . . 14  |-  ( x ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y )
163 3mix1 1163 . . . . . . . . . . . . . 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 432 . . . . . . . . . . . 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 4041 . . . . . . . . . . . . . . 15  |-  ( x  e.  { ( X F ( W `  X ) ) }  ->  x  =  ( X F ( W `
 X ) ) )
167 elsni 4041 . . . . . . . . . . . . . . 15  |-  ( y  e.  { ( X F ( W `  X ) ) }  ->  y  =  ( X F ( W `
 X ) ) )
168 eqtr3 2482 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( X F ( W `  X ) )  /\  y  =  ( X F ( W `  X ) ) )  ->  x  =  y )
169166, 167, 168syl2an 475 . . . . . . . . . . . . . 14  |-  ( ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e. 
{ ( X F ( W `  X
) ) } )  ->  x  =  y )
1701693mix2d 1170 . . . . . . . . . . . . 13  |-  ( ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e. 
{ ( X F ( W `  X
) ) } )  ->  ( x ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) x ) )
171170a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( x  e.  {
( X F ( W `  X ) ) }  /\  y  e.  { ( X F ( W `  X
) ) } )  ->  ( x ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  \/  x  =  y  \/  y ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) ) x ) ) )
172149, 158, 165, 171ccased 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 ) ) )
173137, 172syl5bi 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 ) ) )
174173ralrimivv 2874 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  A. x  e.  ( X  u.  {
( X F ( W `  X ) ) } ) A. y  e.  ( X  u.  { ( X F ( W `  X
) ) } ) ( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
175 dfwe2 6590 . . . . . . . . 9  |-  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  We  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) )  Fr  ( X  u.  { ( X F ( W `  X ) ) } )  /\  A. x  e.  ( X  u.  {
( X F ( W `  X ) ) } ) A. y  e.  ( X  u.  { ( X F ( W `  X
) ) } ) ( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) ) )
176134, 174, 175sylanbrc 662 . . . . . . . 8  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  We  ( X  u.  { ( X F ( W `  X ) ) } ) )
1772fpwwe2cbv 8997 . . . . . . . . . . . . 13  |-  W  =  { <. a ,  s
>.  |  ( (
a  C_  A  /\  s  C_  ( a  X.  a ) )  /\  ( s  We  a  /\  A. z  e.  a 
[. ( `' s
" { z } )  /  b ]. ( b F ( s  i^i  ( b  X.  b ) ) )  =  z ) ) }
178177, 4, 13fpwwe2lem3 9000 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( `' ( W `  X )
" { y } ) F ( ( W `  X )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) ) )  =  y )
179 cnvimass 5345 . . . . . . . . . . . . . . 15  |-  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  C_  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )
180 fvex 5858 . . . . . . . . . . . . . . . . 17  |-  ( W `
 X )  e. 
_V
181 snex 4678 . . . . . . . . . . . . . . . . . 18  |-  { ( X F ( W `
 X ) ) }  e.  _V
182 xpexg 6575 . . . . . . . . . . . . . . . . . 18  |-  ( ( X  e.  dom  W  /\  { ( X F ( W `  X
) ) }  e.  _V )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
1838, 181, 182sylancl 660 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
184 unexg 6574 . . . . . . . . . . . . . . . . 17  |-  ( ( ( W `  X
)  e.  _V  /\  ( X  X.  { ( X F ( W `
 X ) ) } )  e.  _V )  ->  ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  e.  _V )
185180, 183, 184sylancr 661 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )
186 dmexg 6704 . . . . . . . . . . . . . . . 16  |-  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V  ->  dom  ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  e.  _V )
187185, 186syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )
188 ssexg 4583 . . . . . . . . . . . . . . 15  |-  ( ( ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) " { y } )  C_  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  /\  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )  ->  ( `' ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  e. 
_V )
189179, 187, 188sylancr 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } )  e.  _V )
190189adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) " { y } )  e.  _V )
191 id 22 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( `' ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  ->  u  =  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } ) )
192 simpr 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  y  e.  X )
193 simplr 753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  X
)
194 nelne2 2784 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  X  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  y  =/=  ( X F ( W `  X ) ) )
195192, 193, 194syl2anc 659 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  y  =/=  ( X F ( W `  X ) ) )
19688, 167syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  =  ( X F ( W `
 X ) ) )
197196necon3ai 2682 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =/=  ( X F ( W `  X
) )  ->  -.  z ( X  X.  { ( X F ( W `  X
) ) } ) y )
198 biorf 403 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  z ( X  X.  { ( X F ( W `  X
) ) } ) y  ->  ( z
( W `  X
) y  <->  ( z
( X  X.  {
( X F ( W `  X ) ) } ) y  \/  z ( W `
 X ) y ) ) )
199195, 197, 1983syl 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 ) ) )
200 orcom 385 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z ( X  X.  { ( X F ( W `  X
) ) } ) y  \/  z ( W `  X ) y )  <->  ( z
( W `  X
) y  \/  z
( X  X.  {
( X F ( W `  X ) ) } ) y ) )
201200, 85bitr4i 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 )
202199, 201syl6rbb 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 ) )
203 vex 3109 . . . . . . . . . . . . . . . . . . 19  |-  y  e. 
_V
204 vex 3109 . . . . . . . . . . . . . . . . . . . 20  |-  z  e. 
_V
205204eliniseg 5354 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  _V  ->  (
z  e.  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  <->  z (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y ) )
206203, 205ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( `' ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  <->  z (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y )
207204eliniseg 5354 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  _V  ->  (
z  e.  ( `' ( W `  X
) " { y } )  <->  z ( W `  X )
y ) )
208203, 207ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( `' ( W `  X )
" { y } )  <->  z ( W `
 X ) y )
209202, 206, 2083bitr4g 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 } ) ) )
210209eqrdv 2451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) " { y } )  =  ( `' ( W `  X ) " {
y } ) )
211191, 210sylan9eqr 2517 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  u  =  ( `' ( W `  X )
" { y } ) )
212211sqxpeqd 5014 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  (
u  X.  u )  =  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) )
213212ineq2d 3686 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  (
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
u  X.  u ) )  =  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) ) )
214 indir 3743 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) )  =  ( ( ( W `
 X )  i^i  ( ( `' ( W `  X )
" { y } )  X.  ( `' ( W `  X
) " { y } ) ) )  u.  ( ( X  X.  { ( X F ( W `  X ) ) } )  i^i  ( ( `' ( W `  X ) " {
y } )  X.  ( `' ( W `
 X ) " { y } ) ) ) )
215 inxp 5124 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( X  X.  { ( X F ( W `
 X ) ) } )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) )  =  ( ( X  i^i  ( `' ( W `  X ) " {
y } ) )  X.  ( { ( X F ( W `
 X ) ) }  i^i  ( `' ( W `  X
) " { y } ) ) )
216 incom 3677 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X ) " {
y } ) )  =  ( ( `' ( W `  X
) " { y } )  i^i  {
( X F ( W `  X ) ) } )
217 cnvimass 5345 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( `' ( W `  X
) " { y } )  C_  dom  ( W `  X )
21818adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( W `  X
)  C_  ( X  X.  X ) )
219 dmss 5191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( W `  X ) 
C_  ( X  X.  X )  ->  dom  ( W `  X ) 
C_  dom  ( X  X.  X ) )
220218, 219syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  dom  ( W `  X )  C_  dom  ( X  X.  X
) )
221 dmxpid 5211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  dom  ( X  X.  X )  =  X
222220, 221syl6sseq 3535 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  dom  ( W `  X )  C_  X
)
223217, 222syl5ss 3500 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( W `
 X ) " { y } ) 
C_  X )
224223, 193ssneldd 3492 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  ( `' ( W `  X ) " {
y } ) )
225 disjsn 4076 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( `' ( W `
 X ) " { y } )  i^i  { ( X F ( W `  X ) ) } )  =  (/)  <->  -.  ( X F ( W `  X ) )  e.  ( `' ( W `
 X ) " { y } ) )
226224, 225sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( `' ( W `  X )
" { y } )  i^i  { ( X F ( W `
 X ) ) } )  =  (/) )
227216, 226syl5eq 2507 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X )
" { y } ) )  =  (/) )
228227xpeq2d 5012 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( X  i^i  ( `' ( W `  X ) " {
y } ) )  X.  ( { ( X F ( W `
 X ) ) }  i^i  ( `' ( W `  X
) " { y } ) ) )  =  ( ( X  i^i  ( `' ( W `  X )
" { y } ) )  X.  (/) ) )
229 xp0 5410 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  i^i  ( `' ( W `  X
) " { y } ) )  X.  (/) )  =  (/)
230228, 229syl6eq 2511 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( X  i^i  ( `' ( W `  X ) " {
y } ) )  X.  ( { ( X F ( W `
 X ) ) }  i^i  ( `' ( W `  X
) " { y } ) ) )  =  (/) )
231215, 230syl5eq 2507 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( X  X.  { ( X F ( W `  X
) ) } )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) )  =  (/) )
232231uneq2d 3644 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( ( W `
 X )  i^i  ( ( `' ( W `  X )
" { y } )  X.  ( `' ( W `  X
) " { y } ) ) )  u.  ( ( X  X.  { ( X F ( W `  X ) ) } )  i^i  ( ( `' ( W `  X ) " {
y } )  X.  ( `' ( W `
 X ) " { y } ) ) ) )  =  ( ( ( W `
 X )  i^i  ( ( `' ( W `  X )
" { y } )  X.  ( `' ( W `  X
) " { y } ) ) )  u.  (/) ) )
233214, 232syl5eq 2507 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) )  =  ( ( ( W `  X
)  i^i  ( ( `' ( W `  X ) " {
y } )  X.  ( `' ( W `
 X ) " { y } ) ) )  u.  (/) ) )
234 un0 3809 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( W `  X
)  i^i  ( ( `' ( W `  X ) " {
y } )  X.  ( `' ( W `
 X ) " { y } ) ) )  u.  (/) )  =  ( ( W `  X )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) )
235233, 234syl6eq 2511 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) )  =  ( ( W `  X )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) ) )
236235adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  (
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) )  =  ( ( W `  X )  i^i  (
( `' ( W `
 X ) " { y } )  X.  ( `' ( W `  X )
" { y } ) ) ) )
237213, 236eqtrd 2495 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  y  e.  X
)  /\  u  =  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } ) )  ->  (
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  i^i  (
u  X.  u ) )  =  ( ( W `  X )  i^i  ( ( `' ( W `  X
) " { y } )  X.  ( `' ( W `  X ) " {
y } ) ) ) )
238211, 237oveq12d 6288 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  -.  (