Step | Hyp | Ref
| Expression |
1 | | disjinfi.c |
. . 3
   |
2 | | id 22 |
. . . 4
   |
3 | | inss2 3644 |
. . . . 5
    
 |
4 | 3 | a1i 11 |
. . . 4
        |
5 | | ssfi 7810 |
. . . 4
               |
6 | 2, 4, 5 | syl2anc 673 |
. . 3
        |
7 | 1, 6 | syl 17 |
. 2
        |
8 | 3 | a1i 11 |
. . . . 5
        |
9 | 8, 1 | jca 541 |
. . . 4
    
 
   |
10 | | ssexg 4542 |
. . . 4
               |
11 | 9, 10 | syl 17 |
. . 3
        |
12 | | elinel1 3610 |
. . . . . . . . . . . . 13
   
 
     |
13 | | eluni2 4194 |
. . . . . . . . . . . . . . 15
     
    |
14 | 13 | biimpi 199 |
. . . . . . . . . . . . . 14
   
      |
15 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . 21
 |
16 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
17 | 16 | elrnmpt 5087 |
. . . . . . . . . . . . . . . . . . . . 21
    
   |
18 | 15, 17 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
   
  |
19 | 18 | biimpi 199 |
. . . . . . . . . . . . . . . . . . 19
   
  |
20 | 19 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
     
  |
21 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . 21
   |
22 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
23 | 22 | nfrn 5083 |
. . . . . . . . . . . . . . . . . . . . 21
     |
24 | 21, 23 | nfel 2624 |
. . . . . . . . . . . . . . . . . . . 20

   |
25 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . 20

 |
26 | 24, 25 | nfan 2031 |
. . . . . . . . . . . . . . . . . . 19
   
   |
27 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
28 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
29 | 27, 28 | eleqtrd 2551 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
30 | 29 | ex 441 |
. . . . . . . . . . . . . . . . . . . . 21
     |
31 | 30 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
       |
32 | 31 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
           |
33 | 26, 32 | reximdai 2853 |
. . . . . . . . . . . . . . . . . 18
      
    |
34 | 20, 33 | mpd 15 |
. . . . . . . . . . . . . . . . 17
     
  |
35 | 34 | ex 441 |
. . . . . . . . . . . . . . . 16
   

   |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . 15
   
    
    |
37 | 36 | rexlimdv 2870 |
. . . . . . . . . . . . . 14
   
 
   
   |
38 | 14, 37 | mpd 15 |
. . . . . . . . . . . . 13
   

  |
39 | 12, 38 | syl 17 |
. . . . . . . . . . . 12
   
 

  |
40 | 39 | adantl 473 |
. . . . . . . . . . 11
 
      
  |
41 | | nfv 1769 |
. . . . . . . . . . . . 13
   |
42 | | nfcv 2612 |
. . . . . . . . . . . . . 14
   |
43 | 23 | nfuni 4196 |
. . . . . . . . . . . . . . 15
      |
44 | | nfcv 2612 |
. . . . . . . . . . . . . . 15
   |
45 | 43, 44 | nfin 3630 |
. . . . . . . . . . . . . 14
        |
46 | 42, 45 | nfel 2624 |
. . . . . . . . . . . . 13

      |
47 | 41, 46 | nfan 2031 |
. . . . . . . . . . . 12
  
       |
48 | | nfre1 2846 |
. . . . . . . . . . . 12
  
   |
49 | 3 | sseli 3414 |
. . . . . . . . . . . . . 14
   
 
  |
50 | | simp2 1031 |
. . . . . . . . . . . . . . . 16
 
   |
51 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
 
   |
52 | | simpl 464 |
. . . . . . . . . . . . . . . . . 18
 
   |
53 | 51, 52 | elind 3609 |
. . . . . . . . . . . . . . . . 17
 
     |
54 | 53 | 3adant2 1049 |
. . . . . . . . . . . . . . . 16
 
     |
55 | | rspe 2844 |
. . . . . . . . . . . . . . . 16
 
   
    |
56 | 50, 54, 55 | syl2anc 673 |
. . . . . . . . . . . . . . 15
 
 
    |
57 | 56 | 3exp 1230 |
. . . . . . . . . . . . . 14
   
      |
58 | 49, 57 | syl 17 |
. . . . . . . . . . . . 13
   
 

 

     |
59 | 58 | adantl 473 |
. . . . . . . . . . . 12
 
      



     |
60 | 47, 48, 59 | rexlimd 2866 |
. . . . . . . . . . 11
 
       

     |
61 | 40, 60 | mpd 15 |
. . . . . . . . . 10
 
      
    |
62 | | disjinfi.d |
. . . . . . . . . . . . . . . . . . . . 21
 Disj
  |
63 | | disjors 4381 |
. . . . . . . . . . . . . . . . . . . . 21
Disj



 
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
64 | 62, 63 | sylib 201 |
. . . . . . . . . . . . . . . . . . . 20
  
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
65 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . 21
   
   ![]_ ]_](_urbrack.gif)    |
66 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
67 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . . . 23

 |
68 | | nfcsb1v 3365 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
 ![]_ ]_](_urbrack.gif)  |
69 | 21 | nfcsb1 3364 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
 ![]_ ]_](_urbrack.gif)  |
70 | 68, 69 | nfin 3630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
71 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
72 | 70, 71 | nfeq 2623 |
. . . . . . . . . . . . . . . . . . . . . . 23
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
73 | 67, 72 | nfor 2038 |
. . . . . . . . . . . . . . . . . . . . . 22
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
74 | 66, 73 | nfral 2789 |
. . . . . . . . . . . . . . . . . . . . 21
  
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
75 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
76 | | csbeq1a 3358 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ![]_ ]_](_urbrack.gif)   |
77 | 76 | ineq1d 3624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
78 | 77 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . . . . 23
     ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
79 | 75, 78 | orbi12d 724 |
. . . . . . . . . . . . . . . . . . . . . 22
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      |
80 | 79 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . . . 21
  

   ![]_ ]_](_urbrack.gif)  


 
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
81 | 65, 74, 80 | cbvral 3001 |
. . . . . . . . . . . . . . . . . . . 20
 

    ![]_ ]_](_urbrack.gif)  



 
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
82 | 64, 81 | sylibr 217 |
. . . . . . . . . . . . . . . . . . 19
  

   ![]_ ]_](_urbrack.gif)     |
83 | | rspa 2774 |
. . . . . . . . . . . . . . . . . . 19
   

   ![]_ ]_](_urbrack.gif)    

   ![]_ ]_](_urbrack.gif)     |
84 | 82, 83 | sylan 479 |
. . . . . . . . . . . . . . . . . 18
 
 

   ![]_ ]_](_urbrack.gif)     |
85 | 84 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     

   ![]_ ]_](_urbrack.gif)     |
86 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
       |
87 | | rspa 2774 |
. . . . . . . . . . . . . . . . . 18
   
   ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)     |
88 | 87 | orcomd 395 |
. . . . . . . . . . . . . . . . 17
   
   ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif) 
   |
89 | 85, 86, 88 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
         ![]_ ]_](_urbrack.gif) 
   |
90 | 89 | adantr 472 |
. . . . . . . . . . . . . . 15
   


  
  ![] ]](rbrack.gif)         ![]_ ]_](_urbrack.gif)     |
91 | | elinel1 3610 |
. . . . . . . . . . . . . . . . . . 19
  
  |
92 | 91 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
      ![] ]](rbrack.gif)      |
93 | | sbsbc 3259 |
. . . . . . . . . . . . . . . . . . . . . 22
   ![] ]](rbrack.gif)  
  ![]. ].](_drbrack.gif)     |
94 | | sbcel2 3782 |
. . . . . . . . . . . . . . . . . . . . . 22
   ![]. ].](_drbrack.gif)     ![]_ ]_](_urbrack.gif)     |
95 | | csbin 3803 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
96 | 95 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . . . . . 22
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
97 | 93, 94, 96 | 3bitri 279 |
. . . . . . . . . . . . . . . . . . . . 21
   ![] ]](rbrack.gif)  
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
98 | 97 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . 20
   ![] ]](rbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
99 | | elinel1 3610 |
. . . . . . . . . . . . . . . . . . . 20
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   ![] ]](rbrack.gif)     ![]_ ]_](_urbrack.gif)   |
101 | 100 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
      ![] ]](rbrack.gif)      ![]_ ]_](_urbrack.gif)   |
102 | 92, 101 | jca 541 |
. . . . . . . . . . . . . . . . 17
      ![] ]](rbrack.gif)       ![]_ ]_](_urbrack.gif)    |
103 | | inelcm 3823 |
. . . . . . . . . . . . . . . . . 18
 
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
104 | 103 | neneqd 2648 |
. . . . . . . . . . . . . . . . 17
 
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
105 | 102, 104 | syl 17 |
. . . . . . . . . . . . . . . 16
      ![] ]](rbrack.gif)   
   ![]_ ]_](_urbrack.gif)    |
106 | 105 | adantl 473 |
. . . . . . . . . . . . . . 15
   


  
  ![] ]](rbrack.gif)        ![]_ ]_](_urbrack.gif)    |
107 | | pm2.53 380 |
. . . . . . . . . . . . . . 15
     ![]_ ]_](_urbrack.gif) 
     ![]_ ]_](_urbrack.gif) 
   |
108 | 90, 106, 107 | sylc 61 |
. . . . . . . . . . . . . 14
   


  
  ![] ]](rbrack.gif)    
  |
109 | 108 | ex 441 |
. . . . . . . . . . . . 13
           ![] ]](rbrack.gif)   
   |
110 | 109 | ralrimiva 2809 |
. . . . . . . . . . . 12
 
 
      ![] ]](rbrack.gif)       |
111 | 110 | ralrimiva 2809 |
. . . . . . . . . . 11
  
   
  ![] ]](rbrack.gif)       |
112 | 111 | adantr 472 |
. . . . . . . . . 10
 
       
   
  ![] ]](rbrack.gif)       |
113 | 61, 112 | jca 541 |
. . . . . . . . 9
 
       

         ![] ]](rbrack.gif)        |
114 | | reu2 3214 |
. . . . . . . . 9
     

         ![] ]](rbrack.gif)        |
115 | 113, 114 | sylibr 217 |
. . . . . . . 8
 
           |
116 | | riotacl2 6283 |
. . . . . . . 8
   
           |
117 | 115, 116 | syl 17 |
. . . . . . 7
 
           
     |
118 | | nfriota1 6277 |
. . . . . . . . . . . 12
   
    |
119 | 118 | nfcsb1 3364 |
. . . . . . . . . . . . . 14
    
    ![]_ ]_](_urbrack.gif)  |
120 | 119, 44 | nfin 3630 |
. . . . . . . . . . . . 13
          ![]_ ]_](_urbrack.gif)   |
121 | 42, 120 | nfel 2624 |
. . . . . . . . . . . 12

   
    ![]_ ]_](_urbrack.gif)   |
122 | | csbeq1a 3358 |
. . . . . . . . . . . . . 14
     
  
    ![]_ ]_](_urbrack.gif)   |
123 | 122 | ineq1d 3624 |
. . . . . . . . . . . . 13
     
          ![]_ ]_](_urbrack.gif)    |
124 | 123 | eleq2d 2534 |
. . . . . . . . . . . 12
     
           ![]_ ]_](_urbrack.gif)     |
125 | 118, 66, 121, 124 | elrabf 3182 |
. . . . . . . . . . 11
  
   
        
   
    ![]_ ]_](_urbrack.gif)     |
126 | 125 | biimpi 199 |
. . . . . . . . . 10
  
   
        
   
    ![]_ ]_](_urbrack.gif)     |
127 | 126 | simpld 466 |
. . . . . . . . 9
  
   
          |
128 | 126 | simprd 470 |
. . . . . . . . . 10
  
   
           ![]_ ]_](_urbrack.gif)    |
129 | | ne0i 3728 |
. . . . . . . . . 10
         ![]_ ]_](_urbrack.gif)
         ![]_ ]_](_urbrack.gif)
   |
130 | 128, 129 | syl 17 |
. . . . . . . . 9
  
   
           ![]_ ]_](_urbrack.gif)
   |
131 | 127, 130 | jca 541 |
. . . . . . . 8
  
   
                 ![]_ ]_](_urbrack.gif)
    |
132 | 120, 71 | nfne 2742 |
. . . . . . . . 9
          ![]_ ]_](_urbrack.gif)   |
133 | 123 | neeq1d 2702 |
. . . . . . . . 9
     
           ![]_ ]_](_urbrack.gif)
    |
134 | 118, 66, 132, 133 | elrabf 3182 |
. . . . . . . 8
  
      
              ![]_ ]_](_urbrack.gif)
    |
135 | 131, 134 | sylibr 217 |
. . . . . . 7
  
   
        
     |
136 | 117, 135 | syl 17 |
. . . . . 6
 
           
     |
137 | 136 | ralrimiva 2809 |
. . . . 5
         
         |
138 | 69, 44 | nfin 3630 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)
  |
139 | 138, 71 | nfne 2742 |
. . . . . . . . . . . 12
     ![]_ ]_](_urbrack.gif)
  |
140 | | csbeq1a 3358 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
141 | 140 | ineq1d 3624 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)    |
142 | 141 | neeq1d 2702 |
. . . . . . . . . . . 12
   
   ![]_ ]_](_urbrack.gif)     |
143 | 21, 66, 139, 142 | elrabf 3182 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)     |
144 | 143 | simprbi 471 |
. . . . . . . . . 10
    
   ![]_ ]_](_urbrack.gif)    |
145 | | n0 3732 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)
     ![]_ ]_](_urbrack.gif)    |
146 | 144, 145 | sylib 201 |
. . . . . . . . 9
    
    ![]_ ]_](_urbrack.gif)    |
147 | 146 | adantl 473 |
. . . . . . . 8
 
         ![]_ ]_](_urbrack.gif)    |
148 | | nfv 1769 |
. . . . . . . . 9
         |
149 | | simpl 464 |
. . . . . . . . . 10
 
       |
150 | 143 | simplbi 467 |
. . . . . . . . . . 11
    
  |
151 | 150 | adantl 473 |
. . . . . . . . . 10
 
       |
152 | | elinel1 3610 |
. . . . . . . . . . . . . . 15
    ![]_ ]_](_urbrack.gif) 
  ![]_ ]_](_urbrack.gif)   |
153 | 152 | adantl 473 |
. . . . . . . . . . . . . 14
       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
154 | | simplr 770 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)     |
155 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . 19
  
  |
156 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . 20
   |
157 | 69, 156 | nfel 2624 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]_ ]_](_urbrack.gif)
 |
158 | 155, 157 | nfim 2023 |
. . . . . . . . . . . . . . . . . 18
   
   ![]_ ]_](_urbrack.gif)
  |
159 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
160 | 159 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . 19
  

     |
161 | 140 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . 19
 
  ![]_ ]_](_urbrack.gif)    |
162 | 160, 161 | imbi12d 327 |
. . . . . . . . . . . . . . . . . 18
   
   
   ![]_ ]_](_urbrack.gif)
    |
163 | | disjinfi.b |
. . . . . . . . . . . . . . . . . 18
 
   |
164 | 158, 162,
163 | chvar 2119 |
. . . . . . . . . . . . . . . . 17
 
   ![]_ ]_](_urbrack.gif)   |
165 | 164 | adantr 472 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
166 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
167 | 166 | elrnmpt1 5089 |
. . . . . . . . . . . . . . . 16
    ![]_ ]_](_urbrack.gif)
   ![]_ ]_](_urbrack.gif)

  ![]_ ]_](_urbrack.gif)    |
168 | 154, 165,
167 | syl2anc 673 |
. . . . . . . . . . . . . . 15
       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
169 | | nfcv 2612 |
. . . . . . . . . . . . . . . . 17
   |
170 | 140 | equcoms 1872 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
171 | 170 | eqcomd 2477 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif)   |
172 | 69, 169, 171 | cbvmpt 4487 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)     |
173 | 172 | rneqi 5067 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)     |
174 | 168, 173 | syl6eleq 2559 |
. . . . . . . . . . . . . 14
       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     |
175 | | elunii 4195 |
. . . . . . . . . . . . . 14
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  
     |
176 | 153, 174,
175 | syl2anc 673 |
. . . . . . . . . . . . 13
       ![]_ ]_](_urbrack.gif)        |
177 | | elinel2 3611 |
. . . . . . . . . . . . . 14
    ![]_ ]_](_urbrack.gif) 
  |
178 | 177 | adantl 473 |
. . . . . . . . . . . . 13
       ![]_ ]_](_urbrack.gif)     |
179 | 176, 178 | elind 3609 |
. . . . . . . . . . . 12
       ![]_ ]_](_urbrack.gif)          |
180 | | nfv 1769 |
. . . . . . . . . . . . . . 15

   |
181 | 42, 138 | nfel 2624 |
. . . . . . . . . . . . . . 15

   ![]_ ]_](_urbrack.gif)   |
182 | 141 | eleq2d 2534 |
. . . . . . . . . . . . . . 15
   
   ![]_ ]_](_urbrack.gif)
    |
183 | 180, 181,
182 | cbvriota 6280 |
. . . . . . . . . . . . . 14
      
   ![]_ ]_](_urbrack.gif)    |
184 | 183 | a1i 11 |
. . . . . . . . . . . . 13
       ![]_ ]_](_urbrack.gif)         
   ![]_ ]_](_urbrack.gif)     |
185 | | simpr 468 |
. . . . . . . . . . . . . . 15
       ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
186 | 154, 185 | jca 541 |
. . . . . . . . . . . . . 14
       ![]_ ]_](_urbrack.gif)   
   ![]_ ]_](_urbrack.gif)     |
187 | | rspe 2844 |
. . . . . . . . . . . . . . . . . 18
 
   ![]_ ]_](_urbrack.gif)   
   ![]_ ]_](_urbrack.gif)    |
188 | 187 | adantll 728 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif)   
   ![]_ ]_](_urbrack.gif)
   |
189 | | simpll 768 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)     |
190 | | sbequ 2225 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
 ![] ]](rbrack.gif)     ![] ]](rbrack.gif)      |
191 | | sbsbc 3259 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ![] ]](rbrack.gif)  
  ![]. ].](_drbrack.gif)     |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ![] ]](rbrack.gif)   
 ![]. ].](_drbrack.gif)
     |
193 | | sbcel2 3782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   ![]. ].](_drbrack.gif)     ![]_ ]_](_urbrack.gif)     |
194 | | csbin 3803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
195 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
196 | | csbconstg 3362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   ![]_ ]_](_urbrack.gif)   |
197 | 195, 196 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  ![]_ ]_](_urbrack.gif)  |
198 | 197 | ineq2i 3622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  |
199 | 194, 198 | eqtri 2493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   |
200 | 199 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
   |
201 | 193, 200 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ![]. ].](_drbrack.gif)      ![]_ ]_](_urbrack.gif)
   |
202 | 201 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
 ![]. ].](_drbrack.gif)
 
   ![]_ ]_](_urbrack.gif)
    |
203 | 190, 192,
202 | 3bitrd 287 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
 ![] ]](rbrack.gif)      ![]_ ]_](_urbrack.gif)     |
204 | 203 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . . . . 23
       ![] ]](rbrack.gif)      
   ![]_ ]_](_urbrack.gif)
     |
205 | | eqeq2 2482 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
206 | 204, 205 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . . 22
     
  ![] ]](rbrack.gif)    
   
   ![]_ ]_](_urbrack.gif)  
    |
207 | 206 | cbvralv 3005 |
. . . . . . . . . . . . . . . . . . . . 21
 
      ![] ]](rbrack.gif)   


   
   ![]_ ]_](_urbrack.gif)  
   |
208 | 207 | ralbii 2823 |
. . . . . . . . . . . . . . . . . . . 20
 

      ![] ]](rbrack.gif)   



   
   ![]_ ]_](_urbrack.gif)  
   |
209 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . 21
  
   
   ![]_ ]_](_urbrack.gif)
 
  |
210 | 68, 44 | nfin 3630 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     ![]_ ]_](_urbrack.gif)
  |
211 | 42, 210 | nfel 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24

   ![]_ ]_](_urbrack.gif)   |
212 | 181, 211 | nfan 2031 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
   |
213 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . . . 23

 |
214 | 212, 213 | nfim 2023 |
. . . . . . . . . . . . . . . . . . . . . 22
       ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif)
 
  |
215 | 66, 214 | nfral 2789 |
. . . . . . . . . . . . . . . . . . . . 21
  
     ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif)
 
  |
216 | 182 | anbi1d 719 |
. . . . . . . . . . . . . . . . . . . . . . 23
        ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif)
     |
217 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
218 | 216, 217 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . . 22
     
   ![]_ ]_](_urbrack.gif)
 

     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)       |
219 | 218 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . . . 21
  
   
   ![]_ ]_](_urbrack.gif)
 


     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)       |
220 | 209, 215,
219 | cbvral 3001 |
. . . . . . . . . . . . . . . . . . . 20
 

       ![]_ ]_](_urbrack.gif)
 



     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)      |
221 | | biid 244 |
. . . . . . . . . . . . . . . . . . . . 21
 

     ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
 



     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)      |
222 | | sbsbc 3259 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif) 
  ![]. ].](_drbrack.gif)    ![]_ ]_](_urbrack.gif)
   |
223 | | sbcel2 3782 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ![]. ].](_drbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)
   |
224 | | csbin 3803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
225 | | csbco 3359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
226 | | csbconstg 3362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   ![]_ ]_](_urbrack.gif)   |
227 | 195, 226 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  ![]_ ]_](_urbrack.gif)  |
228 | 225, 227 | ineq12i 3623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  |
229 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  |
230 | 224, 228,
229 | 3eqtri 2497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  |
231 | 230 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
   |
232 | 222, 223,
231 | 3bitrri 280 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ![]_ ]_](_urbrack.gif)    ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)
   |
233 | 232 | anbi2i 708 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)  
    ![]_ ]_](_urbrack.gif) 
  ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)     |
234 | 233 | imbi1i 332 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
 

     ![]_ ]_](_urbrack.gif)    ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)  
   |
235 | 234 | ralbii 2823 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
 


     ![]_ ]_](_urbrack.gif)    ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)  
   |
236 | 235 | ralbii 2823 |
. . . . . . . . . . . . . . . . . . . . 21
 

     ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
 



     ![]_ ]_](_urbrack.gif)    ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)  
   |
237 | 221, 236 | bitri 257 |
. . . . . . . . . . . . . . . . . . . 20
 

     ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
 



     ![]_ ]_](_urbrack.gif)    ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)  
   |
238 | 208, 220,
237 | 3bitri 279 |
. . . . . . . . . . . . . . . . . . 19
 

      ![] ]](rbrack.gif)   



     ![]_ ]_](_urbrack.gif)    ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)  
   |
239 | 112, 238 | sylib 201 |
. . . . . . . . . . . . . . . . . 18
 
       
     ![]_ ]_](_urbrack.gif) 
  ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)      |
240 | 189, 179,
239 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif)   

     ![]_ ]_](_urbrack.gif)    ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)  
   |
241 | 188, 240 | jca 541 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)    
   ![]_ ]_](_urbrack.gif)  

     ![]_ ]_](_urbrack.gif)
   ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)
 
    |
242 | | reu2 3214 |
. . . . . . . . . . . . . . . 16
     ![]_ ]_](_urbrack.gif)   
   ![]_ ]_](_urbrack.gif)
        ![]_ ]_](_urbrack.gif)    ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)       |
243 | 241, 242 | sylibr 217 |
. . . . . . . . . . . . . . 15
       ![]_ ]_](_urbrack.gif)   
   ![]_ ]_](_urbrack.gif)    |
244 | | riota1 6288 |
. . . . . . . . . . . . . . 15
     ![]_ ]_](_urbrack.gif) 
 
   ![]_ ]_](_urbrack.gif)  
     ![]_ ]_](_urbrack.gif)      |
245 | 243, 244 | syl 17 |
. . . . . . . . . . . . . 14
       ![]_ ]_](_urbrack.gif)    
 
 ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)
     |
246 | 186, 245 | mpbid 215 |
. . . . . . . . . . . . 13
       ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)     |
247 | 184, 246 | eqtr2d 2506 |
. . . . . . . . . . . 12
       ![]_ ]_](_urbrack.gif)          |
248 | 179, 247 | jca 541 |
. . . . . . . . . . 11
       ![]_ ]_](_urbrack.gif)        
 
      |
249 | 248 | ex 441 |
. . . . . . . . . 10
 
     ![]_ ]_](_urbrack.gif)       
 
       |
250 | 149, 151,
249 | syl2anc 673 |
. . . . . . . . 9
 
         ![]_ ]_](_urbrack.gif) 
       
       |
251 | 148, 250 | eximd 1980 |
. . . . . . . 8
 
          ![]_ ]_](_urbrack.gif)         
         |
252 | 147, 251 | mpd 15 |
. . . . . . 7
 
          
 
 
      |
253 | | df-rex 2762 |
. . . . . . 7
         
  
       
        |
254 | 252, 253 | sylibr 217 |
. . . . . 6
 
                   |
255 | 254 | ralrimiva 2809 |
. . . . 5
       
       
     |
256 | 137, 255 | jca 541 |
. . . 4
          
        
                   |
257 | | eqid 2471 |
. . . . 5
   
                     |
258 | 257 | fompt 37538 |
. . . 4
                         
 
           
         
       
      |
259 | 256, 258 | sylibr 217 |
. . 3
        
        
          |
260 | | fodomg 8971 |
. . 3
          
                                 |
261 | 11, 259, 260 | sylc 61 |
. 2
            |
262 | | domfi 7811 |
. 2
                 
     |
263 | 7, 261, 262 | syl2anc 673 |
1
       |