Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
    
      |
2 | | filunibas 20974 |
. . . 4
    
   |
3 | 2 | fveq2d 5883 |
. . 3
    
           |
4 | 1, 3 | eleqtrrd 2552 |
. 2
    
       |
5 | | nss 3476 |
. . . . . . . 8

 
        |
6 | | simpll 768 |
. . . . . . . . . . . 12
       

    
   
       |
7 | | ssel2 3413 |
. . . . . . . . . . . . . . . . 17
 
   
       |
8 | 7 | adantll 728 |
. . . . . . . . . . . . . . . 16
       

           |
9 | | elun 3565 |
. . . . . . . . . . . . . . . 16
    

     |
10 | 8, 9 | sylib 201 |
. . . . . . . . . . . . . . 15
       

     
     |
11 | 10 | orcomd 395 |
. . . . . . . . . . . . . 14
       

           |
12 | 11 | ord 384 |
. . . . . . . . . . . . 13
       

     
     |
13 | 12 | impr 631 |
. . . . . . . . . . . 12
       

    
   
  |
14 | | uniss 4211 |
. . . . . . . . . . . . . 14
             |
15 | 14 | ad2antlr 741 |
. . . . . . . . . . . . 13
       

    
   
        |
16 | | uniun 4209 |
. . . . . . . . . . . . . 14
 
          |
17 | | 0ex 4528 |
. . . . . . . . . . . . . . . 16
 |
18 | 17 | unisn 4205 |
. . . . . . . . . . . . . . 15
    |
19 | 18 | uneq2i 3576 |
. . . . . . . . . . . . . 14
 
     
  |
20 | | un0 3762 |
. . . . . . . . . . . . . 14
 
   |
21 | 16, 19, 20 | 3eqtrri 2498 |
. . . . . . . . . . . . 13
       |
22 | 15, 21 | syl6sseqr 3465 |
. . . . . . . . . . . 12
       

    
   
    |
23 | | elssuni 4219 |
. . . . . . . . . . . . 13
    |
24 | 23 | ad2antrl 742 |
. . . . . . . . . . . 12
       

    
   
   |
25 | | filss 20946 |
. . . . . . . . . . . 12
         
      |
26 | 6, 13, 22, 24, 25 | syl13anc 1294 |
. . . . . . . . . . 11
       

    
   
   |
27 | | elun1 3592 |
. . . . . . . . . . 11
 
       |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
       

    
   
       |
29 | 28 | ex 441 |
. . . . . . . . 9
                 

      |
30 | 29 | exlimdv 1787 |
. . . . . . . 8
               
  
        |
31 | 5, 30 | syl5bi 225 |
. . . . . . 7
              
        |
32 | | uni0b 4215 |
. . . . . . . 8
 
    |
33 | | ssun2 3589 |
. . . . . . . . . 10
       |
34 | 17 | snid 3988 |
. . . . . . . . . 10
   |
35 | 33, 34 | sselii 3415 |
. . . . . . . . 9
     |
36 | | eleq1 2537 |
. . . . . . . . 9
 
 

          |
37 | 35, 36 | mpbiri 241 |
. . . . . . . 8
 
       |
38 | 32, 37 | sylbir 218 |
. . . . . . 7
          |
39 | 31, 38 | pm2.61d2 165 |
. . . . . 6
            

     |
40 | 39 | ex 441 |
. . . . 5
      
    

      |
41 | 40 | alrimiv 1781 |
. . . 4
         
           |
42 | | filin 20947 |
. . . . . . . . . 10
      
     |
43 | | elun1 3592 |
. . . . . . . . . 10
   
       |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
      
         |
45 | 44 | 3expa 1231 |
. . . . . . . 8
       
  
       |
46 | 45 | ralrimiva 2809 |
. . . . . . 7
      
  
       |
47 | | elsni 3985 |
. . . . . . . . 9
     |
48 | | ineq2 3619 |
. . . . . . . . . . 11

      |
49 | | in0 3763 |
. . . . . . . . . . 11
   |
50 | 48, 49 | syl6eq 2521 |
. . . . . . . . . 10

    |
51 | 50, 35 | syl6eqel 2557 |
. . . . . . . . 9

        |
52 | 47, 51 | syl 17 |
. . . . . . . 8
           |
53 | 52 | rgen 2766 |
. . . . . . 7
          |
54 | | ralun 3607 |
. . . . . . 7
   
               

            |
55 | 46, 53, 54 | sylancl 675 |
. . . . . 6
      
               |
56 | 55 | ralrimiva 2809 |
. . . . 5
      
              |
57 | | elsni 3985 |
. . . . . . 7
     |
58 | | ineq1 3618 |
. . . . . . . . . 10

  
   |
59 | | 0ss 3766 |
. . . . . . . . . . 11
 |
60 | | df-ss 3404 |
. . . . . . . . . . 11
     |
61 | 59, 60 | mpbi 213 |
. . . . . . . . . 10
   |
62 | 58, 61 | syl6eq 2521 |
. . . . . . . . 9

    |
63 | 62, 35 | syl6eqel 2557 |
. . . . . . . 8

        |
64 | 63 | ralrimivw 2810 |
. . . . . . 7

              |
65 | 57, 64 | syl 17 |
. . . . . 6
                 |
66 | 65 | rgen 2766 |
. . . . 5
                 |
67 | | ralun 3607 |
. . . . 5
   

                           

                  |
68 | 56, 66, 67 | sylancl 675 |
. . . 4
                          |
69 | | p0ex 4588 |
. . . . . 6
   |
70 | | unexg 6611 |
. . . . . 6
        
       |
71 | 69, 70 | mpan2 685 |
. . . . 5
      
     |
72 | | istopg 20002 |
. . . . 5
              
  
                            |
73 | 71, 72 | syl 17 |
. . . 4
               
  
                            |
74 | 41, 68, 73 | mpbir2and 936 |
. . 3
      
     |
75 | 21 | cldopn 20123 |
. . . . . . . 8
    
   
         |
76 | | elun 3565 |
. . . . . . . 8
                    |
77 | 75, 76 | sylib 201 |
. . . . . . 7
    
   
  
         |
78 | | elun 3565 |
. . . . . . . . . 10
    

     |
79 | | filfbas 20941 |
. . . . . . . . . . . . . 14
             |
80 | | fbncp 20932 |
. . . . . . . . . . . . . 14
      
      |
81 | 79, 80 | sylan 479 |
. . . . . . . . . . . . 13
      
      |
82 | 81 | pm2.21d 109 |
. . . . . . . . . . . 12
      
        |
83 | 82 | ex 441 |
. . . . . . . . . . 11
               |
84 | 57 | a1d 25 |
. . . . . . . . . . . 12
          |
85 | 84 | a1i 11 |
. . . . . . . . . . 11
            
    |
86 | 83, 85 | jaod 387 |
. . . . . . . . . 10
       
  
  

    |
87 | 78, 86 | syl5bi 225 |
. . . . . . . . 9
              
    |
88 | 87 | imp 436 |
. . . . . . . 8
      
        
   |
89 | | elsni 3985 |
. . . . . . . . 9
           |
90 | | elssuni 4219 |
. . . . . . . . . . . 12
            |
91 | 90, 21 | syl6sseqr 3465 |
. . . . . . . . . . 11
        |
92 | 91 | adantl 473 |
. . . . . . . . . 10
      
        |
93 | | ssdif0 3741 |
. . . . . . . . . . 11
 
     |
94 | 93 | biimpri 211 |
. . . . . . . . . 10
       |
95 | | eqss 3433 |
. . . . . . . . . . 11
 
      |
96 | 95 | simplbi2 637 |
. . . . . . . . . 10
   
    |
97 | 92, 94, 96 | syl2im 38 |
. . . . . . . . 9
      
             |
98 | 89, 97 | syl5 32 |
. . . . . . . 8
      
               |
99 | 88, 98 | orim12d 856 |
. . . . . . 7
      
               
      |
100 | 77, 99 | syl5 32 |
. . . . . 6
      
         
   
      |
101 | 100 | expimpd 614 |
. . . . 5
               
           |
102 | | elin 3608 |
. . . . 5
         
    
        
       |
103 | | vex 3034 |
. . . . . 6
 |
104 | 103 | elpr 3977 |
. . . . 5
    
     |
105 | 101, 102,
104 | 3imtr4g 278 |
. . . 4
                            |
106 | 105 | ssrdv 3424 |
. . 3
                          |
107 | 21 | iscon2 20506 |
. . 3
    
 
                        |
108 | 74, 106, 107 | sylanbrc 677 |
. 2
      
     |
109 | 4, 108 | syl 17 |
1
    
      |