Step | Hyp | Ref
| Expression |
1 | | reconnlem2.9 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)      |
2 | | inss2 3653 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   |
3 | | inss2 3653 |
. . . . . . . . . . . . . . . 16
   |
4 | | reconnlem2.5 |
. . . . . . . . . . . . . . . 16
     |
5 | 3, 4 | sseldi 3430 |
. . . . . . . . . . . . . . 15
   |
6 | | inss2 3653 |
. . . . . . . . . . . . . . . 16
   |
7 | | reconnlem2.6 |
. . . . . . . . . . . . . . . 16
     |
8 | 6, 7 | sseldi 3430 |
. . . . . . . . . . . . . . 15
   |
9 | | reconnlem2.4 |
. . . . . . . . . . . . . . 15
  
  ![[,] [,]](_icc.gif) 
  |
10 | | oveq1 6297 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
11 | 10 | sseq1d 3459 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     |
12 | | oveq2 6298 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
13 | 12 | sseq1d 3459 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     |
14 | 11, 13 | rspc2va 3160 |
. . . . . . . . . . . . . . 15
  



  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
15 | 5, 8, 9, 14 | syl21anc 1267 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif) 
  |
16 | | reconnlem2.1 |
. . . . . . . . . . . . . 14

  |
17 | 15, 16 | sstrd 3442 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif) 
  |
18 | 2, 17 | syl5ss 3443 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)     |
19 | | inss1 3652 |
. . . . . . . . . . . . . . 15
   |
20 | 19, 4 | sseldi 3430 |
. . . . . . . . . . . . . 14
   |
21 | 16, 5 | sseldd 3433 |
. . . . . . . . . . . . . . . 16
   |
22 | 21 | rexrd 9690 |
. . . . . . . . . . . . . . 15
   |
23 | 16, 8 | sseldd 3433 |
. . . . . . . . . . . . . . . 16
   |
24 | 23 | rexrd 9690 |
. . . . . . . . . . . . . . 15
   |
25 | | reconnlem2.8 |
. . . . . . . . . . . . . . 15

  |
26 | | lbicc2 11748 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)    |
27 | 22, 24, 25, 26 | syl3anc 1268 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)    |
28 | 20, 27 | elind 3618 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)     |
29 | | ne0i 3737 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)     |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)     |
31 | 2 | sseli 3428 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
32 | | elicc2 11699 |
. . . . . . . . . . . . . . . . 17
 
    ![[,] [,]](_icc.gif)  
    |
33 | 21, 23, 32 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif)  
    |
34 | | simp3 1010 |
. . . . . . . . . . . . . . . 16
     |
35 | 33, 34 | syl6bi 232 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)     |
36 | 31, 35 | syl5 33 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)      |
37 | 36 | ralrimiv 2800 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)   
  |
38 | | breq2 4406 |
. . . . . . . . . . . . . . 15
 
   |
39 | 38 | ralbidv 2827 |
. . . . . . . . . . . . . 14
  
   ![[,] [,]](_icc.gif)   
    ![[,] [,]](_icc.gif)   
   |
40 | 39 | rspcev 3150 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)      |
41 | 23, 37, 40 | syl2anc 667 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)      |
42 | | suprcl 10569 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)   
      ![[,] [,]](_icc.gif)       |
43 | 18, 30, 41, 42 | syl3anc 1268 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)       |
44 | 1, 43 | syl5eqel 2533 |
. . . . . . . . . 10
   |
45 | | rphalfcl 11327 |
. . . . . . . . . 10

    |
46 | | ltaddrp 11336 |
. . . . . . . . . 10
           |
47 | 44, 45, 46 | syl2an 480 |
. . . . . . . . 9
 

      |
48 | 44 | adantr 467 |
. . . . . . . . . 10
 

  |
49 | 45 | rpred 11341 |
. . . . . . . . . . 11

    |
50 | | readdcl 9622 |
. . . . . . . . . . 11
           |
51 | 44, 49, 50 | syl2an 480 |
. . . . . . . . . 10
 

      |
52 | 48, 51 | ltnled 9782 |
. . . . . . . . 9
 

    
       |
53 | 47, 52 | mpbid 214 |
. . . . . . . 8
 


     |
54 | 18 | ad2antrr 732 |
. . . . . . . . . 10
    
            ![[,] [,]](_icc.gif)     |
55 | 30 | ad2antrr 732 |
. . . . . . . . . 10
    
            ![[,] [,]](_icc.gif)     |
56 | 41 | ad2antrr 732 |
. . . . . . . . . 10
    
              ![[,] [,]](_icc.gif)   
  |
57 | | inss1 3652 |
. . . . . . . . . . . 12
      |
58 | | simpr 463 |
. . . . . . . . . . . 12
    
         
          |
59 | 57, 58 | sseldi 3430 |
. . . . . . . . . . 11
    
         
     |
60 | 51 | adantr 467 |
. . . . . . . . . . . 12
    
         
     |
61 | 21 | ad2antrr 732 |
. . . . . . . . . . . . 13
    
           |
62 | 44 | ad2antrr 732 |
. . . . . . . . . . . . 13
    
           |
63 | | suprub 10570 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)   

   ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)       |
64 | 18, 30, 41, 28, 63 | syl31anc 1271 |
. . . . . . . . . . . . . . 15

     ![[,] [,]](_icc.gif)       |
65 | 64, 1 | syl6breqr 4443 |
. . . . . . . . . . . . . 14

  |
66 | 65 | ad2antrr 732 |
. . . . . . . . . . . . 13
    
           |
67 | 47 | adantr 467 |
. . . . . . . . . . . . . 14
    
               |
68 | 62, 60, 67 | ltled 9783 |
. . . . . . . . . . . . 13
    
               |
69 | 61, 62, 60, 66, 68 | letrd 9792 |
. . . . . . . . . . . 12
    
               |
70 | 23 | ad2antrr 732 |
. . . . . . . . . . . . 13
    
           |
71 | | inss2 3653 |
. . . . . . . . . . . . . . 15
         |
72 | 71, 58 | sseldi 3430 |
. . . . . . . . . . . . . 14
    
         
        |
73 | | eliooord 11694 |
. . . . . . . . . . . . . . 15
            
      |
74 | 73 | simprd 465 |
. . . . . . . . . . . . . 14
        
     |
75 | 72, 74 | syl 17 |
. . . . . . . . . . . . 13
    
         
     |
76 | 60, 70, 75 | ltled 9783 |
. . . . . . . . . . . 12
    
         
     |
77 | | elicc2 11699 |
. . . . . . . . . . . . 13
 
        ![[,] [,]](_icc.gif)      
    
  
    |
78 | 61, 70, 77 | syl2anc 667 |
. . . . . . . . . . . 12
    
                ![[,] [,]](_icc.gif) 
 
               |
79 | 60, 69, 76, 78 | mpbir3and 1191 |
. . . . . . . . . . 11
    
         
     ![[,] [,]](_icc.gif)    |
80 | 59, 79 | elind 3618 |
. . . . . . . . . 10
    
         
      ![[,] [,]](_icc.gif)     |
81 | | suprub 10570 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)   
        ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)       |
82 | 54, 55, 56, 80, 81 | syl31anc 1271 |
. . . . . . . . 9
    
         
        ![[,] [,]](_icc.gif)       |
83 | 82, 1 | syl6breqr 4443 |
. . . . . . . 8
    
         
     |
84 | 53, 83 | mtand 665 |
. . . . . . 7
 


          |
85 | | eqid 2451 |
. . . . . . . . . . . . 13
           |
86 | 85 | remetdval 21807 |
. . . . . . . . . . . 12
     
                          |
87 | 51, 48, 86 | syl2anc 667 |
. . . . . . . . . . 11
 

 
     
                 |
88 | 48 | recnd 9669 |
. . . . . . . . . . . . 13
 

  |
89 | 49 | adantl 468 |
. . . . . . . . . . . . . 14
 

    |
90 | 89 | recnd 9669 |
. . . . . . . . . . . . 13
 

    |
91 | 88, 90 | pncan2d 9988 |
. . . . . . . . . . . 12
 

 
        |
92 | 91 | fveq2d 5869 |
. . . . . . . . . . 11
 

                  |
93 | 45 | adantl 468 |
. . . . . . . . . . . 12
 

    |
94 | | rpre 11308 |
. . . . . . . . . . . . 13
  
    |
95 | | rpge0 11314 |
. . . . . . . . . . . . 13
  
    |
96 | 94, 95 | absidd 13484 |
. . . . . . . . . . . 12
  
          |
97 | 93, 96 | syl 17 |
. . . . . . . . . . 11
 

          |
98 | 87, 92, 97 | 3eqtrd 2489 |
. . . . . . . . . 10
 

 
     
         |
99 | | rphalflt 11329 |
. . . . . . . . . . 11

    |
100 | 99 | adantl 468 |
. . . . . . . . . 10
 

    |
101 | 98, 100 | eqbrtrd 4423 |
. . . . . . . . 9
 

 
     
       |
102 | 85 | rexmet 21809 |
. . . . . . . . . . 11
           |
103 | 102 | a1i 11 |
. . . . . . . . . 10
 

  
         |
104 | | rpxr 11309 |
. . . . . . . . . . 11

  |
105 | 104 | adantl 468 |
. . . . . . . . . 10
 

  |
106 | | elbl3 21407 |
. . . . . . . . . 10
    
         

                
     
 
     
        |
107 | 103, 105,
48, 51, 106 | syl22anc 1269 |
. . . . . . . . 9
 

 
          
                     |
108 | 101, 107 | mpbird 236 |
. . . . . . . 8
 

          
        |
109 | | ssel 3426 |
. . . . . . . 8
       
     

               
     
            |
110 | 108, 109 | syl5com 31 |
. . . . . . 7
 

       
     

    
           |
111 | 84, 110 | mtod 181 |
. . . . . 6
 

      
     

      |
112 | 111 | nrexdv 2843 |
. . . . 5
        
      
      |
113 | 44 | adantr 467 |
. . . . . . . . 9
 
   |
114 | | mnflt 11425 |
. . . . . . . . . 10
   |
115 | 113, 114 | syl 17 |
. . . . . . . . 9
 
   |
116 | | suprleub 10573 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)   

       ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)   
   |
117 | 18, 30, 41, 23, 116 | syl31anc 1271 |
. . . . . . . . . . . . . . . 16
       ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)   
   |
118 | 37, 117 | mpbird 236 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif)       |
119 | 1, 118 | syl5eqbr 4436 |
. . . . . . . . . . . . . 14

  |
120 | 44, 23 | leloed 9778 |
. . . . . . . . . . . . . 14
  
    |
121 | 119, 120 | mpbid 214 |
. . . . . . . . . . . . 13
 
   |
122 | 121 | ord 379 |
. . . . . . . . . . . 12
 
   |
123 | | elndif 3557 |
. . . . . . . . . . . . . . 15

    |
124 | 8, 123 | syl 17 |
. . . . . . . . . . . . . 14
     |
125 | | inss1 3652 |
. . . . . . . . . . . . . . . 16
   |
126 | 125, 7 | sseldi 3430 |
. . . . . . . . . . . . . . 15
   |
127 | | elin 3617 |
. . . . . . . . . . . . . . . 16
       |
128 | | reconnlem2.7 |
. . . . . . . . . . . . . . . . 17
  
    |
129 | 128 | sseld 3431 |
. . . . . . . . . . . . . . . 16
         |
130 | 127, 129 | syl5bir 222 |
. . . . . . . . . . . . . . 15
         |
131 | 126, 130 | mpan2d 680 |
. . . . . . . . . . . . . 14
       |
132 | 124, 131 | mtod 181 |
. . . . . . . . . . . . 13
   |
133 | | eleq1 2517 |
. . . . . . . . . . . . . 14
 
   |
134 | 133 | notbid 296 |
. . . . . . . . . . . . 13
 
   |
135 | 132, 134 | syl5ibrcom 226 |
. . . . . . . . . . . 12
 
   |
136 | 122, 135 | syld 45 |
. . . . . . . . . . 11
 
   |
137 | 136 | con4d 109 |
. . . . . . . . . 10
     |
138 | 137 | imp 431 |
. . . . . . . . 9
 
   |
139 | | mnfxr 11414 |
. . . . . . . . . . 11
 |
140 | | elioo2 11677 |
. . . . . . . . . . 11
  
  
     |
141 | 139, 24, 140 | sylancr 669 |
. . . . . . . . . 10
          |
142 | 141 | adantr 467 |
. . . . . . . . 9
 
 
  
     |
143 | 113, 115,
138, 142 | mpbir3and 1191 |
. . . . . . . 8
 

     |
144 | 143 | ex 436 |
. . . . . . 7
        |
145 | 144 | ancld 556 |
. . . . . 6
  
       |
146 | | elin 3617 |
. . . . . . 7
             |
147 | | reconnlem2.2 |
. . . . . . . 8
       |
148 | | retop 21782 |
. . . . . . . . 9
     |
149 | | iooretop 21786 |
. . . . . . . . 9
        |
150 | | inopn 19929 |
. . . . . . . . 9
         
                   |
151 | 148, 149,
150 | mp3an13 1355 |
. . . . . . . 8
    

          |
152 | | eqid 2451 |
. . . . . . . . . . . 12
    
        
     |
153 | 85, 152 | tgioo 21814 |
. . . . . . . . . . 11
        
     |
154 | 153 | mopni2 21508 |
. . . . . . . . . 10
   
                
             
     

      |
155 | 102, 154 | mp3an1 1351 |
. . . . . . . . 9
                
        
    

      |
156 | 155 | ex 436 |
. . . . . . . 8
                
      
     

       |
157 | 147, 151,
156 | 3syl 18 |
. . . . . . 7
       
      
     

       |
158 | 146, 157 | syl5bir 222 |
. . . . . 6
               
    

       |
159 | 145, 158 | syld 45 |
. . . . 5
         
     

       |
160 | 112, 159 | mtod 181 |
. . . 4
   |
161 | | ltsubrp 11335 |
. . . . . . . . 9
 
  
  |
162 | 44, 161 | sylan 474 |
. . . . . . . 8
 

    |
163 | | rpre 11308 |
. . . . . . . . . 10

  |
164 | | resubcl 9938 |
. . . . . . . . . 10
 
     |
165 | 44, 163, 164 | syl2an 480 |
. . . . . . . . 9
 

    |
166 | 165, 48 | ltnled 9782 |
. . . . . . . 8
 

 

     |
167 | 162, 166 | mpbid 214 |
. . . . . . 7
 

    |
168 | 85 | bl2ioo 21810 |
. . . . . . . . . 10
 
       
           
    |
169 | 44, 163, 168 | syl2an 480 |
. . . . . . . . 9
 

       
               |
170 | 169 | sseq1d 3459 |
. . . . . . . 8
 

       
     
 
         |
171 | 15 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
               ![[,] [,]](_icc.gif) 
  |
172 | 2, 171 | syl5ss 3443 |
. . . . . . . . . . . . . . . 16
                ![[,] [,]](_icc.gif)     |
173 | 172 | sselda 3432 |
. . . . . . . . . . . . . . 15
   
      
 

   ![[,] [,]](_icc.gif)      |
174 | | elndif 3557 |
. . . . . . . . . . . . . . 15

    |
175 | 173, 174 | syl 17 |
. . . . . . . . . . . . . 14
   
      
 

   ![[,] [,]](_icc.gif)   

   |
176 | 128 | ad3antrrr 736 |
. . . . . . . . . . . . . . . 16
   
      
 
     ![[,] [,]](_icc.gif)         
   |
177 | | inss1 3652 |
. . . . . . . . . . . . . . . . . 18
   ![[,] [,]](_icc.gif)    |
178 | | simprl 764 |
. . . . . . . . . . . . . . . . . 18
   
      
 
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     |
179 | 177, 178 | sseldi 3430 |
. . . . . . . . . . . . . . . . 17
   
      
 
     ![[,] [,]](_icc.gif)         |
180 | | simplr 762 |
. . . . . . . . . . . . . . . . . 18
   
      
 
     ![[,] [,]](_icc.gif)                 |
181 | 18 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
 

   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)  
  |
182 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
 

   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
183 | 181, 182 | sseldd 3433 |
. . . . . . . . . . . . . . . . . . . 20
   
      
 

   ![[,] [,]](_icc.gif)      |
184 | 183 | adantrr 723 |
. . . . . . . . . . . . . . . . . . 19
   
      
 
     ![[,] [,]](_icc.gif)         |
185 | | simprr 766 |
. . . . . . . . . . . . . . . . . . 19
   
      
 
     ![[,] [,]](_icc.gif)       
   |
186 | 48 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
   
      
 
     ![[,] [,]](_icc.gif)         |
187 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
 
     ![[,] [,]](_icc.gif)         |
188 | 187 | rpred 11341 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
 
     ![[,] [,]](_icc.gif)         |
189 | 186, 188 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . . 20
   
      
 
     ![[,] [,]](_icc.gif)       
   |
190 | 181 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
 
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     |
191 | 30 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
 
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     |
192 | 41 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
 
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)   
  |
193 | | suprub 10570 |
. . . . . . . . . . . . . . . . . . . . . 22
      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)   

   ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)       |
194 | 190, 191,
192, 178, 193 | syl31anc 1271 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
 
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       |
195 | 194, 1 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . . . . 20
   
      
 
     ![[,] [,]](_icc.gif)         |
196 | 186, 187 | ltaddrpd 11371 |
. . . . . . . . . . . . . . . . . . . 20
   
      
 
     ![[,] [,]](_icc.gif)           |
197 | 184, 186,
189, 195, 196 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . . 19
   
      
 
     ![[,] [,]](_icc.gif)           |
198 | 165 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
   
      
 
     ![[,] [,]](_icc.gif)       
   |
199 | | rexr 9686 |
. . . . . . . . . . . . . . . . . . . . 21
   
   |
200 | | rexr 9686 |
. . . . . . . . . . . . . . . . . . . . 21
   
   |
201 | | elioo2 11677 |
. . . . . . . . . . . . . . . . . . . . 21
    
          
  
      |
202 | 199, 200,
201 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . 20
    
        
    
      |
203 | 198, 189,
202 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
   
      
 
     ![[,] [,]](_icc.gif)               
  
      |
204 | 184, 185,
197, 203 | mpbir3and 1191 |
. . . . . . . . . . . . . . . . . 18
   
      
 
     ![[,] [,]](_icc.gif)            
    |
205 | 180, 204 | sseldd 3433 |
. . . . . . . . . . . . . . . . 17
   
      
 
     ![[,] [,]](_icc.gif)         |
206 | 179, 205 | elind 3618 |
. . . . . . . . . . . . . . . 16
   
      
 
     ![[,] [,]](_icc.gif)           |
207 | 176, 206 | sseldd 3433 |
. . . . . . . . . . . . . . 15
   
      
 
     ![[,] [,]](_icc.gif)           |
208 | 207 | expr 620 |
. . . . . . . . . . . . . 14
   
      
 

   ![[,] [,]](_icc.gif)      

    |
209 | 175, 208 | mtod 181 |
. . . . . . . . . . . . 13
   
      
 

   ![[,] [,]](_icc.gif)   
    |
210 | 165 | ad2antrr 732 |
. . . . . . . . . . . . . 14
   
      
 

   ![[,] [,]](_icc.gif)        |
211 | 183, 210 | lenltd 9781 |
. . . . . . . . . . . . 13
   
      
 

   ![[,] [,]](_icc.gif)      
     |
212 | 209, 211 | mpbird 236 |
. . . . . . . . . . . 12
   
      
 

   ![[,] [,]](_icc.gif)    
   |
213 | 212 | ralrimiva 2802 |
. . . . . . . . . . 11
             
   ![[,] [,]](_icc.gif)        |
214 | 18 | ad2antrr 732 |
. . . . . . . . . . . 12
                ![[,] [,]](_icc.gif)     |
215 | 30 | ad2antrr 732 |
. . . . . . . . . . . 12
                ![[,] [,]](_icc.gif)     |
216 | 41 | ad2antrr 732 |
. . . . . . . . . . . 12
             
    ![[,] [,]](_icc.gif)      |
217 | 165 | adantr 467 |
. . . . . . . . . . . 12
                 |
218 | | suprleub 10573 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)   
          ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)   
     |
219 | 214, 215,
216, 217, 218 | syl31anc 1271 |
. . . . . . . . . . 11
                   ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)   
     |
220 | 213, 219 | mpbird 236 |
. . . . . . . . . 10
                  ![[,] [,]](_icc.gif)    
    |
221 | 1, 220 | syl5eqbr 4436 |
. . . . . . . . 9
                 |
222 | 221 | ex 436 |
. . . . . . . 8
 

              |
223 | 170, 222 | sylbid 219 |
. . . . . . 7
 

       
     
     |
224 | 167, 223 | mtod 181 |
. . . . . 6
 

      
     
  |
225 | 224 | nrexdv 2843 |
. . . . 5
        
        |
226 | | reconnlem2.3 |
. . . . . 6
       |
227 | 153 | mopni2 21508 |
. . . . . . . 8
   
           

        
    
  |
228 | 102, 227 | mp3an1 1351 |
. . . . . . 7
               
    
  |
229 | 228 | ex 436 |
. . . . . 6
    

        
    
   |
230 | 226, 229 | syl 17 |
. . . . 5
         
     
   |
231 | 225, 230 | mtod 181 |
. . . 4
   |
232 | | ioran 493 |
. . . 4
 
 
   |
233 | 160, 231,
232 | sylanbrc 670 |
. . 3
     |
234 | | elun 3574 |
. . 3
  

   |
235 | 233, 234 | sylnibr 307 |
. 2
     |
236 | | elicc2 11699 |
. . . . . 6
 
    ![[,] [,]](_icc.gif)  
    |
237 | 21, 23, 236 | syl2anc 667 |
. . . . 5
    ![[,] [,]](_icc.gif)  
    |
238 | 44, 65, 119, 237 | mpbir3and 1191 |
. . . 4
   ![[,] [,]](_icc.gif)    |
239 | 15, 238 | sseldd 3433 |
. . 3
   |
240 | | ssel 3426 |
. . 3
   
     |
241 | 239, 240 | syl5com 31 |
. 2
  
      |
242 | 235, 241 | mtod 181 |
1
 
   |