Step | Hyp | Ref
| Expression |
1 | | ctinfom 12428 |
. . . 4

 

DECID
        
            |
2 | 1 | simplbi 274 |
. . 3



DECID
  |
3 | 1 | simprbi 275 |
. . . 4

                    |
4 | | simpl 109 |
. . . . . 6
                       |
5 | 4 | a1i 9 |
. . . . 5

                        |
6 | 5 | eximdv 1880 |
. . . 4

       
 
        
        |
7 | 3, 6 | mpd 13 |
. . 3

       |
8 | | nnenom 10433 |
. . . . . 6
 |
9 | | entr 6783 |
. . . . . 6
     |
10 | 8, 9 | mpan2 425 |
. . . . 5

  |
11 | 10 | ensymd 6782 |
. . . 4

  |
12 | | endom 6762 |
. . . 4
   |
13 | 11, 12 | syl 14 |
. . 3

  |
14 | 2, 7, 13 | 3jca 1177 |
. 2

 

DECID
        |
15 | | simp1 997 |
. . 3
   
DECID
      

DECID   |
16 | | 3simpb 995 |
. . . 4
   
DECID
         DECID    |
17 | | simp2 998 |
. . . 4
   
DECID
      
      |
18 | | simp2 998 |
. . . . . . . 8
   
DECID
   
       |
19 | | simpl1 1000 |
. . . . . . . . . . . 12
     DECID       

DECID
  |
20 | | equequ1 1712 |
. . . . . . . . . . . . . . 15
 
   |
21 | 20 | dcbid 838 |
. . . . . . . . . . . . . 14
 DECID
DECID
   |
22 | 21 | ralbidv 2477 |
. . . . . . . . . . . . 13
  
DECID
 DECID    |
23 | 22 | cbvralv 2703 |
. . . . . . . . . . . 12
 

DECID
 
DECID   |
24 | 19, 23 | sylib 122 |
. . . . . . . . . . 11
     DECID       

DECID
  |
25 | | simpl3 1002 |
. . . . . . . . . . 11
     DECID         |
26 | | fof 5438 |
. . . . . . . . . . . . . 14
           |
27 | | imassrn 4981 |
. . . . . . . . . . . . . . 15
     |
28 | | frn 5374 |
. . . . . . . . . . . . . . 15
    
  |
29 | 27, 28 | sstrid 3166 |
. . . . . . . . . . . . . 14
        
  |
30 | 26, 29 | syl 14 |
. . . . . . . . . . . . 13
        
  |
31 | 30 | ad2antrr 488 |
. . . . . . . . . . . 12
               |
32 | 31 | 3adantl1 1153 |
. . . . . . . . . . 11
     DECID             |
33 | | simpl2 1001 |
. . . . . . . . . . . . 13
     DECID             |
34 | | equequ1 1712 |
. . . . . . . . . . . . . . . 16
 
   |
35 | 34 | dcbid 838 |
. . . . . . . . . . . . . . 15
 DECID
DECID
   |
36 | | equequ2 1713 |
. . . . . . . . . . . . . . . 16
 
   |
37 | 36 | dcbid 838 |
. . . . . . . . . . . . . . 15
 DECID
DECID
   |
38 | 35, 37 | cbvral2v 2716 |
. . . . . . . . . . . . . 14
 

DECID
 
DECID   |
39 | | ssralv 3219 |
. . . . . . . . . . . . . . . . 17
      
DECID
     DECID    |
40 | 30, 39 | syl 14 |
. . . . . . . . . . . . . . . 16
       DECID 
    DECID    |
41 | 40 | ralimdv 2545 |
. . . . . . . . . . . . . . 15
        DECID 

    DECID    |
42 | | ssralv 3219 |
. . . . . . . . . . . . . . 15
      

    DECID            DECID    |
43 | 30, 41, 42 | sylsyld 58 |
. . . . . . . . . . . . . 14
        DECID 
          DECID    |
44 | 38, 43 | biimtrid 152 |
. . . . . . . . . . . . 13
        DECID 
          DECID    |
45 | 33, 19, 44 | sylc 62 |
. . . . . . . . . . . 12
     DECID                  DECID   |
46 | | simpr 110 |
. . . . . . . . . . . . . 14
           |
47 | | fofun 5439 |
. . . . . . . . . . . . . . . . 17
       |
48 | 47 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
        
  |
49 | | ordom 4606 |
. . . . . . . . . . . . . . . . . . 19
 |
50 | | ordtr 4378 |
. . . . . . . . . . . . . . . . . . 19

  |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
 |
52 | | trss 4110 |
. . . . . . . . . . . . . . . . . 18
     |
53 | 51, 46, 52 | mpsyl 65 |
. . . . . . . . . . . . . . . . 17
           |
54 | 26 | fdmd 5372 |
. . . . . . . . . . . . . . . . . 18
    
  |
55 | 54 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
        
  |
56 | 53, 55 | sseqtrrd 3194 |
. . . . . . . . . . . . . . . 16
           |
57 | | fores 5447 |
. . . . . . . . . . . . . . . 16
               |
58 | 48, 56, 57 | syl2anc 411 |
. . . . . . . . . . . . . . 15
                     |
59 | | vex 2740 |
. . . . . . . . . . . . . . . . 17
 |
60 | 59 | resex 4948 |
. . . . . . . . . . . . . . . 16
   |
61 | | foeq1 5434 |
. . . . . . . . . . . . . . . 16
                         |
62 | 60, 61 | spcev 2832 |
. . . . . . . . . . . . . . 15
 
         
          |
63 | 58, 62 | syl 14 |
. . . . . . . . . . . . . 14
                    |
64 | | foeq2 5435 |
. . . . . . . . . . . . . . . 16
                     |
65 | 64 | exbidv 1825 |
. . . . . . . . . . . . . . 15
  
       
            |
66 | 65 | rspcev 2841 |
. . . . . . . . . . . . . 14
                        |
67 | 46, 63, 66 | syl2anc 411 |
. . . . . . . . . . . . 13
                     |
68 | 67 | 3adantl1 1153 |
. . . . . . . . . . . 12
     DECID                   |
69 | | fidcenum 6954 |
. . . . . . . . . . . 12
    
 
     
    DECID              |
70 | 45, 68, 69 | sylanbrc 417 |
. . . . . . . . . . 11
     DECID             |
71 | 24, 25, 32, 70 | inffinp1 12429 |
. . . . . . . . . 10
     DECID       
      |
72 | | simprl 529 |
. . . . . . . . . . . 12
    

DECID
    
          |
73 | | foelrn 5753 |
. . . . . . . . . . . 12
     

       |
74 | 33, 72, 73 | syl2an2r 595 |
. . . . . . . . . . 11
    

DECID
    
               |
75 | | simpr 110 |
. . . . . . . . . . . . . 14
       
DECID
   
        

    
      |
76 | | simprr 531 |
. . . . . . . . . . . . . . 15
    

DECID
    
       
      |
77 | 76 | ad2antrr 488 |
. . . . . . . . . . . . . 14
       
DECID
   
        

    
      |
78 | 75, 77 | eqneltrrd 2274 |
. . . . . . . . . . . . 13
       
DECID
   
        

    
          |
79 | 78 | ex 115 |
. . . . . . . . . . . 12
     

DECID
            
     
           |
80 | 79 | reximdva 2579 |
. . . . . . . . . . 11
    

DECID
    
         
                |
81 | 74, 80 | mpd 13 |
. . . . . . . . . 10
    

DECID
    
                   |
82 | 71, 81 | rexlimddv 2599 |
. . . . . . . . 9
     DECID                  |
83 | 82 | ralrimiva 2550 |
. . . . . . . 8
   
DECID
   
             |
84 | 18, 83 | jca 306 |
. . . . . . 7
   
DECID
   
     
 
           |
85 | 84 | 3com23 1209 |
. . . . . 6
   
DECID
         
 
           |
86 | 85 | 3expia 1205 |
. . . . 5
   
DECID
     
      
            |
87 | 86 | eximdv 1880 |
. . . 4
   
DECID
               
            |
88 | 16, 17, 87 | sylc 62 |
. . 3
   
DECID
            
 
           |
89 | 15, 88, 1 | sylanbrc 417 |
. 2
   
DECID
        |
90 | 14, 89 | impbii 126 |
1

 

DECID
    
   |