Step | Hyp | Ref
| Expression |
1 | | uniss 4219 |
. . . . . . 7
     |
2 | 1 | adantl 468 |
. . . . . 6
 
     |
3 | | neiptop.o |
. . . . . . . 8
 

      |
4 | | neiptop.0 |
. . . . . . . 8
         |
5 | | neiptop.1 |
. . . . . . . 8
   


           |
6 | | neiptop.2 |
. . . . . . . 8
 
               |
7 | | neiptop.3 |
. . . . . . . 8
           |
8 | | neiptop.4 |
. . . . . . . 8
                      |
9 | | neiptop.5 |
. . . . . . . 8
 
       |
10 | 3, 4, 5, 6, 7, 8, 9 | neiptopuni 20146 |
. . . . . . 7
    |
11 | 10 | adantr 467 |
. . . . . 6
 
    |
12 | 2, 11 | sseqtr4d 3469 |
. . . . 5
 
    |
13 | | simp-4l 776 |
. . . . . . . . . 10
    

 
    |
14 | 12 | ad3antrrr 736 |
. . . . . . . . . . 11
    

 
     |
15 | | simpllr 769 |
. . . . . . . . . . 11
    

 
     |
16 | 14, 15 | sseldd 3433 |
. . . . . . . . . 10
    

 
    |
17 | 13, 16 | jca 535 |
. . . . . . . . 9
    

 
      |
18 | | elssuni 4227 |
. . . . . . . . . 10
    |
19 | 18 | ad2antlr 733 |
. . . . . . . . 9
    

 
     |
20 | 17, 19, 14 | 3jca 1188 |
. . . . . . . 8
    

 
   
      |
21 | | simpr 463 |
. . . . . . . . . . . 12
 
   |
22 | 21 | sselda 3432 |
. . . . . . . . . . 11
       |
23 | 3 | neipeltop 20145 |
. . . . . . . . . . . 12

 
       |
24 | 23 | simprbi 466 |
. . . . . . . . . . 11
 
      |
25 | 22, 24 | syl 17 |
. . . . . . . . . 10
     
      |
26 | 25 | r19.21bi 2757 |
. . . . . . . . 9
    


      |
27 | 26 | adantllr 725 |
. . . . . . . 8
    

 
        |
28 | | sseq1 3453 |
. . . . . . . . . . . . . 14
 
     |
29 | 28 | 3anbi2d 1344 |
. . . . . . . . . . . . 13
   

            |
30 | | eleq1 2517 |
. . . . . . . . . . . . 13
     
       |
31 | 29, 30 | anbi12d 717 |
. . . . . . . . . . . 12
        
       
   
        |
32 | 31 | imbi1d 319 |
. . . . . . . . . . 11
     
   
     
            
     
        |
33 | 32 | imbi2d 318 |
. . . . . . . . . 10
        
   
     
     
  
   

  
    
          |
34 | | ssid 3451 |
. . . . . . . . . . . . . . . . 17
 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . 16

  |
36 | 9 | ralrimiva 2802 |
. . . . . . . . . . . . . . . 16
 
      |
37 | 3 | neipeltop 20145 |
. . . . . . . . . . . . . . . 16

 
       |
38 | 35, 36, 37 | sylanbrc 670 |
. . . . . . . . . . . . . . 15
   |
39 | | pwexg 4587 |
. . . . . . . . . . . . . . 15
 
  |
40 | | rabexg 4553 |
. . . . . . . . . . . . . . 15
            |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . . . . . . 14
  

       |
42 | 3, 41 | syl5eqel 2533 |
. . . . . . . . . . . . 13
   |
43 | 42 | adantr 467 |
. . . . . . . . . . . 12
 
   |
44 | 43, 21 | ssexd 4550 |
. . . . . . . . . . 11
 
   |
45 | | uniexg 6588 |
. . . . . . . . . . 11
    |
46 | | sseq2 3454 |
. . . . . . . . . . . . . . 15
       |
47 | | sseq1 3453 |
. . . . . . . . . . . . . . 15
   
   |
48 | 46, 47 | 3anbi23d 1342 |
. . . . . . . . . . . . . 14
     
  

      |
49 | 48 | anbi1d 711 |
. . . . . . . . . . . . 13
     
      
  
   
        |
50 | | eleq1 2517 |
. . . . . . . . . . . . 13
       
       |
51 | 49, 50 | imbi12d 322 |
. . . . . . . . . . . 12
                  
   

  
    
         |
52 | 51, 5 | vtoclg 3107 |
. . . . . . . . . . 11
 
       
    
        |
53 | 44, 45, 52 | 3syl 18 |
. . . . . . . . . 10
 
        
    
        |
54 | 33, 53 | chvarv 2107 |
. . . . . . . . 9
 
        
    
        |
55 | 54 | ad3antrrr 736 |
. . . . . . . 8
    

 
         
    
        |
56 | 20, 27, 55 | mp2and 685 |
. . . . . . 7
    

 
         |
57 | | simpr 463 |
. . . . . . . 8
     
   |
58 | | eluni2 4202 |
. . . . . . . 8
 

  |
59 | 57, 58 | sylib 200 |
. . . . . . 7
      
  |
60 | 56, 59 | r19.29a 2932 |
. . . . . 6
      
      |
61 | 60 | ralrimiva 2802 |
. . . . 5
 
           |
62 | 3 | neipeltop 20145 |
. . . . 5
 
  
  
       |
63 | 12, 61, 62 | sylanbrc 670 |
. . . 4
 
    |
64 | 63 | ex 436 |
. . 3
      |
65 | 64 | alrimiv 1773 |
. 2
        |
66 | | inss1 3652 |
. . . . . 6
   |
67 | 3 | neipeltop 20145 |
. . . . . . . 8

 
       |
68 | 67 | simplbi 462 |
. . . . . . 7
   |
69 | 68 | ad2antlr 733 |
. . . . . 6
       |
70 | 66, 69 | syl5ss 3443 |
. . . . 5
     
   |
71 | | simplll 768 |
. . . . . . . 8
   


     |
72 | | simpllr 769 |
. . . . . . . . . 10
   


     |
73 | 72, 68 | syl 17 |
. . . . . . . . 9
   


     |
74 | | simpr 463 |
. . . . . . . . . 10
   


       |
75 | 66, 74 | sseldi 3430 |
. . . . . . . . 9
   


     |
76 | 73, 75 | sseldd 3433 |
. . . . . . . 8
   


     |
77 | 71, 76, 6 | syl2anc 667 |
. . . . . . 7
   


                 |
78 | 67 | simprbi 466 |
. . . . . . . . . 10
 
      |
79 | 78 | r19.21bi 2757 |
. . . . . . . . 9
 
       |
80 | 72, 75, 79 | syl2anc 667 |
. . . . . . . 8
   


         |
81 | | simplr 762 |
. . . . . . . . 9
   


     |
82 | | inss2 3653 |
. . . . . . . . . 10
   |
83 | 82, 74 | sseldi 3430 |
. . . . . . . . 9
   


     |
84 | 3 | neipeltop 20145 |
. . . . . . . . . . 11

 
       |
85 | 84 | simprbi 466 |
. . . . . . . . . 10
 
      |
86 | 85 | r19.21bi 2757 |
. . . . . . . . 9
 
       |
87 | 81, 83, 86 | syl2anc 667 |
. . . . . . . 8
   


         |
88 | | fvex 5875 |
. . . . . . . . 9
     |
89 | | inelfi 7932 |
. . . . . . . . 9
     
         
           |
90 | 88, 89 | mp3an1 1351 |
. . . . . . . 8
     
                 |
91 | 80, 87, 90 | syl2anc 667 |
. . . . . . 7
   


   
           |
92 | 77, 91 | sseldd 3433 |
. . . . . 6
   


   
       |
93 | 92 | ralrimiva 2802 |
. . . . 5
                 |
94 | 3 | neipeltop 20145 |
. . . . 5
  
 
              |
95 | 70, 93, 94 | sylanbrc 670 |
. . . 4
     
   |
96 | 95 | ralrimiva 2802 |
. . 3
 
 
    |
97 | 96 | ralrimiva 2802 |
. 2
  
    |
98 | | istopg 19925 |
. . 3
 
     


      |
99 | 42, 98 | syl 17 |
. 2
       


      |
100 | 65, 97, 99 | mpbir2and 933 |
1
   |