Users' Mathboxes Mathbox for Giovanni Mascellani < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ac6s6 Structured version   Unicode version

Theorem ac6s6 29007
Description: Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
Hypotheses
Ref Expression
ac6s6.1  |-  F/ y ps
ac6s6.2  |-  A  e. 
_V
ac6s6.3  |-  ( y  =  ( f `  x )  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ac6s6  |-  E. f A. x  e.  A  ( E. y ph  ->  ps )
Distinct variable groups:    ph, f    x, y    x, A, f    y,
f    A, f
Allowed substitution hints:    ph( x, y)    ps( x, y, f)    A( y)

Proof of Theorem ac6s6
StepHypRef Expression
1 hbe1 1777 . . . . . 6  |-  ( E. y ph  ->  A. y E. y ph )
2 iftrue 3816 . . . . . . 7  |-  ( E. y ph  ->  if ( E. y ph ,  { y  |  ph } ,  _V )  =  { y  |  ph } )
32abeq2d 2553 . . . . . 6  |-  ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )
41, 3exbidh 1643 . . . . 5  |-  ( E. y ph  ->  ( E. y  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  E. y ph ) )
54ibir 242 . . . 4  |-  ( E. y ph  ->  E. y 
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )
)
6 vex 2994 . . . . . 6  |-  y  e. 
_V
76exiftru 1711 . . . . 5  |-  E. y 
y  e.  _V
81hbn 1829 . . . . . 6  |-  ( -. 
E. y ph  ->  A. y  -.  E. y ph )
9 iffalse 3818 . . . . . . 7  |-  ( -. 
E. y ph  ->  if ( E. y ph ,  { y  |  ph } ,  _V )  =  _V )
109eleq2d 2510 . . . . . 6  |-  ( -. 
E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )
118, 10exbidh 1643 . . . . 5  |-  ( -. 
E. y ph  ->  ( E. y  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  E. y  y  e. 
_V ) )
127, 11mpbiri 233 . . . 4  |-  ( -. 
E. y ph  ->  E. y  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )
)
135, 12pm2.61i 164 . . 3  |-  E. y 
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )
1413rgenw 2802 . 2  |-  A. x  e.  A  E. y 
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )
15 nfe1 1778 . . . 4  |-  F/ y E. y ph
16 ac6s6.1 . . . 4  |-  F/ y ps
1715, 16nfim 1853 . . 3  |-  F/ y ( E. y ph  ->  ps )
18 ac6s6.2 . . 3  |-  A  e. 
_V
19 ac6s6.3 . . . . . 6  |-  ( y  =  ( f `  x )  ->  ( ph 
<->  ps ) )
20 id 22 . . . . . . . . . . . . . . 15  |-  ( -. 
ph  ->  -.  ph )
2120a1i 11 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  -.  ph )
)
22 ax-1 6 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  -.  (
( y  =  ( f `  x )  ->  ( ph  <->  ps )
)  ->  ( ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) ) )
23 tsim3 28966 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ( ( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) )  -> 
( E. y ph  ->  ( y  =  ( f `  x )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) ) )  \/  (
( y  =  ( f `  x )  ->  ( ph  <->  ps )
)  ->  ( ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) ) )
2423a1d 25 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( -.  ( ( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) )  -> 
( E. y ph  ->  ( y  =  ( f `  x )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) ) )  \/  (
( y  =  ( f `  x )  ->  ( ph  <->  ps )
)  ->  ( ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) ) ) )
2522, 24cnf2dd 28917 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  -.  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) )
26 tsim3 28966 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ( E. y ph  ->  ( y  =  ( f `  x )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) )  \/  ( ( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) )
2726a1d 25 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( -.  ( E. y ph  ->  ( y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) )  \/  ( ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) ) )
2825, 27cnf2dd 28917 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  -.  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )
29 tsim2 28965 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( E. y ph  \/  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )
3029a1d 25 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( E. y ph  \/  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) )
3128, 30cnf2dd 28917 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  E. y ph ) )
32 tsim2 28965 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  \/  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) )
3332a1d 25 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  \/  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) ) )
3425, 33cnf2dd 28917 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) ) ) )
3531, 34mpdd 40 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) ) )
36 tsbi4 28970 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
( -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  ph )  \/ 
-.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) ) )
3736a1d 25 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( ( -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  ph )  \/  -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) ) ) )
3835, 37cnfn2dd 28919 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( -.  y  e.  if ( E. y ph ,  {
y  |  ph } ,  _V )  \/  ph ) ) )
3921, 38cnf2dd 28917 . . . . . . . . . . . . 13  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) ) )
40 tsim3 28966 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ( y  =  ( f `  x )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) )  \/  ( E. y ph  ->  ( y  =  ( f `  x
)  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) ) ) )
4140a1d 25 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( -.  ( y  =  ( f `  x )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) )  \/  ( E. y ph  ->  ( y  =  ( f `  x
)  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) ) ) ) )
4228, 41cnf2dd 28917 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  -.  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) )
43 tsim3 28966 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) )  \/  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) )
4443a1d 25 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) )  \/  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )
4542, 44cnf2dd 28917 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  -.  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) )
46 tsbi2 28968 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  ( E. y ph  ->  ps ) )  \/  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) )
4746a1d 25 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  ( E. y ph  ->  ps ) )  \/  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) )
4845, 47cnf2dd 28917 . . . . . . . . . . . . 13  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  ( E. y ph  ->  ps )
) ) )
4939, 48cnf1dd 28916 . . . . . . . . . . . 12  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( E. y ph  ->  ps )
) )
50 tsim2 28965 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
y  =  ( f `
 x )  \/  ( y  =  ( f `  x )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) ) )
5150a1d 25 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( y  =  ( f `  x )  \/  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )
5242, 51cnf2dd 28917 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  y  =  ( f `  x
) ) )
53 simplim 151 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
y  =  ( f `
 x )  -> 
( ph  <->  ps ) ) )
5452, 53syld 44 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( ph  <->  ps ) ) )
55 tsbi3 28969 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
( ph  \/  -.  ps )  \/  -.  ( ph  <->  ps ) ) )
5655a1d 25 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( ( ph  \/  -.  ps )  \/  -.  ( ph  <->  ps )
) ) )
5754, 56cnfn2dd 28919 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( ph  \/  -.  ps ) ) )
5821, 57cnf1dd 28916 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  -.  ps )
)
59 tsim1 28964 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
( -.  E. y ph  \/  ps )  \/ 
-.  ( E. y ph  ->  ps ) ) )
6059a1d 25 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( ( -.  E. y ph  \/  ps )  \/  -.  ( E. y ph  ->  ps ) ) ) )
6160or32dd 28920 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( ( -.  E. y ph  \/  -.  ( E. y ph  ->  ps ) )  \/ 
ps ) ) )
6258, 61cnf2dd 28917 . . . . . . . . . . . . 13  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  ( -.  E. y ph  \/  -.  ( E. y ph  ->  ps ) ) ) )
6331, 62cnfn1dd 28918 . . . . . . . . . . . 12  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -.  ph  ->  -.  ( E. y ph  ->  ps ) ) )
6449, 63contrd 28923 . . . . . . . . . . 11  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ph )
6564a1d 25 . . . . . . . . . 10  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ph ) )
66 ax-1 6 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  -.  (
( y  =  ( f `  x )  ->  ( ph  <->  ps )
)  ->  ( ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) ) )
6723a1d 25 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( -.  ( ( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) )  -> 
( E. y ph  ->  ( y  =  ( f `  x )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) ) )  \/  (
( y  =  ( f `  x )  ->  ( ph  <->  ps )
)  ->  ( ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) ) ) )
6866, 67cnf2dd 28917 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  -.  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) )
6926a1d 25 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( -.  ( E. y ph  ->  ( y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) )  \/  ( ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) ) )
7068, 69cnf2dd 28917 . . . . . . . . . . . . 13  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  -.  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )
7129a1d 25 . . . . . . . . . . . . 13  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( E. y ph  \/  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) )
7270, 71cnf2dd 28917 . . . . . . . . . . . 12  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  E. y ph ) )
7332a1d 25 . . . . . . . . . . . . 13  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( ( E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  \/  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) ) ) )
7468, 73cnf2dd 28917 . . . . . . . . . . . 12  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) ) ) )
7572, 74mpdd 40 . . . . . . . . . . 11  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) ) )
76 tsbi3 28969 . . . . . . . . . . . 12  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  -.  ph )  \/ 
-.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) ) )
7776a1d 25 . . . . . . . . . . 11  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  -.  ph )  \/ 
-.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) ) ) )
7875, 77cnfn2dd 28919 . . . . . . . . . 10  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  -.  ph )
) )
7965, 78cnfn2dd 28919 . . . . . . . . 9  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )
) )
8040a1d 25 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( -.  ( y  =  ( f `  x )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) )  \/  ( E. y ph  ->  ( y  =  ( f `  x
)  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) ) ) ) )
8170, 80cnf2dd 28917 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  -.  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) )
8250a1d 25 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( y  =  ( f `  x )  \/  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )
8381, 82cnf2dd 28917 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  y  =  ( f `  x
) ) )
8483, 53syld 44 . . . . . . . . . . . . 13  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( ph  <->  ps ) ) )
85 tsbi4 28970 . . . . . . . . . . . . . 14  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
( -.  ph  \/  ps )  \/  -.  ( ph  <->  ps ) ) )
8685a1d 25 . . . . . . . . . . . . 13  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( ( -.  ph  \/  ps )  \/  -.  ( ph  <->  ps )
) ) )
8784, 86cnfn2dd 28919 . . . . . . . . . . . 12  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( -.  ph  \/  ps ) ) )
8865, 87cnfn1dd 28918 . . . . . . . . . . 11  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ps )
)
8988a1dd 46 . . . . . . . . . 10  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( E. y ph  ->  ps )
) )
90 tsbi1 28967 . . . . . . . . . . . 12  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  (
( -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  -.  ( E. y ph  ->  ps ) )  \/  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) )
9190a1d 25 . . . . . . . . . . 11  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( ( -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  -.  ( E. y ph  ->  ps ) )  \/  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) ) )
9291or32dd 28920 . . . . . . . . . 10  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( ( -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) )  \/ 
-.  ( E. y ph  ->  ps ) ) ) )
9389, 92cnfn2dd 28919 . . . . . . . . 9  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( -.  y  e.  if ( E. y ph ,  {
y  |  ph } ,  _V )  \/  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) )
9479, 93cnfn1dd 28918 . . . . . . . 8  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) )
9543a1d 25 . . . . . . . . 9  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) )  \/  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )
9681, 95cnf2dd 28917 . . . . . . . 8  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  ->  ( -. F.  ->  -.  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) )
9794, 96contrd 28923 . . . . . . 7  |-  ( -.  ( ( y  =  ( f `  x
)  ->  ( ph  <->  ps ) )  ->  (
( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) ) )  -> F.  )
9897efald2 28901 . . . . . 6  |-  ( ( y  =  ( f `
 x )  -> 
( ph  <->  ps ) )  -> 
( ( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> 
ph ) )  -> 
( E. y ph  ->  ( y  =  ( f `  x )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y ph  ->  ps ) ) ) ) ) )
9919, 98ax-mp 5 . . . . 5  |-  ( ( E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ph ) )  ->  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) ) )
1003, 99ax-mp 5 . . . 4  |-  ( E. y ph  ->  (
y  =  ( f `
 x )  -> 
( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  ( E. y ph  ->  ps ) ) ) )
1016a1i 11 . . . . . . 7  |-  ( -. 
E. y ph  ->  y  e.  _V )
102 id 22 . . . . . . . . . . . 12  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  -.  (
( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -. 
E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) ) )
103 tsim2 28965 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  E. y ph  \/  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) ) )
104103ord 377 . . . . . . . . . . . . . 14  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  -.  E. y ph  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) ) )
105104a1dd 46 . . . . . . . . . . . . 13  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  -.  E. y ph  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
)  ->  ( -.  E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) ) ) )
106105a1dd 46 . . . . . . . . . . . 12  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  -.  E. y ph  ->  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -. 
E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) ) ) )
107102, 106mt3d 125 . . . . . . . . . . 11  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  -.  E. y ph )
108107a1d 25 . . . . . . . . . 10  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -. F.  ->  -.  E. y ph ) )
109 simplim 151 . . . . . . . . . 10  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  E. y ph  ->  y  e.  _V ) )
110108, 109syld 44 . . . . . . . . 9  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -. F.  ->  y  e.  _V ) )
111 tsim2 28965 . . . . . . . . . . . . . 14  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  \/  ( ( -. 
E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) ) )
112111ord 377 . . . . . . . . . . . . 13  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
)  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) ) )
113112a1dd 46 . . . . . . . . . . . 12  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
)  ->  ( ( -.  E. y ph  ->  y  e.  _V )  -> 
( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
)  ->  ( -.  E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) ) ) ) )
114102, 113mt3d 125 . . . . . . . . . . 11  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) ) )
115108, 114syld 44 . . . . . . . . . 10  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -. F.  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
) )
116 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( -.  ( y  e.  if ( E. y ph ,  {
y  |  ph } ,  _V )  <->  y  e.  _V )  \/  -.  y  e.  _V )  ->  -.  ( -.  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V )  \/ 
-.  y  e.  _V ) )
117116notornotel2 28922 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( -.  ( y  e.  if ( E. y ph ,  {
y  |  ph } ,  _V )  <->  y  e.  _V )  \/  -.  y  e.  _V )  ->  y  e.  _V )
118117a1i 11 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  y  e.  _V ) )
119116notornotel1 28921 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( -.  ( y  e.  if ( E. y ph ,  {
y  |  ph } ,  _V )  <->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )
120119a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
) )
121 tsbi3 28969 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  -.  y  e.  _V )  \/  -.  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) ) )
122121a1d 25 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( ( y  e.  if ( E. y ph ,  {
y  |  ph } ,  _V )  \/  -.  y  e.  _V )  \/  -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
) ) )
123120, 122cnfn2dd 28919 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  -.  y  e.  _V ) ) )
124118, 123cnfn2dd 28919 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )
) )
125 a1tru 1385 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  -> T.  )
126125a1d 25 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  -> T.  ) )
127 tsbi1 28967 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( ( -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  -. T.  )  \/  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) )
128127a1d 25 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( ( -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  -. T.  )  \/  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) ) )
129128or32dd 28920 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( ( -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) )  \/  -. T.  ) ) )
130126, 129cnfn2dd 28919 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( -.  y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  \/  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )
131124, 130cnfn1dd 28918 . . . . . . . . . . . . . 14  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) )
132131a1dd 46 . . . . . . . . . . . . 13  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )
133132a1dd 46 . . . . . . . . . . . 12  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( ( -. 
E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) ) )
134 ax-1 6 . . . . . . . . . . . . 13  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  -.  ( ( -.  E. y ph  ->  y  e.  _V )  -> 
( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
)  ->  ( -.  E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) ) ) ) )
135 tsim3 28966 . . . . . . . . . . . . . 14  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
)  ->  ( -.  E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) )  \/  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) ) ) )
136135a1d 25 . . . . . . . . . . . . 13  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  ( -.  (
( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
)  ->  ( -.  E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) )  \/  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) ) ) ) )
137134, 136cnf2dd 28917 . . . . . . . . . . . 12  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )  \/  -.  y  e.  _V )  ->  -.  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) ) )
138133, 137contrd 28923 . . . . . . . . . . 11  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -.  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V )  \/ 
-.  y  e.  _V ) )
139138a1d 25 . . . . . . . . . 10  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -. F.  ->  ( -.  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V )  \/ 
-.  y  e.  _V ) ) )
140115, 139cnfn1dd 28918 . . . . . . . . 9  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  ->  ( -. F.  ->  -.  y  e.  _V ) )
141110, 140contrd 28923 . . . . . . . 8  |-  ( -.  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) ) )  -> F.  )
142141efald2 28901 . . . . . . 7  |-  ( ( -.  E. y ph  ->  y  e.  _V )  ->  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  y  e.  _V )
)  ->  ( -.  E. y ph  ->  (
y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) ) ) )
143101, 142ax-mp 5 . . . . . 6  |-  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <->  y  e.  _V ) )  ->  ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) ) )
14410, 143ax-mp 5 . . . . 5  |-  ( -. 
E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V )  <-> T.  ) )
145 ax-1 6 . . . . . . . . . 10  |-  ( -.  ( ( -.  E. y ph  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<-> T.  ) )  -> 
( -.  E. y ph  ->  ( y  =  ( f `  x
)  ->  ( y  e.  if ( E. y ph ,  { y  |  ph } ,  _V ) 
<->  ( E. y