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

Theorem fpwwe2lem13 9085
Description: Lemma for fpwwe2 9086. (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 3589 . . . 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 472 . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . 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 9084 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  e.  dom  W )
92, 4, 6, 7fpwwe2lem11 9083 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  W : dom  W --> ~P ( X  X.  X ) )
10 ffun 5742 . . . . . . . . . . . . . 14  |-  ( W : dom  W --> ~P ( X  X.  X )  ->  Fun  W )
11 funfvbrb 6010 . . . . . . . . . . . . . 14  |-  ( Fun 
W  ->  ( X  e.  dom  W  <->  X W
( W `  X
) ) )
129, 10, 113syl 18 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  e.  dom  W  <->  X W
( W `  X
) ) )
138, 12mpbid 215 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X W ( W `  X ) )
142, 4fpwwe2lem2 9075 . . . . . . . . . . . 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 215 . . . . . . . . . . 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 466 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
) ) )
1716simpld 466 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  X  C_  A )
1816simprd 470 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  C_  ( X  X.  X
) )
1915simprd 470 . . . . . . . . . . . . 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 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  We  X )
2117, 18, 203jca 1210 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )
222, 3, 5fpwwe2lem5 9077 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  C_  A  /\  ( W `
 X )  C_  ( X  X.  X
)  /\  ( W `  X )  We  X
) )  ->  ( X F ( W `  X ) )  e.  A )
2321, 22syldan 478 . . . . . . . . . 10  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X F ( W `  X ) )  e.  A )
2423snssd 4108 . . . . . . . . 9  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  { ( X F ( W `
 X ) ) }  C_  A )
2517, 24unssd 3601 . . . . . . . 8  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  u.  { ( X F ( W `  X ) ) } )  C_  A )
26 ssun1 3588 . . . . . . . . . . 11  |-  X  C_  ( X  u.  { ( X F ( W `
 X ) ) } )
27 xpss12 4945 . . . . . . . . . . 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 686 . . . . . . . . . 10  |-  ( X  X.  X )  C_  ( ( X  u.  { ( X F ( W `  X ) ) } )  X.  ( X  u.  {
( X F ( W `  X ) ) } ) )
2918, 28syl6ss 3430 . . . . . . . . 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 4945 . . . . . . . . . . 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 686 . . . . . . . . . 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 3601 . . . . . . . 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 541 . . . . . . 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 3741 . . . . . . . . . . . . . 14  |-  ( x 
C_  { ( X F ( W `  X ) ) }  <-> 
( x  \  {
( X F ( W `  X ) ) } )  =  (/) )
36 simpllr 777 . . . . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . . . . . 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 4437 . . . . . . . . . . . . . . . . . . 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 4870 . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . 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 182 . . . . . . . . . . . . . . . . 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 4870 . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) ( X F ( W `
 X ) )  ->  ( X F ( W `  X
) )  e.  X
)
4536, 44nsyl 125 . . . . . . . . . . . . . . . . 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 6336 . . . . . . . . . . . . . . . . . . 19  |-  ( X F ( W `  X ) )  e. 
_V
47 breq2 4399 . . . . . . . . . . . . . . . . . . . . 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 4444 . . . . . . . . . . . . . . . . . . . . 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 269 . . . . . . . . . . . . . . . . . . . 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 301 . . . . . . . . . . . . . . . . . . 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 4002 . . . . . . . . . . . . . . . . . 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 498 . . . . . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . . . . . 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 677 . . . . . . . . . . . . . . . 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 779 . . . . . . . . . . . . . . . . . . 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 2648 . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . 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 4122 . . . . . . . . . . . . . . . . . . . 20  |-  ( x 
C_  { ( X F ( W `  X ) ) }  <-> 
( x  =  (/)  \/  x  =  { ( X F ( W `
 X ) ) } ) )
5957, 58sylib 201 . . . . . . . . . . . . . . . . . . 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 384 . . . . . . . . . . . . . . . . . 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 2979 . . . . . . . . . . . . . . . . . 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 4398 . . . . . . . . . . . . . . . . . . . 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 301 . . . . . . . . . . . . . . . . . . 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 4001 . . . . . . . . . . . . . . . . . 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 269 . . . . . . . . . . . . . . . . 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 2988 . . . . . . . . . . . . . . . 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 240 . . . . . . . . . . . . . . 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 441 . . . . . . . . . . . . . 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 226 . . . . . . . . . . . . 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 3034 . . . . . . . . . . . . . . . . 17  |-  x  e. 
_V
72 difexg 4545 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  _V  ->  (
x  \  { ( X F ( W `  X ) ) } )  e.  _V )
7371, 72mp1i 13 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  ( X F ( W `  X ) )  e.  X )  /\  ( x  C_  ( X  u.  { ( X F ( W `
 X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  -> 
( x  \  {
( X F ( W `  X ) ) } )  e. 
_V )
74 wefr 4829 . . . . . . . . . . . . . . . . . 18  |-  ( ( W `  X )  We  X  ->  ( W `  X )  Fr  X )
7520, 74syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  Fr  X )
7675ad2antrr 740 . . . . . . . . . . . . . . . 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 778 . . . . . . . . . . . . . . . . . 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 3569 . . . . . . . . . . . . . . . . . 18  |-  ( X  u.  { ( X F ( W `  X ) ) } )  =  ( { ( X F ( W `  X ) ) }  u.  X
)
7977, 78syl6sseq 3464 . . . . . . . . . . . . . . . . 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 3842 . . . . . . . . . . . . . . . . 17  |-  ( x 
C_  ( { ( X F ( W `
 X ) ) }  u.  X )  <-> 
( x  \  {
( X F ( W `  X ) ) } )  C_  X )
8179, 80sylib 201 . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . 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 4801 . . . . . . . . . . . . . . . 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 1293 . . . . . . . . . . . . . . 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 4444 . . . . . . . . . . . . . . . . . . . . . . 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 4870 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( z  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
8887simprbi 471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  e.  {
( X F ( W `  X ) ) } )
89 eldifn 3545 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  -.  y  e.  { ( X F ( W `  X ) ) } )
9089adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  -.  y  e.  { ( X F ( W `  X
) ) } )
9190pm2.21d 109 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\ 
-.  ( X F ( W `  X
) )  e.  X
)  /\  ( x  C_  ( X  u.  {
( X F ( W `  X ) ) } )  /\  x  =/=  (/) ) )  /\  ( x  \  { ( X F ( W `
 X ) ) } )  =/=  (/) )  /\  y  e.  ( x  \  { ( X F ( W `  X
) ) } ) )  ->  ( y  e.  { ( X F ( W `  X
) ) }  ->  z ( W `  X
) y ) )
9288, 91syl5 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 387 . . . . . . . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . . . . . . . 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 140 . . . . . . . . . . . . . . . . . . . . 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 2806 . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  -.  ( X F ( W `
 X ) )  e.  X )
9897ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . 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 744 . . . . . . . . . . . . . . . . . . . . . . . 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 4437 . . . . . . . . . . . . . . . . . . . . . . 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 4870 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X F ( W `
 X ) ) ( X  X.  X
) y  <->  ( ( X F ( W `  X ) )  e.  X  /\  y  e.  X ) )
102101simplbi 467 . . . . . . . . . . . . . . . . . . . . . . 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 182 . . . . . . . . . . . . . . . . . . . . 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 4870 . . . . . . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X F ( W `
 X ) ) ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  e.  {
( X F ( W `  X ) ) } )
10790, 106nsyl 125 . . . . . . . . . . . . . . . . . . . . 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 4444 . . . . . . . . . . . . . . . . . . . . . . . . 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 269 . . . . . . . . . . . . . . . . . . . . . . . 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 301 . . . . . . . . . . . . . . . . . . . . . . 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 4001 . . . . . . . . . . . . . . . . . . . . . 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 498 . . . . . . . . . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . . . . . . . . . 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 677 . . . . . . . . . . . . . . . . . . . 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 553 . . . . . . . . . . . . . . . . . . 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 3588 . . . . . . . . . . . . . . . . . . . . 21  |-  x  C_  ( x  u.  { ( X F ( W `
 X ) ) } )
117 undif1 3833 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  \  { ( X F ( W `
 X ) ) } )  u.  {
( X F ( W `  X ) ) } )  =  ( x  u.  {
( X F ( W `  X ) ) } )
118116, 117sseqtr4i 3451 . . . . . . . . . . . . . . . . . . . 20  |-  x  C_  ( ( x  \  { ( X F ( W `  X
) ) } )  u.  { ( X F ( W `  X ) ) } )
119 ralun 3607 . . . . . . . . . . . . . . . . . . . 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 3479 . . . . . . . . . . . . . . . . . . . 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 64 . . . . . . . . . . . . . . . . . . 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 3544 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( x  \  { ( X F ( W `  X
) ) } )  ->  y  e.  x
)
124123adantl 473 . . . . . . . . . . . . . . . . . 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 552 . . . . . . . . . . . . . . . . 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 614 . . . . . . . . . . . . . . . 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 2855 . . . . . . . . . . . . . . 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 441 . . . . . . . . . . . . 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 2729 . . . . . . . . . . . 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 441 . . . . . . . . . . 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 1781 . . . . . . . . . 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 4798 . . . . . . . . . 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 217 . . . . . . . . 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 3565 . . . . . . . . . . . 12  |-  ( x  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( x  e.  X  \/  x  e.  { ( X F ( W `  X
) ) } ) )
136 elun 3565 . . . . . . . . . . . 12  |-  ( y  e.  ( X  u.  { ( X F ( W `  X ) ) } )  <->  ( y  e.  X  \/  y  e.  { ( X F ( W `  X
) ) } ) )
137135, 136anbi12i 711 . . . . . . . . . . 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 4830 . . . . . . . . . . . . . . . 16  |-  ( ( W `  X )  We  X  ->  ( W `  X )  Or  X )
13920, 138syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( W `  X )  Or  X )
140 solin 4783 . . . . . . . . . . . . . . 15  |-  ( ( ( W `  X
)  Or  X  /\  ( x  e.  X  /\  y  e.  X
) )  ->  (
x ( W `  X ) y  \/  x  =  y  \/  y ( W `  X ) x ) )
141139, 140sylan 479 . . . . . . . . . . . . . 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 3588 . . . . . . . . . . . . . . . . 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 4437 . . . . . . . . . . . . . . 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 4437 . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . 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 441 . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . 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 458 . . . . . . . . . . . . . . 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 4870 . . . . . . . . . . . . . . 15  |-  ( y ( X  X.  {
( X F ( W `  X ) ) } ) x  <-> 
( y  e.  X  /\  x  e.  { ( X F ( W `
 X ) ) } ) )
153151, 152sylibr 217 . . . . . . . . . . . . . 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 3589 . . . . . . . . . . . . . . 15  |-  ( X  X.  { ( X F ( W `  X ) ) } )  C_  ( ( W `  X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
155154ssbri 4438 . . . . . . . . . . . . . 14  |-  ( y ( X  X.  {
( X F ( W `  X ) ) } ) x  ->  y ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) x )
156 3mix3 1201 . . . . . . . . . . . . . 14  |-  ( y ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x  -> 
( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
157153, 155, 1563syl 18 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e.  X ) )  -> 
( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
158157ex 441 . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . 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 4870 . . . . . . . . . . . . . . 15  |-  ( x ( X  X.  {
( X F ( W `  X ) ) } ) y  <-> 
( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )
161159, 160sylibr 217 . . . . . . . . . . . . . 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 4438 . . . . . . . . . . . . . 14  |-  ( x ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y )
163 3mix1 1199 . . . . . . . . . . . . . 14  |-  ( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) y  -> 
( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
164161, 162, 1633syl 18 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  ( x  e.  X  /\  y  e.  { ( X F ( W `
 X ) ) } ) )  -> 
( x ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X
) ) } ) ) y  \/  x  =  y  \/  y
( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) x ) )
165164ex 441 . . . . . . . . . . . 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 3985 . . . . . . . . . . . . . . 15  |-  ( x  e.  { ( X F ( W `  X ) ) }  ->  x  =  ( X F ( W `
 X ) ) )
167 elsni 3985 . . . . . . . . . . . . . . 15  |-  ( y  e.  { ( X F ( W `  X ) ) }  ->  y  =  ( X F ( W `
 X ) ) )
168 eqtr3 2492 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( X F ( W `  X ) )  /\  y  =  ( X F ( W `  X ) ) )  ->  x  =  y )
169166, 167, 168syl2an 485 . . . . . . . . . . . . . 14  |-  ( ( x  e.  { ( X F ( W `
 X ) ) }  /\  y  e. 
{ ( X F ( W `  X
) ) } )  ->  x  =  y )
1701693mix2d 1206 . . . . . . . . . . . . 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 962 . . . . . . . . . . 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 225 . . . . . . . . . 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 2813 . . . . . . . . 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 6627 . . . . . . . . 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 677 . . . . . . . 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 9073 . . . . . . . . . . . . 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 9076 . . . . . . . . . . . 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 5194 . . . . . . . . . . . . . . 15  |-  ( `' ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) ) " {
y } )  C_  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )
180 fvex 5889 . . . . . . . . . . . . . . . . 17  |-  ( W `
 X )  e. 
_V
181 snex 4641 . . . . . . . . . . . . . . . . . 18  |-  { ( X F ( W `
 X ) ) }  e.  _V
182 xpexg 6612 . . . . . . . . . . . . . . . . . 18  |-  ( ( X  e.  dom  W  /\  { ( X F ( W `  X
) ) }  e.  _V )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
1838, 181, 182sylancl 675 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( X  X.  { ( X F ( W `  X ) ) } )  e.  _V )
184 unexg 6611 . . . . . . . . . . . . . . . . 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 676 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  (
( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )
186 dmexg 6743 . . . . . . . . . . . . . . . 16  |-  ( ( ( W `  X
)  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V  ->  dom  ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )  e.  _V )
187185, 186syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  dom  ( ( W `  X )  u.  ( X  X.  { ( X F ( W `  X ) ) } ) )  e.  _V )
188 ssexg 4542 . . . . . . . . . . . . . . 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 676 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  ( `' ( ( W `
 X )  u.  ( X  X.  {
( X F ( W `  X ) ) } ) )
" { y } )  e.  _V )
190189adantr 472 . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  y  e.  X )
193 simplr 770 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  X
)
194 nelne2 2740 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  X  /\  -.  ( X F ( W `  X ) )  e.  X )  ->  y  =/=  ( X F ( W `  X ) ) )
195192, 193, 194syl2anc 673 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  y  =/=  ( X F ( W `  X ) ) )
19688, 167syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z ( X  X.  {
( X F ( W `  X ) ) } ) y  ->  y  =  ( X F ( W `
 X ) ) )
197196necon3ai 2668 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =/=  ( X F ( W `  X
) )  ->  -.  z ( X  X.  { ( X F ( W `  X
) ) } ) y )
198 biorf 412 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  z ( X  X.  { ( X F ( W `  X
) ) } ) y  ->  ( z
( W `  X
) y  <->  ( z
( X  X.  {
( X F ( W `  X ) ) } ) y  \/  z ( W `
 X ) y ) ) )
199195, 197, 1983syl 18 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( z ( W `
 X ) y  <-> 
( z ( X  X.  { ( X F ( W `  X ) ) } ) y  \/  z
( W `  X
) y ) ) )
200 orcom 394 . . . . . . . . . . . . . . . . . . . 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 260 . . . . . . . . . . . . . . . . . . 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 270 . . . . . . . . . . . . . . . . . 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 3034 . . . . . . . . . . . . . . . . . . 19  |-  y  e. 
_V
204 vex 3034 . . . . . . . . . . . . . . . . . . . 20  |-  z  e. 
_V
205204eliniseg 5203 . . . . . . . . . . . . . . . . . . 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 5203 . . . . . . . . . . . . . . . . . . 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 296 . . . . . . . . . . . . . . . . 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 2469 . . . . . . . . . . . . . . . 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 2527 . . . . . . . . . . . . . . 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 4865 . . . . . . . . . . . . . . . . 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 3625 . . . . . . . . . . . . . . . 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 3682 . . . . . . . . . . . . . . . . . . 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 4972 . . . . . . . . . . . . . . . . . . . . 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 3616 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X ) " {
y } ) )  =  ( ( `' ( W `  X
) " { y } )  i^i  {
( X F ( W `  X ) ) } )
217 cnvimass 5194 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( `' ( W `  X
) " { y } )  C_  dom  ( W `  X )
21818adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( W `  X
)  C_  ( X  X.  X ) )
219 dmss 5039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( W `  X ) 
C_  ( X  X.  X )  ->  dom  ( W `  X ) 
C_  dom  ( X  X.  X ) )
220218, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  dom  ( W `  X )  C_  dom  ( X  X.  X
) )
221 dmxpid 5060 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  dom  ( X  X.  X )  =  X
222220, 221syl6sseq 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  dom  ( W `  X )  C_  X
)
223217, 222syl5ss 3429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( `' ( W `
 X ) " { y } ) 
C_  X )
224223, 193ssneldd 3421 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  -.  ( X F ( W `  X
) )  e.  ( `' ( W `  X ) " {
y } ) )
225 disjsn 4023 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( `' ( W `
 X ) " { y } )  i^i  { ( X F ( W `  X ) ) } )  =  (/)  <->  -.  ( X F ( W `  X ) )  e.  ( `' ( W `
 X ) " { y } ) )
226224, 225sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( ( `' ( W `  X )
" { y } )  i^i  { ( X F ( W `
 X ) ) } )  =  (/) )
227216, 226syl5eq 2517 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  ( X F ( W `
 X ) )  e.  X )  /\  y  e.  X )  ->  ( { ( X F ( W `  X ) ) }  i^i  ( `' ( W `  X )
" { y } ) )  =  (/) )
228227xpeq2d 4863 . . . . . . . . . . . . . . . . . . . . . 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 5261 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  i^i  ( `' ( W `  X
) " { y } ) )  X.  (/) )  =  (/)
230228, 229syl6eq 2521 . . . . . . . . . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . . . . . . . . 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 3579 . . . . . . . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . . . . . . 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 3762 . . . . . . . . . . . . . . . . . 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 2521 . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . 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 2505 . . . . . . . . . . . . . . 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 6326 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\