Step | Hyp | Ref
| Expression |
1 | | uniss 4211 |
. . . . . . 7
     |
2 | 1 | adantl 473 |
. . . . . 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 20223 |
. . . . . . 7
    |
11 | 10 | adantr 472 |
. . . . . 6
 
    |
12 | 2, 11 | sseqtr4d 3455 |
. . . . 5
 
    |
13 | | simp-4l 784 |
. . . . . . . . . 10
    

 
    |
14 | 12 | ad3antrrr 744 |
. . . . . . . . . . 11
    

 
     |
15 | | simpllr 777 |
. . . . . . . . . . 11
    

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

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

 
      |
18 | | elssuni 4219 |
. . . . . . . . . 10
    |
19 | 18 | ad2antlr 741 |
. . . . . . . . 9
    

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

 
   
      |
21 | | simpr 468 |
. . . . . . . . . . . 12
 
   |
22 | 21 | sselda 3418 |
. . . . . . . . . . 11
       |
23 | 3 | neipeltop 20222 |
. . . . . . . . . . . 12

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


      |
27 | 26 | adantllr 733 |
. . . . . . . 8
    

 
        |
28 | | sseq1 3439 |
. . . . . . . . . . . . . 14
 
     |
29 | 28 | 3anbi2d 1370 |
. . . . . . . . . . . . 13
   

            |
30 | | eleq1 2537 |
. . . . . . . . . . . . 13
     
       |
31 | 29, 30 | anbi12d 725 |
. . . . . . . . . . . 12
        
       
   
        |
32 | 31 | imbi1d 324 |
. . . . . . . . . . 11
     
   
     
            
     
        |
33 | 32 | imbi2d 323 |
. . . . . . . . . 10
        
   
     
     
  
   

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

  |
36 | 9 | ralrimiva 2809 |
. . . . . . . . . . . . . . . 16
 
      |
37 | 3 | neipeltop 20222 |
. . . . . . . . . . . . . . . 16

 
       |
38 | 35, 36, 37 | sylanbrc 677 |
. . . . . . . . . . . . . . 15
   |
39 | | pwexg 4585 |
. . . . . . . . . . . . . . 15
 
  |
40 | | rabexg 4549 |
. . . . . . . . . . . . . . 15
            |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . . . . . . 14
  

       |
42 | 3, 41 | syl5eqel 2553 |
. . . . . . . . . . . . 13
   |
43 | 42 | adantr 472 |
. . . . . . . . . . . 12
 
   |
44 | 43, 21 | ssexd 4543 |
. . . . . . . . . . 11
 
   |
45 | | uniexg 6607 |
. . . . . . . . . . 11
    |
46 | | sseq2 3440 |
. . . . . . . . . . . . . . 15
       |
47 | | sseq1 3439 |
. . . . . . . . . . . . . . 15
   
   |
48 | 46, 47 | 3anbi23d 1368 |
. . . . . . . . . . . . . 14
     
  

      |
49 | 48 | anbi1d 719 |
. . . . . . . . . . . . 13
     
      
  
   
        |
50 | | eleq1 2537 |
. . . . . . . . . . . . 13
       
       |
51 | 49, 50 | imbi12d 327 |
. . . . . . . . . . . 12
                  
   

  
    
         |
52 | 51, 5 | vtoclg 3093 |
. . . . . . . . . . 11
 
       
    
        |
53 | 44, 45, 52 | 3syl 18 |
. . . . . . . . . 10
 
        
    
        |
54 | 33, 53 | chvarv 2120 |
. . . . . . . . 9
 
        
    
        |
55 | 54 | ad3antrrr 744 |
. . . . . . . 8
    

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

 
         |
57 | | simpr 468 |
. . . . . . . 8
     
   |
58 | | eluni2 4194 |
. . . . . . . 8
 

  |
59 | 57, 58 | sylib 201 |
. . . . . . 7
      
  |
60 | 56, 59 | r19.29a 2918 |
. . . . . 6
      
      |
61 | 60 | ralrimiva 2809 |
. . . . 5
 
           |
62 | 3 | neipeltop 20222 |
. . . . 5
 
  
  
       |
63 | 12, 61, 62 | sylanbrc 677 |
. . . 4
 
    |
64 | 63 | ex 441 |
. . 3
      |
65 | 64 | alrimiv 1781 |
. 2
        |
66 | | inss1 3643 |
. . . . . 6
   |
67 | 3 | neipeltop 20222 |
. . . . . . . 8

 
       |
68 | 67 | simplbi 467 |
. . . . . . 7
   |
69 | 68 | ad2antlr 741 |
. . . . . 6
       |
70 | 66, 69 | syl5ss 3429 |
. . . . 5
     
   |
71 | | simplll 776 |
. . . . . . . 8
   


     |
72 | | simpllr 777 |
. . . . . . . . . 10
   


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


     |
74 | | simpr 468 |
. . . . . . . . . 10
   


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


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


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


                 |
78 | 67 | simprbi 471 |
. . . . . . . . . 10
 
      |
79 | 78 | r19.21bi 2776 |
. . . . . . . . 9
 
       |
80 | 72, 75, 79 | syl2anc 673 |
. . . . . . . 8
   


         |
81 | | simplr 770 |
. . . . . . . . 9
   


     |
82 | | inss2 3644 |
. . . . . . . . . 10
   |
83 | 82, 74 | sseldi 3416 |
. . . . . . . . 9
   


     |
84 | 3 | neipeltop 20222 |
. . . . . . . . . . 11

 
       |
85 | 84 | simprbi 471 |
. . . . . . . . . 10
 
      |
86 | 85 | r19.21bi 2776 |
. . . . . . . . 9
 
       |
87 | 81, 83, 86 | syl2anc 673 |
. . . . . . . 8
   


         |
88 | | fvex 5889 |
. . . . . . . . 9
     |
89 | | inelfi 7950 |
. . . . . . . . 9
     
         
           |
90 | 88, 89 | mp3an1 1377 |
. . . . . . . 8
     
                 |
91 | 80, 87, 90 | syl2anc 673 |
. . . . . . 7
   


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


   
       |
93 | 92 | ralrimiva 2809 |
. . . . 5
                 |
94 | 3 | neipeltop 20222 |
. . . . 5
  
 
              |
95 | 70, 93, 94 | sylanbrc 677 |
. . . 4
     
   |
96 | 95 | ralrimiva 2809 |
. . 3
 
 
    |
97 | 96 | ralrimiva 2809 |
. 2
  
    |
98 | | istopg 20002 |
. . 3
 
     


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


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