Step | Hyp | Ref
| Expression |
1 | | ssel 3428 |
. . . . . . . . . . . . 13
                   
                     |
2 | | elun 3576 |
. . . . . . . . . . . . . . 15
                  
                    |
3 | | sseq2 3456 |
. . . . . . . . . . . . . . . . . 18
 
   |
4 | | pweq 3956 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
5 | 4 | ineq1d 3635 |
. . . . . . . . . . . . . . . . . . 19
  
      |
6 | 5 | raleqdv 2995 |
. . . . . . . . . . . . . . . . . 18
  
 

         |
7 | 3, 6 | anbi12d 718 |
. . . . . . . . . . . . . . . . 17
        
          |
8 | 7 | elrab 3198 |
. . . . . . . . . . . . . . . 16
       
   
  
      
   
     |
9 | | elsn 3984 |
. . . . . . . . . . . . . . . 16
  
  |
10 | 8, 9 | orbi12i 524 |
. . . . . . . . . . . . . . 15
               
          
   
      |
11 | 2, 10 | bitri 253 |
. . . . . . . . . . . . . 14
                  
                  |
12 | | elpwi 3962 |
. . . . . . . . . . . . . . . 16
            |
13 | 12 | adantr 467 |
. . . . . . . . . . . . . . 15
                     |
14 | | 0ss 3765 |
. . . . . . . . . . . . . . . 16
     |
15 | | sseq1 3455 |
. . . . . . . . . . . . . . . 16

    
       |
16 | 14, 15 | mpbiri 237 |
. . . . . . . . . . . . . . 15

      |
17 | 13, 16 | jaoi 381 |
. . . . . . . . . . . . . 14
                       |
18 | 11, 17 | sylbi 199 |
. . . . . . . . . . . . 13
                         |
19 | 1, 18 | syl6 34 |
. . . . . . . . . . . 12
                           |
20 | 19 | ralrimiv 2802 |
. . . . . . . . . . 11
                   
      |
21 | | unissb 4232 |
. . . . . . . . . . 11
     

      |
22 | 20, 21 | sylibr 216 |
. . . . . . . . . 10
                          |
23 | 22 | adantr 467 |
. . . . . . . . 9
 
                  [ ] 
       |
24 | 23 | ad2antlr 734 |
. . . . . . . 8
                 
 
 
 
      
    
        
   
      [ ]     
      |
25 | | vex 3050 |
. . . . . . . . . 10
 |
26 | 25 | uniex 6592 |
. . . . . . . . 9
  |
27 | 26 | elpw 3959 |
. . . . . . . 8
 
    
       |
28 | 24, 27 | sylibr 216 |
. . . . . . 7
                 
 
 
 
      
    
        
   
      [ ]     
       |
29 | | uni0b 4226 |
. . . . . . . . . 10
 
    |
30 | 29 | notbii 298 |
. . . . . . . . 9
      |
31 | | disjssun 3824 |
. . . . . . . . . . . . 13
                
                  
     |
32 | 31 | biimpcd 228 |
. . . . . . . . . . . 12
                                   
     |
33 | 32 | necon3bd 2640 |
. . . . . . . . . . 11
                   
                     |
34 | | n0 3743 |
. . . . . . . . . . . 12
                                    |
35 | | elin 3619 |
. . . . . . . . . . . . . . 15
                                   |
36 | 8 | anbi2i 701 |
. . . . . . . . . . . . . . 15
 
      
   
           
   
      |
37 | 35, 36 | bitri 253 |
. . . . . . . . . . . . . 14
                                   |
38 | | simprrl 775 |
. . . . . . . . . . . . . . 15
  
             
  |
39 | | simpl 459 |
. . . . . . . . . . . . . . 15
  
             
  |
40 | | ssuni 4223 |
. . . . . . . . . . . . . . 15
 

   |
41 | 38, 39, 40 | syl2anc 667 |
. . . . . . . . . . . . . 14
  
             
   |
42 | 37, 41 | sylbi 199 |
. . . . . . . . . . . . 13
                
   |
43 | 42 | exlimiv 1778 |
. . . . . . . . . . . 12
                     |
44 | 34, 43 | sylbi 199 |
. . . . . . . . . . 11
                
   |
45 | 33, 44 | syl6 34 |
. . . . . . . . . 10
                   
      |
46 | 45 | ad2antrl 735 |
. . . . . . . . 9
                    
           
  
                  [ ]   
      |
47 | 30, 46 | syl5bi 221 |
. . . . . . . 8
                    
           
  
                  [ ]    
    |
48 | 47 | imp 431 |
. . . . . . 7
                 
 
 
 
      
    
        
   
      [ ]    
   |
49 | | elfpw 7881 |
. . . . . . . . . 10
    
     |
50 | | unieq 4209 |
. . . . . . . . . . . . . . . . . . . 20

    |
51 | | uni0 4228 |
. . . . . . . . . . . . . . . . . . . 20
  |
52 | 50, 51 | syl6eq 2503 |
. . . . . . . . . . . . . . . . . . 19

   |
53 | 52 | necon3bi 2652 |
. . . . . . . . . . . . . . . . . 18
    |
54 | 53 | adantr 467 |
. . . . . . . . . . . . . . . . 17
      |
55 | 54 | ad2antrl 735 |
. . . . . . . . . . . . . . . 16
                 
 
 
 
      
    
        
   
      [ ]            |
56 | | simplrr 772 |
. . . . . . . . . . . . . . . 16
                 
 
 
 
      
    
        
   
      [ ]          [ ]   |
57 | | simprlr 774 |
. . . . . . . . . . . . . . . 16
                 
 
 
 
      
    
        
   
      [ ]            |
58 | | simprr 767 |
. . . . . . . . . . . . . . . 16
                 
 
 
 
      
    
        
   
      [ ]             |
59 | | finsschain 7886 |
. . . . . . . . . . . . . . . 16
   [ ] 
    
  |
60 | 55, 56, 57, 58, 59 | syl22anc 1270 |
. . . . . . . . . . . . . . 15
                 
 
 
 
      
    
        
   
      [ ]          
  |
61 | 60 | expr 620 |
. . . . . . . . . . . . . 14
                 
 
 
 
      
    
        
   
      [ ]      
  
   |
62 | | 0elpw 4575 |
. . . . . . . . . . . . . . . . . . . . 21
  |
63 | | 0fin 7804 |
. . . . . . . . . . . . . . . . . . . . 21
 |
64 | | elin 3619 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
65 | 62, 63, 64 | mpbir2an 932 |
. . . . . . . . . . . . . . . . . . . 20
    |
66 | | unieq 4209 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
67 | 66 | eqeq2d 2463 |
. . . . . . . . . . . . . . . . . . . . . 22

 
    |
68 | 67 | notbid 296 |
. . . . . . . . . . . . . . . . . . . . 21

      |
69 | 68 | rspccv 3149 |
. . . . . . . . . . . . . . . . . . . 20
 
    
 
     |
70 | 65, 69 | mpi 20 |
. . . . . . . . . . . . . . . . . . 19
 
       |
71 | | vex 3050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
72 | 71 | elpw 3959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  |
73 | | elin 3619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
     |
74 | | unieq 4209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
75 | 74 | eqeq2d 2463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
     |
76 | 75 | notbid 296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
     |
77 | 76 | rspccv 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       
    |
78 | 73, 77 | syl5bir 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
       
    |
79 | 78 | expd 438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
      
     |
80 | 72, 79 | syl5bir 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
           |
81 | 80 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
           |
82 | 81 | ad2antll 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                      |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  
      |
84 | | sseq2 3456 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26


   |
85 | | ss0 3767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
86 | 84, 85 | syl6bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

    |
87 | | unieq 4209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

    |
88 | 87 | eqeq2d 2463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

 
    |
89 | 88 | notbid 296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

      |
90 | 89 | biimprcd 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
    |
91 | 90 | a1dd 47 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
92 | 86, 91 | syl9r 74 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
       |
93 | 92 | com34 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
      |
94 | 83, 93 | jaod 382 |
. . . . . . . . . . . . . . . . . . . . . 22
          
   
            |
95 | 11, 94 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . . 21
                      
      |
96 | 1, 95 | sylan9r 664 |
. . . . . . . . . . . . . . . . . . . 20
                     

 
      |
97 | 96 | com23 81 |
. . . . . . . . . . . . . . . . . . 19
                     



      |
98 | 70, 97 | sylan 474 |
. . . . . . . . . . . . . . . . . 18
                         



      |
99 | 98 | ad2ant2lr 755 |
. . . . . . . . . . . . . . . . 17
                    
           
  
                  [ ]            |
100 | 99 | imp 431 |
. . . . . . . . . . . . . . . 16
                 
 
 
 
      
    
        
   
      [ ]           |
101 | 100 | adantrl 723 |
. . . . . . . . . . . . . . 15
                 
 
 
 
      
    
        
   
      [ ]      


     |
102 | 101 | rexlimdv 2879 |
. . . . . . . . . . . . . 14
                 
 
 
 
      
    
        
   
      [ ]      
 
    |
103 | 61, 102 | syld 45 |
. . . . . . . . . . . . 13
                 
 
 
 
      
    
        
   
      [ ]      
 
    |
104 | 103 | expr 620 |
. . . . . . . . . . . 12
                 
 
 
 
      
    
        
   
      [ ]             |
105 | 104 | com23 81 |
. . . . . . . . . . 11
                 
 
 
 
      
    
        
   
      [ ]             |
106 | 105 | impd 433 |
. . . . . . . . . 10
                 
 
 
 
      
    
        
   
      [ ]        
    |
107 | 49, 106 | syl5bi 221 |
. . . . . . . . 9
                 
 
 
 
      
    
        
   
      [ ]         
    |
108 | 107 | ralrimiv 2802 |
. . . . . . . 8
                 
 
 
 
      
    
        
   
      [ ]     
       |
109 | | unieq 4209 |
. . . . . . . . . . 11
     |
110 | 109 | eqeq2d 2463 |
. . . . . . . . . 10
 
     |
111 | 110 | notbid 296 |
. . . . . . . . 9
 
     |
112 | 111 | cbvralv 3021 |
. . . . . . . 8
 
   
         |
113 | 108, 112 | sylib 200 |
. . . . . . 7
                 
 
 
 
      
    
        
   
      [ ]     
       |
114 | 28, 48, 113 | jca32 538 |
. . . . . 6
                 
 
 
 
      
    
        
   
      [ ]            
           |
115 | 114 | ex 436 |
. . . . 5
                    
           
  
                  [ ]            
            |
116 | | orcom 389 |
. . . . . 6
                                           |
117 | 26 | elsnc 3994 |
. . . . . . . 8
 
 
   |
118 | | sseq2 3456 |
. . . . . . . . . 10
       |
119 | | pweq 3956 |
. . . . . . . . . . . 12
  
    |
120 | 119 | ineq1d 3635 |
. . . . . . . . . . 11
           |
121 | 120 | raleqdv 2995 |
. . . . . . . . . 10
       
         |
122 | 118, 121 | anbi12d 718 |
. . . . . . . . 9
         
  
   
     |
123 | 122 | elrab 3198 |
. . . . . . . 8
 
      
   
  
 
                 |
124 | 117, 123 | orbi12i 524 |
. . . . . . 7
                        
                  |
125 | | df-or 372 |
. . . . . . 7
          
           
 
                  |
126 | 124, 125 | bitr2i 254 |
. . . . . 6
          
              
      
   
      |
127 | | elun 3576 |
. . . . . 6
 
                 
 
      
   
         |
128 | 116, 126,
127 | 3bitr4i 281 |
. . . . 5
          
                               |
129 | 115, 128 | sylib 200 |
. . . 4
                    
           
  
                  [ ]           
   
        |
130 | 129 | ex 436 |
. . 3
                   
           
                      [ ]

        
   
         |
131 | 130 | alrimiv 1775 |
. 2
                   
           
                        [ ]

        
   
         |
132 | | fvex 5880 |
. . . . . 6
     |
133 | 132 | pwex 4589 |
. . . . 5
      |
134 | 133 | rabex 4557 |
. . . 4
               |
135 | | p0ex 4593 |
. . . 4
   |
136 | 134, 135 | unex 6594 |
. . 3
                   |
137 | 136 | zorn 8942 |
. 2
                       [ ] 
        
   
       
                                        |
138 | 131, 137 | syl 17 |
1
                   
           
          
   
               
   
        |