Step | Hyp | Ref
| Expression |
1 | | kelac1.c |
. . . . . . 7
 
       |
2 | | eqid 2462 |
. . . . . . . 8
   |
3 | 2 | cldss 20099 |
. . . . . . 7
    
   |
4 | 1, 3 | syl 17 |
. . . . . 6
 
    |
5 | 4 | ralrimiva 2814 |
. . . . 5
     |
6 | | boxriin 7595 |
. . . . 5
 
 
  

          |
7 | 5, 6 | syl 17 |
. . . 4
 
 
            |
8 | | kelac1.k |
. . . . . . . . 9
         |
9 | | cmptop 20465 |
. . . . . . . . 9
    
     
    |
10 | | 0ntop 19990 |
. . . . . . . . . . 11
 |
11 | | fvprc 5886 |
. . . . . . . . . . . 12
           |
12 | 11 | eleq1d 2524 |
. . . . . . . . . . 11
             |
13 | 10, 12 | mtbiri 309 |
. . . . . . . . . 10
           |
14 | 13 | con4i 135 |
. . . . . . . . 9
    
      |
15 | 8, 9, 14 | 3syl 18 |
. . . . . . . 8
     |
16 | | kelac1.j |
. . . . . . . . 9
 
   |
17 | | eqid 2462 |
. . . . . . . . 9
     |
18 | 16, 17 | fmptd 6074 |
. . . . . . . 8
         |
19 | | dmfex 6783 |
. . . . . . . 8
             |
20 | 15, 18, 19 | syl2anc 671 |
. . . . . . 7
   |
21 | 16 | ralrimiva 2814 |
. . . . . . 7
 
  |
22 | | eqid 2462 |
. . . . . . . 8
             |
23 | 22 | ptunimpt 20665 |
. . . . . . 7
     
         |
24 | 20, 21, 23 | syl2anc 671 |
. . . . . 6
  
         |
25 | 24 | ineq1d 3645 |
. . . . 5
     
 
             

         |
26 | | eqid 2462 |
. . . . . 6
               |
27 | 2 | topcld 20105 |
. . . . . . . . . 10
        |
28 | 16, 27 | syl 17 |
. . . . . . . . 9
 
        |
29 | 1, 28 | ifcld 3936 |
. . . . . . . 8
 
  
          |
30 | 20, 16, 29 | ptcldmpt 20684 |
. . . . . . 7
                    |
31 | 30 | adantr 471 |
. . . . . 6
 
 
                  |
32 | | simprr 771 |
. . . . . . . 8
 
     |
33 | | kelac1.b |
. . . . . . . . . . . . . . 15
 
       |
34 | | f1ofo 5848 |
. . . . . . . . . . . . . . 15
    
      |
35 | | foima 5825 |
. . . . . . . . . . . . . . 15
           |
36 | 33, 34, 35 | 3syl 18 |
. . . . . . . . . . . . . 14
 
       |
37 | 36 | eqcomd 2468 |
. . . . . . . . . . . . 13
 
       |
38 | | kelac1.z |
. . . . . . . . . . . . . 14
 
   |
39 | | f1ofn 5842 |
. . . . . . . . . . . . . . . . 17
    
  |
40 | 33, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
 
   |
41 | | ssid 3463 |
. . . . . . . . . . . . . . . 16
 |
42 | | fnimaeq0 5723 |
. . . . . . . . . . . . . . . 16
           |
43 | 40, 41, 42 | sylancl 673 |
. . . . . . . . . . . . . . 15
 
     
   |
44 | 43 | necon3bid 2680 |
. . . . . . . . . . . . . 14
 
     
   |
45 | 38, 44 | mpbird 240 |
. . . . . . . . . . . . 13
 
       |
46 | 37, 45 | eqnetrd 2703 |
. . . . . . . . . . . 12
 
   |
47 | | n0 3753 |
. . . . . . . . . . . 12
    |
48 | 46, 47 | sylib 201 |
. . . . . . . . . . 11
 
 
  |
49 | | rexv 3074 |
. . . . . . . . . . 11
 
   |
50 | 48, 49 | sylibr 217 |
. . . . . . . . . 10
 
    |
51 | 50 | ralrimiva 2814 |
. . . . . . . . 9
  
  |
52 | | ssralv 3505 |
. . . . . . . . . 10
  

 
   |
53 | 52 | adantr 471 |
. . . . . . . . 9
 
     
   |
54 | 51, 53 | mpan9 476 |
. . . . . . . 8
 
   

  |
55 | | eleq1 2528 |
. . . . . . . . 9
     
       |
56 | 55 | ac6sfi 7846 |
. . . . . . . 8
   
        
       |
57 | 32, 54, 56 | syl2anc 671 |
. . . . . . 7
 
         

       |
58 | 24 | eqcomd 2468 |
. . . . . . . . . . 11
        
   |
59 | 58 | ineq1d 3645 |
. . . . . . . . . 10
          
 
       

          |
60 | 59 | ad2antrr 737 |
. . . . . . . . 9
   
 

    
        
         
  
 
       |
61 | | iftrue 3899 |
. . . . . . . . . . . . . . . . . . 19
  
             |
62 | 61 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . 18
   
 

                     |
63 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
   |
64 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
  |
65 | 64 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
   |
66 | 63, 65, 4 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . 20
   
 
    |
67 | 66 | sseld 3443 |
. . . . . . . . . . . . . . . . . . 19
   
 
              |
68 | 67 | impr 629 |
. . . . . . . . . . . . . . . . . 18
   
 

             |
69 | 62, 68 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . 17
   
 

                  |
70 | 69 | expr 624 |
. . . . . . . . . . . . . . . 16
   
 
                   |
71 | 70 | ralimdva 2808 |
. . . . . . . . . . . . . . 15
 
                       |
72 | 71 | imp 435 |
. . . . . . . . . . . . . 14
   
 

    

            |
73 | | eldifn 3568 |
. . . . . . . . . . . . . . . . . . 19
  
  |
74 | 73 | iffalsed 3904 |
. . . . . . . . . . . . . . . . . 18
    
         |
75 | 74 | adantl 472 |
. . . . . . . . . . . . . . . . 17
 

   
         |
76 | | eldifi 3567 |
. . . . . . . . . . . . . . . . . 18
     |
77 | | kelac1.u |
. . . . . . . . . . . . . . . . . 18
 
    |
78 | 76, 77 | sylan2 481 |
. . . . . . . . . . . . . . . . 17
 

     |
79 | 75, 78 | eqeltrd 2540 |
. . . . . . . . . . . . . . . 16
 

   
          |
80 | 79 | ralrimiva 2814 |
. . . . . . . . . . . . . . 15
                 |
81 | 80 | ad2antrr 737 |
. . . . . . . . . . . . . 14
   
 

    
                |
82 | | ralun 3628 |
. . . . . . . . . . . . . 14
                            
                 |
83 | 72, 81, 82 | syl2anc 671 |
. . . . . . . . . . . . 13
   
 

    
  
               |
84 | | undif 3860 |
. . . . . . . . . . . . . . . . 17

      |
85 | 84 | biimpi 199 |
. . . . . . . . . . . . . . . 16
       |
86 | 85 | ad2antrl 739 |
. . . . . . . . . . . . . . 15
 
    
    |
87 | 86 | raleqdv 3005 |
. . . . . . . . . . . . . 14
 
      
            

             |
88 | 87 | adantr 471 |
. . . . . . . . . . . . 13
   
 

    
 
              

             |
89 | 83, 88 | mpbid 215 |
. . . . . . . . . . . 12
   
 

    

            |
90 | 20 | ad2antrr 737 |
. . . . . . . . . . . . 13
   
 

    
  |
91 | | mptelixpg 7590 |
. . . . . . . . . . . . 13
             

              |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . 12
   
 

    
            
               |
93 | 89, 92 | mpbird 240 |
. . . . . . . . . . 11
   
 

    

          
   |
94 | | eleq2 2529 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
95 | | eleq2 2529 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     
     
     
       |
96 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                |
97 | 68 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                 |
98 | 94, 95, 96, 97 | ifbothda 3928 |
. . . . . . . . . . . . . . . . . . . . 21
   
 

                  |
99 | 62, 98 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . . 20
   
 

                       |
100 | 99 | expr 624 |
. . . . . . . . . . . . . . . . . . 19
   
 
                        |
101 | 100 | ralimdva 2808 |
. . . . . . . . . . . . . . . . . 18
 
                    
       |
102 | 101 | imp 435 |
. . . . . . . . . . . . . . . . 17
   
 

    

                 |
103 | 102 | adantr 471 |
. . . . . . . . . . . . . . . 16
    
  
      
                 |
104 | 78 | adantlr 726 |
. . . . . . . . . . . . . . . . . . . 20
          |
105 | 74 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
        
         |
106 | | incom 3637 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
   |
107 | | disjdif 3851 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
108 | 106, 107 | eqtri 2484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
   |
110 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
111 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
112 | | disjne 3822 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
   |
113 | 109, 110,
111, 112 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
114 | 113 | neneqd 2640 |
. . . . . . . . . . . . . . . . . . . . 21
      
  |
115 | 114 | iffalsed 3904 |
. . . . . . . . . . . . . . . . . . . 20
        
       |
116 | 104, 105,
115 | 3eltr4d 2555 |
. . . . . . . . . . . . . . . . . . 19
        
               |
117 | 116 | ralrimiva 2814 |
. . . . . . . . . . . . . . . . . 18
 
                      |
118 | 117 | adantlr 726 |
. . . . . . . . . . . . . . . . 17
   
 
                      |
119 | 118 | adantlr 726 |
. . . . . . . . . . . . . . . 16
    
  
                           |
120 | | ralun 3628 |
. . . . . . . . . . . . . . . 16
             
   
                    
               
      |
121 | 103, 119,
120 | syl2anc 671 |
. . . . . . . . . . . . . . 15
    
  
        
                    |
122 | 86 | raleqdv 3005 |
. . . . . . . . . . . . . . . 16
 
      
                 

                  |
123 | 122 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
    
  
       
               
                       |
124 | 121, 123 | mpbid 215 |
. . . . . . . . . . . . . 14
    
  
      
                 |
125 | 20 | ad3antrrr 741 |
. . . . . . . . . . . . . . 15
    
  
        |
126 | | mptelixpg 7590 |
. . . . . . . . . . . . . . 15
             
     

                  |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . 14
    
  
                  
     

                  |
128 | 124, 127 | mpbird 240 |
. . . . . . . . . . . . 13
    
  
                 
 
      |
129 | 128 | ralrimiva 2814 |
. . . . . . . . . . . 12
   
 

    


          
        |
130 | | mptexg 6165 |
. . . . . . . . . . . . . . 15
              |
131 | 20, 130 | syl 17 |
. . . . . . . . . . . . . 14
              |
132 | 131 | ad2antrr 737 |
. . . . . . . . . . . . 13
   
 

    

            |
133 | | eliin 4298 |
. . . . . . . . . . . . 13
                               


          
         |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . 12
   
 

    
            

                  
         |
135 | 129, 134 | mpbird 240 |
. . . . . . . . . . 11
   
 

    

          
         |
136 | 93, 135 | elind 3630 |
. . . . . . . . . 10
   
 

    

           
            |
137 | | ne0i 3749 |
. . . . . . . . . 10
              

         
  
 
       |
138 | 136, 137 | syl 17 |
. . . . . . . . 9
   
 

    
 
            |
139 | 60, 138 | eqnetrd 2703 |
. . . . . . . 8
   
 

    
        
          |
140 | 139 | adantrl 727 |
. . . . . . 7
   
 
                               |
141 | 57, 140 | exlimddv 1792 |
. . . . . 6
 
            
 
       |
142 | 26, 8, 31, 141 | cmpfiiin 35585 |
. . . . 5
          
 
       |
143 | 25, 142 | eqnetrd 2703 |
. . . 4
     
 
       |
144 | 7, 143 | eqnetrd 2703 |
. . 3
    |
145 | | n0 3753 |
. . 3
 
 
  |
146 | 144, 145 | sylib 201 |
. 2
  
  |
147 | | elixp2 7557 |
. . . . . 6
           |
148 | 147 | simp3bi 1031 |
. . . . 5
         |
149 | | f1ocnv 5853 |
. . . . . . . 8
    
       |
150 | | f1of 5841 |
. . . . . . . 8
             |
151 | | ffvelrn 6048 |
. . . . . . . . 9
                       |
152 | 151 | ex 440 |
. . . . . . . 8
                       |
153 | 33, 149, 150, 152 | 4syl 19 |
. . . . . . 7
 
                  |
154 | 153 | ralimdva 2808 |
. . . . . 6
                    |
155 | 154 | imp 435 |
. . . . 5
 

    

           |
156 | 148, 155 | sylan2 481 |
. . . 4
 
 

           |
157 | | mptelixpg 7590 |
. . . . . 6
             
             |
158 | 20, 157 | syl 17 |
. . . . 5
             
             |
159 | 158 | adantr 471 |
. . . 4
 
 
            

            |
160 | 156, 159 | mpbird 240 |
. . 3
 
 

          
  |
161 | | ne0i 3749 |
. . 3
            

  |
162 | 160, 161 | syl 17 |
. 2
 
 
   |
163 | 146, 162 | exlimddv 1792 |
1
    |