Proof of Theorem iunrelexp0
Step | Hyp | Ref
| Expression |
1 | | df-pr 3971 |
. . . . . . 7
          |
2 | 1 | ineq1i 3630 |
. . . . . 6
              |
3 | | indir 3691 |
. . . . . 6
                   |
4 | 2, 3 | eqtr2i 2474 |
. . . . 5
                |
5 | 4 | uneq1i 3584 |
. . . 4
                    |
6 | | inss2 3653 |
. . . . 5
      |
7 | | ssequn1 3604 |
. . . . 5
     
         |
8 | 6, 7 | mpbi 212 |
. . . 4
        |
9 | 5, 8 | eqtr2i 2474 |
. . 3
             |
10 | | iuneq1 4292 |
. . . 4
            
                       |
11 | 10 | oveq1d 6305 |
. . 3
            
 
                           |
12 | 9, 11 | ax-mp 5 |
. 2
 
                          |
13 | | dmiun 5043 |
. . . . . . 7
                                   |
14 | | iunxun 4363 |
. . . . . . 7
             
                         |
15 | | iunxun 4363 |
. . . . . . . . . 10
                         
    
     |
16 | 15 | equncomi 3580 |
. . . . . . . . 9
                         
    
     |
17 | 16 | uneq1i 3584 |
. . . . . . . 8
 
                                              |
18 | 17 | equncomi 3580 |
. . . . . . 7
 
                    

   
                    |
19 | 13, 14, 18 | 3eqtri 2477 |
. . . . . 6
                                
    
      |
20 | | rniun 5246 |
. . . . . . 7
                                   |
21 | | iunxun 4363 |
. . . . . . 7
             
                         |
22 | | iunxun 4363 |
. . . . . . . 8
                         
    
     |
23 | 22 | uneq1i 3584 |
. . . . . . 7
 
                                              |
24 | 20, 21, 23 | 3eqtri 2477 |
. . . . . 6
                            
    
    
     |
25 | 19, 24 | uneq12i 3586 |
. . . . 5
 
                                                  
    
                                 |
26 | | uncom 3578 |
. . . . . . 7
 

   
                     
    
                   |
27 | 26 | uneq1i 3584 |
. . . . . 6
       
                     
    
                                                         
    
    
      |
28 | | un4 3594 |
. . . . . 6
            
    
    
                                                               
    
      
   

     |
29 | 27, 28 | eqtri 2473 |
. . . . 5
       
                     
    
                                                   
    
      
   

     |
30 | | uncom 3578 |
. . . . . . . 8
 
    
                       
    
     |
31 | 30 | uneq1i 3584 |
. . . . . . 7
                               
    
                
    
     
    
               |
32 | | un4 3594 |
. . . . . . 7
                               
    
                
    
     
    
               |
33 | 31, 32 | eqtri 2473 |
. . . . . 6
                               
    
                
    
     
    
               |
34 | 33 | uneq1i 3584 |
. . . . 5
            
    
     
    
               
                     
    
     
    
               
          |
35 | 25, 29, 34 | 3eqtri 2477 |
. . . 4
 
                                              
    
     
    
               
          |
36 | | df-ne 2624 |
. . . . . . . . . 10
     
       |
37 | | incom 3625 |
. . . . . . . . . . . . . . 15
           |
38 | 1 | ineq2i 3631 |
. . . . . . . . . . . . . . 15
              |
39 | | indi 3689 |
. . . . . . . . . . . . . . 15
                   |
40 | 37, 38, 39 | 3eqtri 2477 |
. . . . . . . . . . . . . 14
                |
41 | 40 | eqeq1i 2456 |
. . . . . . . . . . . . 13
     
            |
42 | | un00 3800 |
. . . . . . . . . . . . 13
          
            |
43 | | anor 492 |
. . . . . . . . . . . . 13
          
 
          |
44 | 41, 42, 43 | 3bitr2i 277 |
. . . . . . . . . . . 12
     
 
          |
45 | 44 | notbii 298 |
. . . . . . . . . . 11
     
            |
46 | | notnot 293 |
. . . . . . . . . . 11
          
            |
47 | | disjsn 4032 |
. . . . . . . . . . . . . 14
    
  |
48 | 47 | notbii 298 |
. . . . . . . . . . . . 13
       |
49 | | notnot 293 |
. . . . . . . . . . . . 13

  |
50 | 48, 49 | bitr4i 256 |
. . . . . . . . . . . 12
       |
51 | | disjsn 4032 |
. . . . . . . . . . . . . 14
    
  |
52 | 51 | notbii 298 |
. . . . . . . . . . . . 13
       |
53 | | notnot 293 |
. . . . . . . . . . . . 13

  |
54 | 52, 53 | bitr4i 256 |
. . . . . . . . . . . 12
       |
55 | 50, 54 | orbi12i 524 |
. . . . . . . . . . 11
          
    |
56 | 45, 46, 55 | 3bitr2i 277 |
. . . . . . . . . 10
     
    |
57 | 36, 56 | sylbb 201 |
. . . . . . . . 9
     
    |
58 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . 20
  
 
  |
59 | 58 | snssd 4117 |
. . . . . . . . . . . . . . . . . . 19
  
 
    |
60 | | df-ss 3418 |
. . . . . . . . . . . . . . . . . . 19
           |
61 | 59, 60 | sylib 200 |
. . . . . . . . . . . . . . . . . 18
  
 
        |
62 | 61 | iuneq1d 4303 |
. . . . . . . . . . . . . . . . 17
  
 
         
        |
63 | | c0ex 9637 |
. . . . . . . . . . . . . . . . . 18
 |
64 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . 19
         |
65 | 64 | dmeqd 5037 |
. . . . . . . . . . . . . . . . . 18
 
  
    |
66 | 63, 65 | iunxsn 4361 |
. . . . . . . . . . . . . . . . 17
    
  
   |
67 | 62, 66 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
  
 
         
    |
68 | | relexp0g 13085 |
. . . . . . . . . . . . . . . . . . 19
         |
69 | 68 | ad2antll 735 |
. . . . . . . . . . . . . . . . . 18
  
 
        |
70 | 69 | dmeqd 5037 |
. . . . . . . . . . . . . . . . 17
  
 
        |
71 | | dmresi 5160 |
. . . . . . . . . . . . . . . . 17
      |
72 | 70, 71 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
  
 
       |
73 | 67, 72 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
  
 
             |
74 | 61 | iuneq1d 4303 |
. . . . . . . . . . . . . . . . 17
  
 
         
        |
75 | 64 | rneqd 5062 |
. . . . . . . . . . . . . . . . . 18
 
  
    |
76 | 63, 75 | iunxsn 4361 |
. . . . . . . . . . . . . . . . 17
    
  
   |
77 | 74, 76 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
  
 
         
    |
78 | 69 | rneqd 5062 |
. . . . . . . . . . . . . . . . 17
  
 
        |
79 | | rnresi 5181 |
. . . . . . . . . . . . . . . . 17
      |
80 | 78, 79 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
  
 
       |
81 | 77, 80 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
  
 
             |
82 | 73, 81 | uneq12d 3589 |
. . . . . . . . . . . . . 14
  
 
 
    
                     |
83 | | unidm 3577 |
. . . . . . . . . . . . . 14
         |
84 | 82, 83 | syl6eq 2501 |
. . . . . . . . . . . . 13
  
 
 
    
                 |
85 | 84 | uneq1d 3587 |
. . . . . . . . . . . 12
  
 
  
                            
    
         
                     |
86 | | relexpdmg 13105 |
. . . . . . . . . . . . . . . . . . 19
 
        |
87 | 86 | expcom 437 |
. . . . . . . . . . . . . . . . . 18
          |
88 | 87 | ralrimiv 2800 |
. . . . . . . . . . . . . . . . 17
 
       |
89 | 88 | ad2antll 735 |
. . . . . . . . . . . . . . . 16
  
 

       |
90 | | olc 386 |
. . . . . . . . . . . . . . . . . . . . 21

      |
91 | 90 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . 20
  
 
      |
92 | | inss 3661 |
. . . . . . . . . . . . . . . . . . . 20
           |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
  
 
   
  |
94 | 93 | sseld 3431 |
. . . . . . . . . . . . . . . . . 18
  
 
    
   |
95 | 94 | imim1d 78 |
. . . . . . . . . . . . . . . . 17
  
 
            
         |
96 | 95 | ralimdv2 2795 |
. . . . . . . . . . . . . . . 16
  
 
 
     
             |
97 | 89, 96 | mpd 15 |
. . . . . . . . . . . . . . 15
  
 
             |
98 | | iunss 4319 |
. . . . . . . . . . . . . . 15
 
    
    
             |
99 | 97, 98 | sylibr 216 |
. . . . . . . . . . . . . 14
  
 
             |
100 | | relexprng 13109 |
. . . . . . . . . . . . . . . . . . 19
 
        |
101 | 100 | expcom 437 |
. . . . . . . . . . . . . . . . . 18
          |
102 | 101 | ralrimiv 2800 |
. . . . . . . . . . . . . . . . 17
 
       |
103 | 102 | ad2antll 735 |
. . . . . . . . . . . . . . . 16
  
 

       |
104 | 94 | imim1d 78 |
. . . . . . . . . . . . . . . . 17
  
 
            
         |
105 | 104 | ralimdv2 2795 |
. . . . . . . . . . . . . . . 16
  
 
 
     
             |
106 | 103, 105 | mpd 15 |
. . . . . . . . . . . . . . 15
  
 
             |
107 | | iunss 4319 |
. . . . . . . . . . . . . . 15
 
    
    
             |
108 | 106, 107 | sylibr 216 |
. . . . . . . . . . . . . 14
  
 
             |
109 | 99, 108 | unssd 3610 |
. . . . . . . . . . . . 13
  
 
 
    
                 |
110 | | ssequn2 3607 |
. . . . . . . . . . . . 13
                           
    
                  |
111 | 109, 110 | sylib 200 |
. . . . . . . . . . . 12
  
 
    
    
                  |
112 | 85, 111 | eqtrd 2485 |
. . . . . . . . . . 11
  
 
  
                            
    
         |
113 | 112 | ex 436 |
. . . . . . . . . 10
  
            
    
     
    
                   |
114 | | simpl 459 |
. . . . . . . . . . . . . . . . . . 19
  
 
  |
115 | 114 | snssd 4117 |
. . . . . . . . . . . . . . . . . 18
  
 
    |
116 | | df-ss 3418 |
. . . . . . . . . . . . . . . . . 18
           |
117 | 115, 116 | sylib 200 |
. . . . . . . . . . . . . . . . 17
  
 
        |
118 | 117 | iuneq1d 4303 |
. . . . . . . . . . . . . . . 16
  
 
         
        |
119 | | 1ex 9638 |
. . . . . . . . . . . . . . . . 17
 |
120 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18
         |
121 | 120 | dmeqd 5037 |
. . . . . . . . . . . . . . . . 17
 
  
    |
122 | 119, 121 | iunxsn 4361 |
. . . . . . . . . . . . . . . 16
    
  
   |
123 | 118, 122 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
  
 
         
    |
124 | | relexp1g 13089 |
. . . . . . . . . . . . . . . . 17
      |
125 | 124 | ad2antll 735 |
. . . . . . . . . . . . . . . 16
  
 
     |
126 | 125 | dmeqd 5037 |
. . . . . . . . . . . . . . 15
  
 
     |
127 | 123, 126 | eqtrd 2485 |
. . . . . . . . . . . . . 14
  
 
           |
128 | 117 | iuneq1d 4303 |
. . . . . . . . . . . . . . . 16
  
 
         
        |
129 | 120 | rneqd 5062 |
. . . . . . . . . . . . . . . . 17
 
  
    |
130 | 119, 129 | iunxsn 4361 |
. . . . . . . . . . . . . . . 16
    
  
   |
131 | 128, 130 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
  
 
         
    |
132 | 125 | rneqd 5062 |
. . . . . . . . . . . . . . 15
  
 
     |
133 | 131, 132 | eqtrd 2485 |
. . . . . . . . . . . . . 14
  
 
           |
134 | 127, 133 | uneq12d 3589 |
. . . . . . . . . . . . 13
  
 
 
    
                 |
135 | 134 | uneq2d 3588 |
. . . . . . . . . . . 12
  
 
  
                            
    
                
    
         |
136 | 88 | ad2antll 735 |
. . . . . . . . . . . . . . . 16
  
 

       |
137 | | olc 386 |
. . . . . . . . . . . . . . . . . . . . 21

      |
138 | 137 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . 20
  
 
      |
139 | | inss 3661 |
. . . . . . . . . . . . . . . . . . . 20
           |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
  
 
   
  |
141 | 140 | sseld 3431 |
. . . . . . . . . . . . . . . . . 18
  
 
    
   |
142 | 141 | imim1d 78 |
. . . . . . . . . . . . . . . . 17
  
 
            
         |
143 | 142 | ralimdv2 2795 |
. . . . . . . . . . . . . . . 16
  
 
 
     
             |
144 | 136, 143 | mpd 15 |
. . . . . . . . . . . . . . 15
  
 
             |
145 | | iunss 4319 |
. . . . . . . . . . . . . . 15
 
    
    
             |
146 | 144, 145 | sylibr 216 |
. . . . . . . . . . . . . 14
  
 
             |
147 | 102 | ad2antll 735 |
. . . . . . . . . . . . . . . 16
  
 

       |
148 | 141 | imim1d 78 |
. . . . . . . . . . . . . . . . 17
  
 
            
         |
149 | 148 | ralimdv2 2795 |
. . . . . . . . . . . . . . . 16
  
 
 
     
             |
150 | 147, 149 | mpd 15 |
. . . . . . . . . . . . . . 15
  
 
             |
151 | | iunss 4319 |
. . . . . . . . . . . . . . 15
 
    
    
             |
152 | 150, 151 | sylibr 216 |
. . . . . . . . . . . . . 14
  
 
             |
153 | 146, 152 | unssd 3610 |
. . . . . . . . . . . . 13
  
 
 
    
                 |
154 | | ssequn1 3604 |
. . . . . . . . . . . . 13
                         
    
                    |
155 | 153, 154 | sylib 200 |
. . . . . . . . . . . 12
  
 
  
                         |
156 | 135, 155 | eqtrd 2485 |
. . . . . . . . . . 11
  
 
  
                            
    
         |
157 | 156 | ex 436 |
. . . . . . . . . 10
  
            
    
     
    
                   |
158 | 113, 157 | jaoi 381 |
. . . . . . . . 9
 
   
  
                            
    
          |
159 | 57, 158 | syl 17 |
. . . . . . . 8
     
 
                                
    
          |
160 | 159 | 3impib 1206 |
. . . . . . 7
      
                                
    
         |
161 | 160 | 3com13 1213 |
. . . . . 6
 
                                     
    
         |
162 | 161 | uneq1d 3587 |
. . . . 5
 
                  
    
     
    
               
             
   

      |
163 | 88 | adantr 467 |
. . . . . . . . . 10
   
       |
164 | | ssel 3426 |
. . . . . . . . . . . . 13

    |
165 | 164 | adantl 468 |
. . . . . . . . . . . 12
       |
166 | 165 | imim1d 78 |
. . . . . . . . . . 11
    
      
         |
167 | 166 | ralimdv2 2795 |
. . . . . . . . . 10
         

        |
168 | 163, 167 | mpd 15 |
. . . . . . . . 9
   
       |
169 | | iunss 4319 |
. . . . . . . . 9
 

            |
170 | 168, 169 | sylibr 216 |
. . . . . . . 8
   
       |
171 | 102 | adantr 467 |
. . . . . . . . . 10
   
       |
172 | 165 | imim1d 78 |
. . . . . . . . . . 11
    
      
         |
173 | 172 | ralimdv2 2795 |
. . . . . . . . . 10
         

        |
174 | 171, 173 | mpd 15 |
. . . . . . . . 9
   
       |
175 | | iunss 4319 |
. . . . . . . . 9
 

            |
176 | 174, 175 | sylibr 216 |
. . . . . . . 8
   
       |
177 | 170, 176 | unssd 3610 |
. . . . . . 7
        

       |
178 | 177 | 3adant3 1028 |
. . . . . 6
 
       
   

       |
179 | | ssequn2 3607 |
. . . . . 6
      

         

  

        |
180 | 178, 179 | sylib 200 |
. . . . 5
 
       
  
   

        |
181 | 162, 180 | eqtrd 2485 |
. . . 4
 
                  
    
     
    
               
             |
182 | 35, 181 | syl5eq 2497 |
. . 3
 
                                              |
183 | | nn0ex 10875 |
. . . . . . 7
 |
184 | 183 | ssex 4547 |
. . . . . 6

  |
185 | | incom 3625 |
. . . . . . . . . 10
         |
186 | | inex1g 4546 |
. . . . . . . . . 10
       |
187 | 185, 186 | syl5eqelr 2534 |
. . . . . . . . 9
       |
188 | | incom 3625 |
. . . . . . . . . 10
         |
189 | | inex1g 4546 |
. . . . . . . . . 10
       |
190 | 188, 189 | syl5eqelr 2534 |
. . . . . . . . 9
       |
191 | | unexg 6592 |
. . . . . . . . 9
     
                 |
192 | 187, 190,
191 | syl2anc 667 |
. . . . . . . 8
             |
193 | | unexg 6592 |
. . . . . . . 8
           
               |
194 | 192, 193 | mpancom 675 |
. . . . . . 7
               |
195 | | ovex 6318 |
. . . . . . . 8
    |
196 | 195 | rgenw 2749 |
. . . . . . 7
                  |
197 | | iunexg 6769 |
. . . . . . 7
                                                   |
198 | 194, 196,
197 | sylancl 668 |
. . . . . 6
                    |
199 | 184, 198 | syl 17 |
. . . . 5

                   |
200 | 199 | 3ad2ant2 1030 |
. . . 4
 
                         |
201 | | simp1 1008 |
. . . 4
 
        |
202 | | relexp0eq 36293 |
. . . 4
                      
                                                              |
203 | 200, 201,
202 | syl2anc 667 |
. . 3
 
       
                                    
 
                        |
204 | 182, 203 | mpbid 214 |
. 2
 
       
                       |
205 | 12, 204 | syl5eq 2497 |
1
 
       

         |