Step | Hyp | Ref
| Expression |
1 | | icccncfext.2 |
. . . . . . . . . . . 12
     |
2 | | retopon 21839 |
. . . . . . . . . . . 12
    TopOn   |
3 | 1, 2 | eqeltri 2536 |
. . . . . . . . . . 11
TopOn   |
4 | | icccncfext.5 |
. . . . . . . . . . . 12
   |
5 | | icccncfext.6 |
. . . . . . . . . . . 12
   |
6 | 4, 5 | iccssred 37687 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif) 
  |
7 | | resttopon 20232 |
. . . . . . . . . . 11
  TopOn 
  ![[,] [,]](_icc.gif)  
 ↾t   ![[,] [,]](_icc.gif)   TopOn   ![[,] [,]](_icc.gif)     |
8 | 3, 6, 7 | sylancr 674 |
. . . . . . . . . 10
 
↾t   ![[,] [,]](_icc.gif)   TopOn   ![[,] [,]](_icc.gif)     |
9 | | icccncfext.8 |
. . . . . . . . . . . 12
   |
10 | | icccncfext.3 |
. . . . . . . . . . . 12
  |
11 | 9, 10 | jctir 545 |
. . . . . . . . . . 11
      |
12 | | istopon 19995 |
. . . . . . . . . . 11
 TopOn  
    |
13 | 11, 12 | sylibr 217 |
. . . . . . . . . 10
 TopOn    |
14 | | icccncfext.9 |
. . . . . . . . . 10
   ↾t   ![[,] [,]](_icc.gif)      |
15 | | cnf2 20320 |
. . . . . . . . . 10
  
↾t   ![[,] [,]](_icc.gif)   TopOn   ![[,] [,]](_icc.gif)  
TopOn 
  ↾t   ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)      |
16 | 8, 13, 14, 15 | syl3anc 1276 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)      |
17 | | ffn 5755 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)    |
18 | 16, 17 | syl 17 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)    |
19 | | dffn3 5763 |
. . . . . . . 8
   ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)   
  |
20 | 18, 19 | sylib 201 |
. . . . . . 7
     ![[,] [,]](_icc.gif)      |
21 | 20 | ffvelrnda 6050 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)  
      |
22 | | fnfun 5699 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
23 | 18, 22 | syl 17 |
. . . . . . . . 9
   |
24 | 4 | rexrd 9721 |
. . . . . . . . . . 11
   |
25 | 5 | rexrd 9721 |
. . . . . . . . . . 11
   |
26 | | icccncfext.7 |
. . . . . . . . . . 11

  |
27 | | lbicc2 11783 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)    |
28 | 24, 25, 26, 27 | syl3anc 1276 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
29 | | fndm 5701 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    |
30 | 18, 29 | syl 17 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
31 | 30 | eqcomd 2468 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
32 | 28, 31 | eleqtrd 2542 |
. . . . . . . . 9
   |
33 | | fvelrn 6043 |
. . . . . . . . 9
         |
34 | 23, 32, 33 | syl2anc 671 |
. . . . . . . 8
       |
35 | | ubicc2 11784 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)    |
36 | 24, 25, 26, 35 | syl3anc 1276 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
37 | 36, 31 | eleqtrd 2542 |
. . . . . . . . 9
   |
38 | | fvelrn 6043 |
. . . . . . . . 9
         |
39 | 23, 37, 38 | syl2anc 671 |
. . . . . . . 8
       |
40 | 34, 39 | ifcld 3936 |
. . . . . . 7
                |
41 | 40 | adantr 471 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)                  |
42 | 21, 41 | ifclda 3925 |
. . . . 5
     ![[,] [,]](_icc.gif)                        |
43 | 42 | adantr 471 |
. . . 4
 

    ![[,] [,]](_icc.gif)                        |
44 | | icccncfext.4 |
. . . . 5
     ![[,] [,]](_icc.gif)         
              |
45 | | nfv 1772 |
. . . . . . 7
   ![[,] [,]](_icc.gif)   |
46 | | nfcv 2603 |
. . . . . . 7
       |
47 | | nfcv 2603 |
. . . . . . 7
                |
48 | 45, 46, 47 | nfif 3922 |
. . . . . 6
      ![[,] [,]](_icc.gif)         
             |
49 | | nfv 1772 |
. . . . . . 7

  ![[,] [,]](_icc.gif)   |
50 | | icccncfext.1 |
. . . . . . . 8
   |
51 | | nfcv 2603 |
. . . . . . . 8
   |
52 | 50, 51 | nffv 5899 |
. . . . . . 7
       |
53 | | nfv 1772 |
. . . . . . . 8
  |
54 | | nfcv 2603 |
. . . . . . . . 9
   |
55 | 50, 54 | nffv 5899 |
. . . . . . . 8
       |
56 | | nfcv 2603 |
. . . . . . . . 9
   |
57 | 50, 56 | nffv 5899 |
. . . . . . . 8
       |
58 | 53, 55, 57 | nfif 3922 |
. . . . . . 7
                |
59 | 49, 52, 58 | nfif 3922 |
. . . . . 6
      ![[,] [,]](_icc.gif)                       |
60 | | eleq1 2528 |
. . . . . . 7
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     |
61 | | fveq2 5892 |
. . . . . . 7
           |
62 | | breq1 4421 |
. . . . . . . 8
 
   |
63 | 62 | ifbid 3915 |
. . . . . . 7
  
                          |
64 | 60, 61, 63 | ifbieq12d 3920 |
. . . . . 6
  
  ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)                        |
65 | 48, 59, 64 | cbvmpt 4510 |
. . . . 5
     ![[,] [,]](_icc.gif)                            ![[,] [,]](_icc.gif)                        |
66 | 44, 65 | eqtri 2484 |
. . . 4
     ![[,] [,]](_icc.gif)                        |
67 | 43, 66 | fmptd 6074 |
. . 3
       |
68 | 67 | adantr 471 |
. . . . 5
 

      |
69 | | simplll 773 |
. . . . . . . . . . 11
   

 ↾t          |
70 | | simplr 767 |
. . . . . . . . . . 11
   

 ↾t       
 ↾t    |
71 | 69, 70 | jca 539 |
. . . . . . . . . 10
   

 ↾t        

↾t     |
72 | | ssid 3463 |
. . . . . . . . . . . . . 14
 |
73 | 72 | a1i 11 |
. . . . . . . . . . . . 13
   |
74 | | frn 5762 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)   
  |
75 | 16, 74 | syl 17 |
. . . . . . . . . . . . 13
   |
76 | | cnrest2 20357 |
. . . . . . . . . . . . 13
  TopOn 
   
↾t   ![[,] [,]](_icc.gif)   
  ↾t   ![[,] [,]](_icc.gif)    ↾t      |
77 | 13, 73, 75, 76 | syl3anc 1276 |
. . . . . . . . . . . 12
   
↾t   ![[,] [,]](_icc.gif)   
  ↾t   ![[,] [,]](_icc.gif)    ↾t      |
78 | 14, 77 | mpbid 215 |
. . . . . . . . . . 11
   ↾t   ![[,] [,]](_icc.gif)    ↾t     |
79 | 78 | anim1i 576 |
. . . . . . . . . 10
 

↾t      ↾t   ![[,] [,]](_icc.gif)    ↾t   
↾t     |
80 | | cnima 20336 |
. . . . . . . . . 10
    ↾t   ![[,] [,]](_icc.gif)    ↾t  
 ↾t         ↾t   ![[,] [,]](_icc.gif)     |
81 | 71, 79, 80 | 3syl 18 |
. . . . . . . . 9
   

 ↾t              ↾t   ![[,] [,]](_icc.gif)     |
82 | | retop 21837 |
. . . . . . . . . . . . . 14
     |
83 | 1, 82 | eqeltri 2536 |
. . . . . . . . . . . . 13
 |
84 | 83 | a1i 11 |
. . . . . . . . . . . 12
   |
85 | | reex 9661 |
. . . . . . . . . . . . . 14
 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
   |
87 | 86, 6 | ssexd 4566 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    |
88 | 84, 87 | jca 539 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)     |
89 | 69, 88 | syl 17 |
. . . . . . . . . 10
   

 ↾t           ![[,] [,]](_icc.gif)     |
90 | | elrest 15381 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)          ↾t   ![[,] [,]](_icc.gif)  

        ![[,] [,]](_icc.gif)      |
91 | 89, 90 | syl 17 |
. . . . . . . . 9
   

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

        ![[,] [,]](_icc.gif)      |
92 | 81, 91 | mpbid 215 |
. . . . . . . 8
   

 ↾t        
        ![[,] [,]](_icc.gif)     |
93 | 69 | 3ad2ant1 1035 |
. . . . . . . . . . 11
       ↾t       
        ![[,] [,]](_icc.gif)   
  |
94 | | simpllr 774 |
. . . . . . . . . . . 12
   

 ↾t          |
95 | 94 | 3ad2ant1 1035 |
. . . . . . . . . . 11
       ↾t       
        ![[,] [,]](_icc.gif)   
  |
96 | | simp1r 1039 |
. . . . . . . . . . 11
       ↾t       
        ![[,] [,]](_icc.gif)   
      |
97 | 93, 95, 96 | jca31 541 |
. . . . . . . . . 10
       ↾t       
        ![[,] [,]](_icc.gif)   
          |
98 | | simpll2 1054 |
. . . . . . . . . . . . . 14
     

    
        ![[,] [,]](_icc.gif)             
  |
99 | | iooretop 21841 |
. . . . . . . . . . . . . . . . 17
        |
100 | 99, 1 | eleqtrri 2539 |
. . . . . . . . . . . . . . . 16
    |
101 | | iooretop 21841 |
. . . . . . . . . . . . . . . . 17
        |
102 | 101, 1 | eleqtrri 2539 |
. . . . . . . . . . . . . . . 16
    |
103 | | unopn 19988 |
. . . . . . . . . . . . . . . 16
                   |
104 | 83, 100, 102, 103 | mp3an 1373 |
. . . . . . . . . . . . . . 15
         |
105 | | unopn 19988 |
. . . . . . . . . . . . . . 15
 
                     |
106 | 83, 104, 105 | mp3an13 1364 |
. . . . . . . . . . . . . 14
             |
107 | 98, 106 | syl 17 |
. . . . . . . . . . . . 13
     

    
        ![[,] [,]](_icc.gif)                          |
108 | | simpl1l 1065 |
. . . . . . . . . . . . . . 15
          
        ![[,] [,]](_icc.gif)             |
109 | 108 | adantr 471 |
. . . . . . . . . . . . . 14
     

    
        ![[,] [,]](_icc.gif)              
   |
110 | | simpl1r 1066 |
. . . . . . . . . . . . . . 15
          
        ![[,] [,]](_icc.gif)               |
111 | 110 | adantr 471 |
. . . . . . . . . . . . . 14
     

    
        ![[,] [,]](_icc.gif)                    |
112 | | simpll3 1055 |
. . . . . . . . . . . . . 14
     

    
        ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)     |
113 | | difreicc 11799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
    ![[,] [,]](_icc.gif)             |
114 | 4, 5, 113 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    ![[,] [,]](_icc.gif)             |
115 | 114 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
            ![[,] [,]](_icc.gif)     |
116 | 115 | eleq2d 2525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             ![[,] [,]](_icc.gif)      |
117 | 116 | notbid 300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
   ![[,] [,]](_icc.gif)      |
118 | 117 | biimpa 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
        
   ![[,] [,]](_icc.gif)     |
119 | | eldif 3426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)     |
120 | 118, 119 | sylnib 310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
        

  ![[,] [,]](_icc.gif)     |
121 | | imnan 428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)     |
122 | 120, 121 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
        

  ![[,] [,]](_icc.gif)     |
123 | 122 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
        
   ![[,] [,]](_icc.gif)    |
124 | 123 | notnotrd 118 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
        
   ![[,] [,]](_icc.gif)    |
125 | 124 | an32s 818 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
           ![[,] [,]](_icc.gif)    |
126 | 125 | adantlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
              
  ![[,] [,]](_icc.gif)    |
127 | | simplll 773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
              
  |
128 | 6 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
  ![[,] [,]](_icc.gif)  
  |
129 | 16 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
  ![[,] [,]](_icc.gif)  
    ![[,] [,]](_icc.gif)      |
130 | 129 | ffvelrnda 6050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)         |
131 | 16, 28 | ffvelrnd 6051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
132 | 131 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)   
      |
133 | 16, 36 | ffvelrnd 6051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
134 | 133 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)          |
135 | 132, 134 | ifclda 3925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)                  |
136 | 130, 135 | ifclda 3925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
  ![[,] [,]](_icc.gif)  
    ![[,] [,]](_icc.gif)                        |
137 | 66 | fvmpt2 5985 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      ![[,] [,]](_icc.gif)                      
        ![[,] [,]](_icc.gif)                        |
138 | 128, 136,
137 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)                        |
139 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
140 | 139 | iftrued 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  ![[,] [,]](_icc.gif)  
    ![[,] [,]](_icc.gif)                            |
141 | 138, 140 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  ![[,] [,]](_icc.gif)  
          |
142 | 141 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  ![[,] [,]](_icc.gif)  
          |
143 | 127, 126,
142 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
              
          |
144 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
              
      |
145 | 143, 144 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
              
      |
146 | 127, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
              
  ![[,] [,]](_icc.gif)    |
147 | | elpreima 6030 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
              
     
   ![[,] [,]](_icc.gif) 
        |
149 | 126, 145,
148 | mpbir2and 938 |
. . . . . . . . . . . . . . . . . . . . . 22
   
              
       |
150 | 149 | adantlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
          
        ![[,] [,]](_icc.gif)            
       |
151 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . 21
          
        ![[,] [,]](_icc.gif)            
        ![[,] [,]](_icc.gif)     |
152 | 150, 151 | eleqtrd 2542 |
. . . . . . . . . . . . . . . . . . . 20
          
        ![[,] [,]](_icc.gif)            

  ![[,] [,]](_icc.gif)     |
153 | | elin 3629 |
. . . . . . . . . . . . . . . . . . . 20
    ![[,] [,]](_icc.gif)  

  ![[,] [,]](_icc.gif)     |
154 | 152, 153 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
          
        ![[,] [,]](_icc.gif)            

  ![[,] [,]](_icc.gif)     |
155 | 154 | simpld 465 |
. . . . . . . . . . . . . . . . . 18
          
        ![[,] [,]](_icc.gif)            
  |
156 | 155 | ex 440 |
. . . . . . . . . . . . . . . . 17
   
              ![[,] [,]](_icc.gif)   

           |
157 | 156 | orrd 384 |
. . . . . . . . . . . . . . . 16
   
              ![[,] [,]](_icc.gif)   
            |
158 | 157 | orcomd 394 |
. . . . . . . . . . . . . . 15
   
              ![[,] [,]](_icc.gif)   

           |
159 | | elun 3586 |
. . . . . . . . . . . . . . 15
                       |
160 | 158, 159 | sylibr 217 |
. . . . . . . . . . . . . 14
   
              ![[,] [,]](_icc.gif)   

           |
161 | 109, 111,
112, 160 | syl21anc 1275 |
. . . . . . . . . . . . 13
     

    
        ![[,] [,]](_icc.gif)                          |
162 | | imaundi 5270 |
. . . . . . . . . . . . . 14
                                 |
163 | 109 | simpld 465 |
. . . . . . . . . . . . . . . . . 18
     

    
        ![[,] [,]](_icc.gif)                |
164 | | toponss 19999 |
. . . . . . . . . . . . . . . . . . 19
  TopOn 
   |
165 | 3, 98, 164 | sylancr 674 |
. . . . . . . . . . . . . . . . . 18
     

    
        ![[,] [,]](_icc.gif)                |
166 | 163, 165,
112 | jca31 541 |
. . . . . . . . . . . . . . . . 17
     

    
        ![[,] [,]](_icc.gif)                         ![[,] [,]](_icc.gif)      |
167 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
     

    
        ![[,] [,]](_icc.gif)                    |
168 | | simpr 467 |
. . . . . . . . . . . . . . . . 17
     

    
        ![[,] [,]](_icc.gif)                    |
169 | 44 | funmpt2 5642 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
171 | 170 | ad5antr 745 |
. . . . . . . . . . . . . . . . . . . . 21
     
         ![[,] [,]](_icc.gif)                     |
172 | | fvelima 5944 |
. . . . . . . . . . . . . . . . . . . . 21
       
      |
173 | 171, 172 | sylancom 678 |
. . . . . . . . . . . . . . . . . . . 20
     
         ![[,] [,]](_icc.gif)                   
      |
174 | | eqcom 2469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
      |
175 | 174 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
176 | 175 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . . . . . 22
                ![[,] [,]](_icc.gif)             
    
           |
177 | | simp1ll 1077 |
. . . . . . . . . . . . . . . . . . . . . . 23
                ![[,] [,]](_icc.gif)             
    
       
         ![[,] [,]](_icc.gif)           |
178 | | simp1lr 1078 |
. . . . . . . . . . . . . . . . . . . . . . 23
                ![[,] [,]](_icc.gif)             
    
           |
179 | | simp2 1015 |
. . . . . . . . . . . . . . . . . . . . . . 23
                ![[,] [,]](_icc.gif)             
    
       |
180 | | simp-5l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                ![[,] [,]](_icc.gif)             

  ![[,] [,]](_icc.gif)       |
181 | | simp-5r 784 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                ![[,] [,]](_icc.gif)             

  ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)     |
182 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                ![[,] [,]](_icc.gif)             

  ![[,] [,]](_icc.gif)     |
183 | 180, 181,
182 | jca31 541 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                ![[,] [,]](_icc.gif)             

  ![[,] [,]](_icc.gif)     
         ![[,] [,]](_icc.gif)       |
184 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     |
185 | 184 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  
  ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)      |
186 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
187 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
188 | 186, 187 | eqeq12d 2477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
           |
189 | 185, 188 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
  ![[,] [,]](_icc.gif)             
  ![[,] [,]](_icc.gif)               |
190 | 189, 141 | chvarv 2118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
  ![[,] [,]](_icc.gif)  
          |
191 | 190 | adant423 37408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            ![[,] [,]](_icc.gif)   

  ![[,] [,]](_icc.gif)             |
192 | 191 | adantlllr 37402 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)             |
193 | | simp-4l 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
194 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
195 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            ![[,] [,]](_icc.gif)   

  ![[,] [,]](_icc.gif)     |
196 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            ![[,] [,]](_icc.gif)   

  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
197 | 195, 196 | elind 3630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            ![[,] [,]](_icc.gif)   

  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
198 | | eqcom 2469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)          |
199 | 198 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)          |
200 | 199 | ad3antlr 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            ![[,] [,]](_icc.gif)   

  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)          |
201 | 197, 200 | eleqtrd 2542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            ![[,] [,]](_icc.gif)   

  ![[,] [,]](_icc.gif)          |
202 | 201 | adantlllr 37402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
203 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 |
204 | 18 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
  ![[,] [,]](_icc.gif)    |
205 | | elpreima 6030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   ![[,] [,]](_icc.gif)          |
207 | 203, 206 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             ![[,] [,]](_icc.gif)         |
208 | 207 | simprd 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                |
209 | 193, 194,
202, 208 | syl21anc 1275 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
210 | 192, 209 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
211 | 183, 210 | sylancom 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                ![[,] [,]](_icc.gif)             

  ![[,] [,]](_icc.gif)         |
212 | | simp-5l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
     
    

  ![[,] [,]](_icc.gif)     |
213 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
     
    

  ![[,] [,]](_icc.gif)         |
214 | 212, 213 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
     
    

  ![[,] [,]](_icc.gif)   
       |
215 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
     
    

  ![[,] [,]](_icc.gif)         |
216 | | simp-5r 784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
     
    

  ![[,] [,]](_icc.gif)     |
217 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
     
    

  ![[,] [,]](_icc.gif)     |
218 | 216, 217 | sseldd 3445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
     
    

  ![[,] [,]](_icc.gif)     |
219 | 214, 215,
218 | jca31 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
     
    

  ![[,] [,]](_icc.gif)               
   |
220 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
              

  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                         |
221 | | breq1 4421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   |
222 | 221 | ifbid 3915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                             |
223 | 184, 187,
222 | ifeq123d 37412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)                        |
224 | 223 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
    
    

  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)                        |
225 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
              

  ![[,] [,]](_icc.gif)     |
226 | | iffalse 3902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                     |
227 | 226 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
              

  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                                     |
228 | | simp-5r 784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
    
    

  ![[,] [,]](_icc.gif)          |
229 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
    
    

  ![[,] [,]](_icc.gif)          |
230 | 228, 229 | ifclda 3925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
              

  ![[,] [,]](_icc.gif)                  |
231 | 227, 230 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
              

  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                        |
232 | 220, 224,
225, 231 | fvmptd 5982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
              

  ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)                        |
233 | 232, 227 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
              

  ![[,] [,]](_icc.gif)                      |
234 | 233, 230 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              

  ![[,] [,]](_icc.gif)         |
235 | 219, 234 | sylancom 678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
     
    

  ![[,] [,]](_icc.gif)         |
236 | 235 | adantl4r 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                ![[,] [,]](_icc.gif)             
   ![[,] [,]](_icc.gif)  
      |
237 | 211, 236 | pm2.61dan 805 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
         ![[,] [,]](_icc.gif)                     |
238 | 177, 178,
179, 237 | syl21anc 1275 |
. . . . . . . . . . . . . . . . . . . . . 22
                ![[,] [,]](_icc.gif)             
    
           |
239 | 176, 238 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . . . 21
                ![[,] [,]](_icc.gif)             
    
       |
240 | 239 | rexlimdv3a 2893 |
. . . . . . . . . . . . . . . . . . . 20
     
         ![[,] [,]](_icc.gif)                    
       |
241 | 173, 240 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
     
         ![[,] [,]](_icc.gif)                     |
242 | 241 | ex 440 |
. . . . . . . . . . . . . . . . . 18
    
         ![[,] [,]](_icc.gif)                      |
243 | 242 | alrimiv 1784 |
. . . . . . . . . . . . . . . . 17
    
         ![[,] [,]](_icc.gif)                        |
244 | 166, 167,
168, 243 | syl21anc 1275 |
. . . . . . . . . . . . . . . 16
     

    
        ![[,] [,]](_icc.gif)                    
   |
245 | | dfss2 3433 |
. . . . . . . . . . . . . . . 16
    
          |
246 | 244, 245 | sylibr 217 |
. . . . . . . . . . . . . . 15
     

    
        ![[,] [,]](_icc.gif)                 
  |
247 | | imaundi 5270 |
. . . . . . . . . . . . . . . . 17
                             |
248 | 169 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       
  |
249 | | fvelima 5944 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         

          |
250 | 248, 249 | sylancom 678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                   |
251 | | simp1l 1038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             
    
  |
252 | | simp2 1015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             
    
     |
253 | | simp3 1016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             
    
      |
254 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   
     ![[,] [,]](_icc.gif)                         |
255 | 223 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  
         ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)                        |
256 | | elioore 11700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      |
257 | 256 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   
  |
258 | | elioo3g 11699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   

     |
259 | 258 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
     |
260 | 259 | simprrd 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
      |
261 | 260 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   
  |
262 | | ltnle 9744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
 
   |
263 | 256, 4, 262 | syl2anr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   

   |
264 | 261, 263 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   
  |
265 | 264 | intn3an2d 1390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   
    |
266 | 4, 5 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     |
267 | 266 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   
    |
268 | | elicc2 11733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
    ![[,] [,]](_icc.gif)  
    |
269 | 267, 268 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   
   ![[,] [,]](_icc.gif)  
    |
270 | 265, 269 | mtbird 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   
  ![[,] [,]](_icc.gif)    |
271 | 270 | iffalsed 3904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   
    ![[,] [,]](_icc.gif)                                     |
272 | 260 | iftrued 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                       |
273 | 272 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   
 
                 |
274 | 271, 273 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
   
    ![[,] [,]](_icc.gif)                            |
275 | 131 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
   
      |
276 | 274, 275 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   
    ![[,] [,]](_icc.gif)                        |
277 | 254, 255,
257, 276 | fvmptd 5982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   
        ![[,] [,]](_icc.gif)                        |
278 | 277 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
                 ![[,] [,]](_icc.gif)                        |
279 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
               |
280 | 274 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
             ![[,] [,]](_icc.gif)                            |
281 | 278, 279,
280 | 3eqtr3d 2504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
               |
282 | 251, 252,
253, 281 | syl21anc 1275 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
    
      |
283 | 282 | rexlimdv3a 2893 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
         
               |
284 | 250, 283 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
              |
285 | | elsn 3994 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
286 | 284, 285 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                |
287 | 286 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
288 | 287 | ssrdv 3450 |
. . . . . . . . . . . . . . . . . . . . 21
                |
289 | 288 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
 
    
               |
290 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
      |
291 | 290 | snssd 4130 |
. . . . . . . . . . . . . . . . . . . 20
 
    
        |
292 | 289, 291 | sstrd 3454 |
. . . . . . . . . . . . . . . . . . 19
 
    
         |
293 | 292 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
                      |
294 | | fvelima 5944 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
           |
295 | 170, 294 | sylan 478 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       
           |
296 | | simp1l 1038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  
  |
297 | | simp2 1015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  
     |
298 | | simp3 1016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  
      |
299 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   
     ![[,] [,]](_icc.gif)                         |
300 | 223 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)                        |
301 | | elioore 11700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
  |
302 | 301 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   
  |
303 | 16 | ffvelrnda 6050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
  ![[,] [,]](_icc.gif)  
      |
304 | 303 | adantlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         ![[,] [,]](_icc.gif)         |
305 | 4 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   
  |
306 | 5 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   
  |
307 | 26 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   
  |
308 | | elioo3g 11699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     
 
    |
309 | 308 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   
 
      |
310 | 309 | simprld 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
   
  |
311 | 310 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   
  |
312 | 305, 306,
302, 307, 311 | lelttrd 9824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   
  |
313 | 305, 302,
312 | ltnsymd 9815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   
  |
314 | 313 | iffalsed 3904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   
 
                 |
315 | 133 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   
      |
316 | 314, 315 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   
 
             |
317 | 316 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      
  ![[,] [,]](_icc.gif)                  |
318 | 304, 317 | ifclda 3925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   
    ![[,] [,]](_icc.gif)                        |
319 | 299, 300,
302, 318 | fvmptd 5982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   
        ![[,] [,]](_icc.gif)                        |
320 | 319 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                    ![[,] [,]](_icc.gif)                        |
321 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                  |
322 | 306, 302 | ltnled 9813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   

   |
323 | 311, 322 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   
  |
324 | 323 | intn3an3d 1391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   
    |
325 | 266 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   
    |
326 | 325, 268 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   
   ![[,] [,]](_icc.gif)  
    |
327 | 324, 326 | mtbird 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
   
  ![[,] [,]](_icc.gif)    |
328 | 327 | iffalsed 3904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   
    ![[,] [,]](_icc.gif)                                     |
329 | 328, 314 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   
    ![[,] [,]](_icc.gif)                            |
330 | 329 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                ![[,] [,]](_icc.gif)                            |
331 | 320, 321,
330 | 3eqtr3d 2504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                  |
332 | 296, 297,
298, 331 | syl21anc 1275 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                  
      |
333 | 332 | rexlimdv3a 2893 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       
 
       
       |
334 | 295, 333 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       
      |
335 | | elsn 3994 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
336 | 334, 335 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       
        |
337 | 336 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
338 | 337 | ssrdv 3450 |
. . . . . . . . . . . . . . . . . . . . 21
                |
339 | 338 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
 
    
               |
340 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
      |
341 | 340 | snssd 4130 |
. . . . . . . . . . . . . . . . . . . 20
 
    
        |
342 | 339, 341 | sstrd 3454 |
. . . . . . . . . . . . . . . . . . 19
 
    
         |
343 | 342 | adantlr 726 |
. . . . . . . . . . . . . . . . . 18
                      |
344 | 293, 343 | unssd 3622 |
. . . . . . . . . . . . . . . . 17
                               |
345 | 247, 344 | syl5eqss 3488 |
. . . . . . . . . . . . . . . 16
                        
  |
346 | 163, 167,
168, 345 | syl21anc 1275 |
. . . . . . . . . . . . . . 15
     

    
        ![[,] [,]](_icc.gif)                            |
347 | 246, 346 | unssd 3622 |
. . . . . . . . . . . . . 14
     

    
        ![[,] [,]](_icc.gif)                                  |
348 | 162, 347 | syl5eqss 3488 |
. . . . . . . . . . . . 13
     

    
        ![[,] [,]](_icc.gif)                              |
349 | | eleq2 2529 |
. . . . . . . . . . . . . . 15
          

             |
350 | | imaeq2 5186 |
. . . . . . . . . . . . . . . 16
          
                    |
351 | 350 | sseq1d 3471 |
. . . . . . . . . . . . . . 15
          
                      |
352 | 349, 351 | anbi12d 722 |
. . . . . . . . . . . . . 14
          
      
                             |
353 | 352 | rspcev 3162 |
. . . . . . . . . . . . 13
                                       

       |
354 | 107, 161,
348, 353 | syl12anc 1274 |
. . . . . . . . . . . 12
     

    
        ![[,] [,]](_icc.gif)              
        |
355 | 83 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
356 | | iooretop 21841 |
. . . . . . . . . . . . . . . . . 18
        |
357 | 356, 1 | eleqtrri 2539 |
. . . . . . . . . . . . . . . . 17
    |
358 | | inopn 19984 |
. . . . . . . . . . . . . . . . 17
 
           |
359 | 83, 357, 358 | mp3an13 1364 |
. . . . . . . . . . . . . . . 16
 
      |
360 | 100 | a1i 11 |
. . . . . . . . . . . . . . . 16
      |
361 | | unopn 19988 |
. . . . . . . . . . . . . . . 16
  
                    |
362 | 355, 359,
360, 361 | syl3anc 1276 |
. . . . . . . . . . . . . . 15
             |
363 | 362 | 3ad2ant2 1036 |
. . . . . . . . . . . . . 14
   
              ![[,] [,]](_icc.gif)   
 
          |
364 | 363 | ad2antrr 737 |
. . . . . . . . . . . . 13
     

    
        ![[,] [,]](_icc.gif)                          |
365 | | simpll1 1053 |
. . . . . . . . . . . . . 14
     

    
        ![[,] [,]](_icc.gif)                        |
366 | | simpll3 1055 |
. . . . . . . . . . . . . 14
     

    
        ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)     |
367 | | simpr 467 |
. . . . . . . . . . . . . 14
     

    
        ![[,] [,]](_icc.gif)             
      |
368 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . 20
     

             ![[,] [,]](_icc.gif)               
              ![[,] [,]](_icc.gif)      |
369 | 266 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
           
   |
370 | | eqimss 3496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)             |
371 | 113, 370 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
    ![[,] [,]](_icc.gif)             |
372 | | difcom 3864 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)    |
373 | 371, 372 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
             ![[,] [,]](_icc.gif)    |
374 | 369, 373 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
                    
  ![[,] [,]](_icc.gif)    |
375 | 374 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
          
    
                ![[,] [,]](_icc.gif)    |
376 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
    
      |
377 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
    
   
     |
378 | | elioore 11700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
  |
379 | 378 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   
  |
380 | | elioo3g 11699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
     
 
    |
381 | 380 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   
 
      |
382 | 381 | simprld 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   
  |
383 | 382 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
   
  |
384 | 5 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
   
  |
385 | 384, 379 | ltnled 9813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
   

   |
386 | 383, 385 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
   
  |
387 | 386 | intn3an3d 1391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   
    |
388 | 266 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
   
    |
389 | | elicc2 11733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
    ![[,] [,]](_icc.gif)  
    |
390 | 388, 389 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   
   ![[,] [,]](_icc.gif)  
    |
391 | 387, 390 | mtbird 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   
  ![[,] [,]](_icc.gif)    |
392 | 391 | iffalsed 3904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   
    ![[,] [,]](_icc.gif)                                ![]() |