Metamath Proof Explorer

Theorem ac6s6

Description: Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018)

Ref Expression
Hypotheses ac6s6.1 
|- F/ y ps
ac6s6.2 
|- A e. _V
ac6s6.3 
|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion ac6s6 
|- E. f A. x e. A ( E. y ph -> ps )

Proof

Step Hyp Ref Expression
1 ac6s6.1 
 |-  F/ y ps
2 ac6s6.2 
 |-  A e. _V
3 ac6s6.3 
 |-  ( y = ( f ` x ) -> ( ph <-> ps ) )
4 hbe1 
 |-  ( E. y ph -> A. y E. y ph )
5 iftrue 
 |-  ( E. y ph -> if ( E. y ph , { y | ph } , _V ) = { y | ph } )
6 5 eqabrd 
 |-  ( E. y ph -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ph ) )
7 4 6 exbidh 
 |-  ( E. y ph -> ( E. y y e. if ( E. y ph , { y | ph } , _V ) <-> E. y ph ) )
8 7 ibir 
 |-  ( E. y ph -> E. y y e. if ( E. y ph , { y | ph } , _V ) )
9 vex 
 |-  y e. _V
10 9 exgen 
 |-  E. y y e. _V
11 4 hbn 
 |-  ( -. E. y ph -> A. y -. E. y ph )
12 iffalse 
 |-  ( -. E. y ph -> if ( E. y ph , { y | ph } , _V ) = _V )
13 12 eleq2d 
 |-  ( -. E. y ph -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> y e. _V ) )
14 11 13 exbidh 
 |-  ( -. E. y ph -> ( E. y y e. if ( E. y ph , { y | ph } , _V ) <-> E. y y e. _V ) )
15 10 14 mpbiri 
 |-  ( -. E. y ph -> E. y y e. if ( E. y ph , { y | ph } , _V ) )
16 8 15 pm2.61i 
 |-  E. y y e. if ( E. y ph , { y | ph } , _V )
17 16 rgenw 
 |-  A. x e. A E. y y e. if ( E. y ph , { y | ph } , _V )
18 nfe1 
 |-  F/ y E. y ph
19 18 1 nfim 
 |-  F/ y ( E. y ph -> ps )
20 id 
 |-  ( -. ph -> -. ph )
21 20 a1i 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) ) ) ) ) )
24 23 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) ) ) )
25 22 24 cnf2dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) ) ) ) )
27 26 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) ) )
28 25 27 cnf2dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) ) ) )
30 29 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) )
31 28 30 cnf2dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) ) ) ) )
33 32 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) ) )
34 25 33 cnf2dd 
 |-  ( -. ( ( 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 ) ) ) )
35 31 34 mpdd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) )
37 36 a1d 
 |-  ( -. ( ( 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 ) ) ) )
38 35 37 cnfn2dd 
 |-  ( -. ( ( 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 ) ) )
39 21 38 cnf2dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) ) ) )
41 40 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) )
42 28 41 cnf2dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) ) )
44 43 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) )
45 42 44 cnf2dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) )
47 46 a1d 
 |-  ( -. ( ( 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 ) ) ) ) )
48 45 47 cnf2dd 
 |-  ( -. ( ( 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 ) ) ) )
49 39 48 cnf1dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) ) )
51 50 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) )
52 42 51 cnf2dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) )
54 52 53 syld 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) )
56 55 a1d 
 |-  ( -. ( ( 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 ) ) ) )
57 54 56 cnfn2dd 
 |-  ( -. ( ( 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 ) ) )
58 21 57 cnf1dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) )
60 59 a1d 
 |-  ( -. ( ( 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 ) ) ) )
61 60 or32dd 
 |-  ( -. ( ( 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 ) ) )
62 58 61 cnf2dd 
 |-  ( -. ( ( 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 ) ) ) )
63 31 62 cnfn1dd 
 |-  ( -. ( ( 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 ) ) )
64 49 63 contrd 
 |-  ( -. ( ( 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 )
65 64 a1d 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) ) ) ) ) )
67 23 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) ) ) )
68 66 67 cnf2dd 
 |-  ( -. ( ( 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 ) ) ) ) ) ) )
69 26 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) ) )
70 68 69 cnf2dd 
 |-  ( -. ( ( 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 ) ) ) ) ) )
71 29 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) )
72 70 71 cnf2dd 
 |-  ( -. ( ( 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 ) )
73 32 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) ) )
74 68 73 cnf2dd 
 |-  ( -. ( ( 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 ) ) ) )
75 72 74 mpdd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) )
77 76 a1d 
 |-  ( -. ( ( 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 ) ) ) )
78 75 77 cnfn2dd 
 |-  ( -. ( ( 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 ) ) )
79 65 78 cnfn2dd 
 |-  ( -. ( ( 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 ) ) )
80 40 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) ) )
81 70 80 cnf2dd 
 |-  ( -. ( ( 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 ) ) ) ) )
82 50 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) )
83 81 82 cnf2dd 
 |-  ( -. ( ( 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 ) ) )
84 83 53 syld 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) )
86 85 a1d 
 |-  ( -. ( ( 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 ) ) ) )
87 84 86 cnfn2dd 
 |-  ( -. ( ( 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 ) ) )
88 65 87 cnfn1dd 
 |-  ( -. ( ( 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 ) )
89 88 a1dd 
 |-  ( -. ( ( 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 
 |-  ( -. ( ( 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 ) ) ) )
91 90 a1d 
 |-  ( -. ( ( 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 ) ) ) ) )
92 91 or32dd 
 |-  ( -. ( ( 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 ) ) ) )
93 89 92 cnfn2dd 
 |-  ( -. ( ( 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 ) ) ) ) )
94 79 93 cnfn1dd 
 |-  ( -. ( ( 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 ) ) ) )
95 43 a1d 
 |-  ( -. ( ( 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 ) ) ) ) ) )
96 81 95 cnf2dd 
 |-  ( -. ( ( 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 ) ) ) )
97 94 96 contrd 
 |-  ( -. ( ( 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. )
98 97 efald2 
 |-  ( ( 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 ) ) ) ) ) )
99 3 98 ax-mp 
 |-  ( ( 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 ) ) ) ) )
100 6 99 ax-mp 
 |-  ( E. y ph -> ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) )
101 9 a1i 
 |-  ( -. E. y ph -> y e. _V )
102 id 
 |-  ( -. ( ( -. 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 
 |-  ( -. ( ( -. 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. ) ) ) )
104 103 ord 
 |-  ( -. ( ( -. 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. ) ) ) )
105 104 a1dd 
 |-  ( -. ( ( -. 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. ) ) ) ) )
106 105 a1dd 
 |-  ( -. ( ( -. 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. ) ) ) ) ) )
107 102 106 mt3d 
 |-  ( -. ( ( -. 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 )
108 107 a1d 
 |-  ( -. ( ( -. 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 
 |-  ( -. ( ( -. 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 ) )
110 108 109 syld 
 |-  ( -. ( ( -. 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 
 |-  ( -. ( ( -. 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. ) ) ) ) )
112 111 ord 
 |-  ( -. ( ( -. 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. ) ) ) ) )
113 112 a1dd 
 |-  ( -. ( ( -. 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. ) ) ) ) ) )
114 102 113 mt3d 
 |-  ( -. ( ( -. 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 ) ) )
115 108 114 syld 
 |-  ( -. ( ( -. 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 
 |-  ( -. ( -. ( 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 ) )
117 116 notornotel2 
 |-  ( -. ( -. ( y e. if ( E. y ph , { y | ph } , _V ) <-> y e. _V ) \/ -. y e. _V ) -> y e. _V )
118 117 a1i 
 |-  ( -. ( ( -. 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 ) )
119 116 notornotel1 
 |-  ( -. ( -. ( 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 ) )
120 119 a1i 
 |-  ( -. ( ( -. 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 
 |-  ( -. ( ( -. 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 ) ) )
122 121 a1d 
 |-  ( -. ( ( -. 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 ) ) ) )
123 120 122 cnfn2dd 
 |-  ( -. ( ( -. 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 ) ) )
124 118 123 cnfn2dd 
 |-  ( -. ( ( -. 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 trud 
 |-  ( -. ( ( -. 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. )
126 125 a1d 
 |-  ( -. ( ( -. 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 
 |-  ( -. ( ( -. 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. ) ) )
128 127 a1d 
 |-  ( -. ( ( -. 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. ) ) ) )
129 128 or32dd 
 |-  ( -. ( ( -. 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. ) ) )
130 126 129 cnfn2dd 
 |-  ( -. ( ( -. 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. ) ) ) )
131 124 130 cnfn1dd 
 |-  ( -. ( ( -. 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. ) ) )
132 131 a1dd 
 |-  ( -. ( ( -. 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. ) ) ) )
133 132 a1dd 
 |-  ( -. ( ( -. 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 
 |-  ( -. ( ( -. 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 
 |-  ( -. ( ( -. 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. ) ) ) ) ) )
136 135 a1d 
 |-  ( -. ( ( -. 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. ) ) ) ) ) ) )
137 134 136 cnf2dd 
 |-  ( -. ( ( -. 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. ) ) ) ) )
138 133 137 contrd 
 |-  ( -. ( ( -. 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 ) )
139 138 a1d 
 |-  ( -. ( ( -. 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 ) ) )
140 115 139 cnfn1dd 
 |-  ( -. ( ( -. 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 ) )
141 110 140 contrd 
 |-  ( -. ( ( -. 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. )
142 141 efald2 
 |-  ( ( -. 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. ) ) ) )
143 101 142 ax-mp 
 |-  ( ( -. 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. ) ) )
144 13 143 ax-mp 
 |-  ( -. E. y ph -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> T. ) )
145 ax-1 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> -. ( ( -. 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 ph -> ps ) ) ) ) ) ) )
146 tsim3 
 |-  ( -. ( ( -. 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 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 ) <-> T. ) ) -> ( -. E. y ph -> ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) ) ) ) )
147 146 a1d 
 |-  ( -. ( ( -. 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 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 ) <-> T. ) ) -> ( -. E. y ph -> ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) ) ) ) ) )
148 145 147 cnf2dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> -. ( -. E. y ph -> ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) ) ) )
149 tsim2 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. E. y ph \/ ( -. E. y ph -> ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) ) ) )
150 149 a1d 
 |-  ( -. ( ( -. 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 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 ) ) ) ) ) ) )
151 148 150 cnf2dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> -. E. y ph ) )
152 tsim2 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( ( -. 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 ) <-> T. ) ) -> ( -. E. y ph -> ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) ) ) ) )
153 152 a1d 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> ( ( -. 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 ) <-> T. ) ) -> ( -. E. y ph -> ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) ) ) ) ) )
154 145 153 cnf2dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> ( -. E. y ph -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> T. ) ) ) )
155 151 154 mpdd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> T. ) ) )
156 id 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> -. ( ( -. 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 ph -> ps ) ) ) ) ) )
157 id 
 |-  ( -. ( E. y ph -> ps ) -> -. ( E. y ph -> ps ) )
158 157 a1i 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. ( E. y ph -> ps ) -> -. ( E. y ph -> ps ) ) )
159 tsim2 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( E. y ph \/ ( E. y ph -> ps ) ) )
160 159 a1d 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. ( E. y ph -> ps ) -> ( E. y ph \/ ( E. y ph -> ps ) ) ) )
161 158 160 cnf2dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. ( E. y ph -> ps ) -> E. y ph ) )
162 149 a1d 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. ( 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 ) ) ) ) ) ) )
163 161 162 cnfn1dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. ( E. y ph -> ps ) -> ( -. E. y ph -> ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) ) ) )
164 163 a1dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. ( E. y ph -> ps ) -> ( ( -. 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 ph -> ps ) ) ) ) ) ) )
165 156 164 mt3d 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( E. y ph -> ps ) )
166 165 a1d 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> ( E. y ph -> ps ) ) )
167 tsim3 
 |-  ( -. ( ( -. 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 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 ) ) ) ) ) )
168 167 a1d 
 |-  ( -. ( ( -. 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 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 ) ) ) ) ) ) )
169 148 168 cnf2dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> -. ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) ) )
170 tsim3 
 |-  ( -. ( ( -. 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 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 ) ) ) ) )
171 170 a1d 
 |-  ( -. ( ( -. 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 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 ) ) ) ) ) )
172 169 171 cnf2dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> -. ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) )
173 tsbi1 
 |-  ( -. ( ( -. 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 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 ) ) ) )
174 173 a1d 
 |-  ( -. ( ( -. 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 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 ) ) ) ) )
175 172 174 cnf2dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> ( -. y e. if ( E. y ph , { y | ph } , _V ) \/ -. ( E. y ph -> ps ) ) ) )
176 166 175 cnfn2dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> -. y e. if ( E. y ph , { y | ph } , _V ) ) )
177 trud 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> T. )
178 177 a1d 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> T. ) )
179 tsbi3 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( ( y e. if ( E. y ph , { y | ph } , _V ) \/ -. T. ) \/ -. ( y e. if ( E. y ph , { y | ph } , _V ) <-> T. ) ) )
180 179 a1d 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> ( ( y e. if ( E. y ph , { y | ph } , _V ) \/ -. T. ) \/ -. ( y e. if ( E. y ph , { y | ph } , _V ) <-> T. ) ) ) )
181 180 or32dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> ( ( y e. if ( E. y ph , { y | ph } , _V ) \/ -. ( y e. if ( E. y ph , { y | ph } , _V ) <-> T. ) ) \/ -. T. ) ) )
182 178 181 cnfn2dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> ( y e. if ( E. y ph , { y | ph } , _V ) \/ -. ( y e. if ( E. y ph , { y | ph } , _V ) <-> T. ) ) ) )
183 176 182 cnf1dd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> ( -. F. -> -. ( y e. if ( E. y ph , { y | ph } , _V ) <-> T. ) ) )
184 155 183 contrd 
 |-  ( -. ( ( -. 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 ph -> ps ) ) ) ) ) -> F. )
185 184 efald2 
 |-  ( ( -. 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 ph -> ps ) ) ) ) )
186 144 185 ax-mp 
 |-  ( -. E. y ph -> ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) ) )
187 100 186 pm2.61i 
 |-  ( y = ( f ` x ) -> ( y e. if ( E. y ph , { y | ph } , _V ) <-> ( E. y ph -> ps ) ) )
188 19 2 187 ac6s3f 
 |-  ( A. x e. A E. y y e. if ( E. y ph , { y | ph } , _V ) -> E. f A. x e. A ( E. y ph -> ps ) )
189 17 188 ax-mp 
 |-  E. f A. x e. A ( E. y ph -> ps )