Step | Hyp | Ref
| Expression |
1 | | ctiunct.som |
. . 3

  |
2 | | ctiunct.sdc |
. . 3
  DECID   |
3 | | ctiunct.f |
. . 3
       |
4 | | ctiunct.tom |
. . 3
 
   |
5 | | ctiunct.tdc |
. . 3
 
  DECID   |
6 | | ctiunct.g |
. . 3
 
       |
7 | | ctiunct.j |
. . 3
         |
8 | | ctiunct.u |
. . 3
                                ![]_ ]_](_urbrack.gif)    |
9 | | ctiunct.h |
. . 3
                ![]_ ]_](_urbrack.gif)              |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | ctiunctlemf 12439 |
. 2
     
  |
11 | | nfv 1528 |
. . . . 5
   |
12 | | nfiu1 3917 |
. . . . . 6
  
 |
13 | 12 | nfcri 2313 |
. . . . 5

  |
14 | 11, 13 | nfan 1565 |
. . . 4
  
   |
15 | | ctiunct.nfu |
. . . . 5
   |
16 | | ctiunct.nfh |
. . . . . . 7
   |
17 | | nfcv 2319 |
. . . . . . 7
   |
18 | 16, 17 | nffv 5526 |
. . . . . 6
       |
19 | 18 | nfeq2 2331 |
. . . . 5

     |
20 | 15, 19 | nfrexxy 2516 |
. . . 4
  
     |
21 | | simplll 533 |
. . . . . . 7
   
 


  |
22 | | simplr 528 |
. . . . . . 7
   
 


  |
23 | 21, 22, 6 | syl2anc 411 |
. . . . . 6
   
 


      |
24 | | foelrn 5754 |
. . . . . 6
     


      |
25 | 23, 24 | sylancom 420 |
. . . . 5
   
 



      |
26 | 3 | ad4antr 494 |
. . . . . . 7
     


 
            |
27 | | simpllr 534 |
. . . . . . 7
     


 
        |
28 | | foelrn 5754 |
. . . . . . 7
     


      |
29 | 26, 27, 28 | syl2anc 411 |
. . . . . 6
     


 
      
      |
30 | | f1ocnv 5475 |
. . . . . . . . . . . 12
                |
31 | 7, 30 | syl 14 |
. . . . . . . . . . 11
          |
32 | | f1of 5462 |
. . . . . . . . . . 11
       
         |
33 | 31, 32 | syl 14 |
. . . . . . . . . 10
          |
34 | 33 | ad5antr 496 |
. . . . . . . . 9
     
 
  
                      |
35 | 1 | ad5antr 496 |
. . . . . . . . . . 11
     
 
  
               |
36 | | simprl 529 |
. . . . . . . . . . 11
     
 
  
               |
37 | 35, 36 | sseldd 3157 |
. . . . . . . . . 10
     
 
  
               |
38 | | simp-5l 543 |
. . . . . . . . . . . 12
     
 
  
               |
39 | 27 | adantr 276 |
. . . . . . . . . . . 12
     
 
  
            
  |
40 | 38, 39, 4 | syl2anc 411 |
. . . . . . . . . . 11
     
 
  
               |
41 | | simplrl 535 |
. . . . . . . . . . 11
     
 
  
            
  |
42 | 40, 41 | sseldd 3157 |
. . . . . . . . . 10
     
 
  
            
  |
43 | 37, 42 | opelxpd 4660 |
. . . . . . . . 9
     
 
  
                    |
44 | 34, 43 | ffvelcdmd 5653 |
. . . . . . . 8
     
 
  
                       |
45 | 38, 7 | syl 14 |
. . . . . . . . . . . . 13
     
 
  
                     |
46 | | f1ocnvfv2 5779 |
. . . . . . . . . . . . 13
                               |
47 | 45, 43, 46 | syl2anc 411 |
. . . . . . . . . . . 12
     
 
  
                              |
48 | 47 | fveq2d 5520 |
. . . . . . . . . . 11
     
 
  
                                      |
49 | | vex 2741 |
. . . . . . . . . . . 12
 |
50 | | vex 2741 |
. . . . . . . . . . . 12
 |
51 | 49, 50 | op1st 6147 |
. . . . . . . . . . 11
        |
52 | 48, 51 | eqtrdi 2226 |
. . . . . . . . . 10
     
 
  
                               |
53 | 52, 36 | eqeltrd 2254 |
. . . . . . . . 9
     
 
  
                               |
54 | 47 | fveq2d 5520 |
. . . . . . . . . . 11
     
 
  
                                      |
55 | 49, 50 | op2nd 6148 |
. . . . . . . . . . 11
        |
56 | 54, 55 | eqtrdi 2226 |
. . . . . . . . . 10
     
 
  
                               |
57 | 52 | fveq2d 5520 |
. . . . . . . . . . . . 13
     
 
  
                                       |
58 | | simprr 531 |
. . . . . . . . . . . . 13
     
 
  
            
      |
59 | 57, 58 | eqtr4d 2213 |
. . . . . . . . . . . 12
     
 
  
                                   |
60 | 59 | csbeq1d 3065 |
. . . . . . . . . . 11
     
 
  
                                   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
61 | | csbid 3066 |
. . . . . . . . . . 11
  ![]_ ]_](_urbrack.gif)  |
62 | 60, 61 | eqtrdi 2226 |
. . . . . . . . . 10
     
 
  
                                   ![]_ ]_](_urbrack.gif)
  |
63 | 41, 56, 62 | 3eltr4d 2261 |
. . . . . . . . 9
     
 
  
                                                   ![]_ ]_](_urbrack.gif)   |
64 | 53, 63 | jca 306 |
. . . . . . . 8
     
 
  
                                                                    ![]_ ]_](_urbrack.gif)    |
65 | | 2fveq3 5521 |
. . . . . . . . . . 11
        
                          |
66 | 65 | eleq1d 2246 |
. . . . . . . . . 10
        
                            |
67 | | 2fveq3 5521 |
. . . . . . . . . . 11
        
                          |
68 | 65 | fveq2d 5520 |
. . . . . . . . . . . 12
        
                                  |
69 | 68 | csbeq1d 3065 |
. . . . . . . . . . 11
        
              ![]_ ]_](_urbrack.gif)
                      ![]_ ]_](_urbrack.gif)   |
70 | 67, 69 | eleq12d 2248 |
. . . . . . . . . 10
        
                       ![]_ ]_](_urbrack.gif)                                       ![]_ ]_](_urbrack.gif)    |
71 | 66, 70 | anbi12d 473 |
. . . . . . . . 9
        
                                ![]_ ]_](_urbrack.gif) 
                                                       ![]_ ]_](_urbrack.gif)     |
72 | 71, 8 | elrab2 2897 |
. . . . . . . 8
                                                                         ![]_ ]_](_urbrack.gif)     |
73 | 44, 64, 72 | sylanbrc 417 |
. . . . . . 7
     
 
  
                       |
74 | 59 | csbeq1d 3065 |
. . . . . . . . . 10
     
 
  
                                   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
75 | | csbid 3066 |
. . . . . . . . . 10
  ![]_ ]_](_urbrack.gif)  |
76 | 74, 75 | eqtrdi 2226 |
. . . . . . . . 9
     
 
  
                                   ![]_ ]_](_urbrack.gif)
  |
77 | 76, 56 | fveq12d 5523 |
. . . . . . . 8
     
 
  
                                    ![]_ ]_](_urbrack.gif)                          |
78 | | 2fveq3 5521 |
. . . . . . . . . . . 12
        
                          |
79 | 78 | fveq2d 5520 |
. . . . . . . . . . 11
        
                                  |
80 | 79 | csbeq1d 3065 |
. . . . . . . . . 10
        
              ![]_ ]_](_urbrack.gif)
                      ![]_ ]_](_urbrack.gif)   |
81 | | 2fveq3 5521 |
. . . . . . . . . 10
        
                          |
82 | 80, 81 | fveq12d 5523 |
. . . . . . . . 9
        
               ![]_ ]_](_urbrack.gif)                                   ![]_ ]_](_urbrack.gif)                      |
83 | | simplrr 536 |
. . . . . . . . . . 11
     
 
  
            
      |
84 | 83, 77 | eqtr4d 2213 |
. . . . . . . . . 10
     
 
  
            
                       ![]_ ]_](_urbrack.gif)                      |
85 | | simpllr 534 |
. . . . . . . . . 10
     
 
  
            
  |
86 | 84, 85 | eqeltrrd 2255 |
. . . . . . . . 9
     
 
  
                                    ![]_ ]_](_urbrack.gif)                      |
87 | 9, 82, 73, 86 | fvmptd3 5610 |
. . . . . . . 8
     
 
  
                                                ![]_ ]_](_urbrack.gif)                      |
88 | 77, 87, 83 | 3eqtr4rd 2221 |
. . . . . . 7
     
 
  
            
              |
89 | | fveq2 5516 |
. . . . . . . 8
        
                  |
90 | 89 | rspceeqv 2860 |
. . . . . . 7
                       
      |
91 | 73, 88, 90 | syl2anc 411 |
. . . . . 6
     
 
  
             
      |
92 | 29, 91 | rexlimddv 2599 |
. . . . 5
     


 
      
      |
93 | 25, 92 | rexlimddv 2599 |
. . . 4
   
 



      |
94 | | eliun 3891 |
. . . . . 6
 

  |
95 | 94 | biimpi 120 |
. . . . 5
  
  |
96 | 95 | adantl 277 |
. . . 4
 
 

  |
97 | 14, 20, 93, 96 | r19.29af2 2617 |
. . 3
 
 

      |
98 | 97 | ralrimiva 2550 |
. 2
 
 
      |
99 | | dffo3 5664 |
. 2
     
        
       |
100 | 10, 98, 99 | sylanbrc 417 |
1
     
  |