Step | Hyp | Ref
| Expression |
1 | | ssrab 3493 |
. . . . 5
              |
2 | | simprl 772 |
. . . . . . . . 9
  

  

  
   |
3 | | sspwuni 4360 |
. . . . . . . . 9
 
   |
4 | 2, 3 | sylib 201 |
. . . . . . . 8
  

  

  
   |
5 | | vex 3034 |
. . . . . . . . . 10
 |
6 | 5 | uniex 6606 |
. . . . . . . . 9
  |
7 | 6 | elpw 3948 |
. . . . . . . 8
 
 
  |
8 | 4, 7 | sylibr 217 |
. . . . . . 7
  

  

  
    |
9 | | neq0 3733 |
. . . . . . . . . 10
  
   |
10 | | eluni2 4194 |
. . . . . . . . . . . 12
 

  |
11 | | r19.29 2912 |
. . . . . . . . . . . . . . 15
   
   
  
   |
12 | | n0i 3727 |
. . . . . . . . . . . . . . . . . . . 20

  |
13 | 12 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
  

   |
14 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . 20
  

 
   |
15 | 14 | ord 384 |
. . . . . . . . . . . . . . . . . . 19
  

 
   |
16 | 13, 15 | mt3d 130 |
. . . . . . . . . . . . . . . . . 18
  

   |
17 | 16 | adantl 473 |
. . . . . . . . . . . . . . . . 17
    
 
  |
18 | | simpl 464 |
. . . . . . . . . . . . . . . . 17
    
 
  |
19 | | elunii 4195 |
. . . . . . . . . . . . . . . . 17
 
    |
20 | 17, 18, 19 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
    
 
   |
21 | 20 | rexlimiva 2868 |
. . . . . . . . . . . . . . 15
   

    |
22 | 11, 21 | syl 17 |
. . . . . . . . . . . . . 14
   
  
   |
23 | 22 | ex 441 |
. . . . . . . . . . . . 13
 

       |
24 | 23 | ad2antll 743 |
. . . . . . . . . . . 12
  

  

  
 
    |
25 | 10, 24 | syl5bi 225 |
. . . . . . . . . . 11
  

  

  
      |
26 | 25 | exlimdv 1787 |
. . . . . . . . . 10
  

  

  
 
     |
27 | 9, 26 | syl5bi 225 |
. . . . . . . . 9
  

  

  
      |
28 | 27 | con1d 129 |
. . . . . . . 8
  

  

  

     |
29 | 28 | orrd 385 |
. . . . . . 7
  

  

  
  
   |
30 | | eleq2 2538 |
. . . . . . . . 9
       |
31 | | eqeq1 2475 |
. . . . . . . . 9
   
   |
32 | 30, 31 | orbi12d 724 |
. . . . . . . 8
    
  
    |
33 | 32 | elrab 3184 |
. . . . . . 7
 
        
      |
34 | 8, 29, 33 | sylanbrc 677 |
. . . . . 6
  

  

  
  

    |
35 | 34 | ex 441 |
. . . . 5
 
   


  
        |
36 | 1, 35 | syl5bi 225 |
. . . 4
 
                |
37 | 36 | alrimiv 1781 |
. . 3
 
                  |
38 | | eleq2 2538 |
. . . . . . . 8
 
   |
39 | | eqeq1 2475 |
. . . . . . . 8
 
   |
40 | 38, 39 | orbi12d 724 |
. . . . . . 7
  


    |
41 | 40 | elrab 3184 |
. . . . . 6
             |
42 | | eleq2 2538 |
. . . . . . . 8
 
   |
43 | | eqeq1 2475 |
. . . . . . . 8
 
   |
44 | 42, 43 | orbi12d 724 |
. . . . . . 7
  


    |
45 | 44 | elrab 3184 |
. . . . . 6
             |
46 | 41, 45 | anbi12i 711 |
. . . . 5
            
              |
47 | | inss1 3643 |
. . . . . . . . 9
   |
48 | | simprll 780 |
. . . . . . . . . 10
  

                |
49 | 48 | elpwid 3952 |
. . . . . . . . 9
  

               |
50 | 47, 49 | syl5ss 3429 |
. . . . . . . 8
  

                 |
51 | 5 | inex1 4537 |
. . . . . . . . 9
   |
52 | 51 | elpw 3948 |
. . . . . . . 8
   
    |
53 | 50, 52 | sylibr 217 |
. . . . . . 7
  

                  |
54 | | ianor 496 |
. . . . . . . . . . 11
   
   |
55 | | elin 3608 |
. . . . . . . . . . 11
  

   |
56 | 54, 55 | xchnxbir 316 |
. . . . . . . . . 10
  

   |
57 | | simprlr 781 |
. . . . . . . . . . . 12
  

                 |
58 | 57 | ord 384 |
. . . . . . . . . . 11
  

             
   |
59 | | simprrr 783 |
. . . . . . . . . . . 12
  

                 |
60 | 59 | ord 384 |
. . . . . . . . . . 11
  

             
   |
61 | 58, 60 | orim12d 856 |
. . . . . . . . . 10
  

               
     |
62 | 56, 61 | syl5bi 225 |
. . . . . . . . 9
  

               
     |
63 | | inss 3652 |
. . . . . . . . . 10
 

    |
64 | | ss0b 3767 |
. . . . . . . . . . 11
   |
65 | | ss0b 3767 |
. . . . . . . . . . 11
   |
66 | 64, 65 | orbi12i 530 |
. . . . . . . . . 10
 

    |
67 | | ss0b 3767 |
. . . . . . . . . 10
       |
68 | 63, 66, 67 | 3imtr3i 273 |
. . . . . . . . 9
   
   |
69 | 62, 68 | syl6 33 |
. . . . . . . 8
  

               
     |
70 | 69 | orrd 385 |
. . . . . . 7
  

                     |
71 | | eleq2 2538 |
. . . . . . . . 9
   
     |
72 | | eqeq1 2475 |
. . . . . . . . 9
   
     |
73 | 71, 72 | orbi12d 724 |
. . . . . . . 8
    

         |
74 | 73 | elrab 3184 |
. . . . . . 7
                     |
75 | 53, 70, 74 | sylanbrc 677 |
. . . . . 6
  

                      |
76 | 75 | ex 441 |
. . . . 5
 
     
    
  
          |
77 | 46, 76 | syl5bi 225 |
. . . 4
 
    

 
     
          |
78 | 77 | ralrimivv 2813 |
. . 3
 
          

  
  

    |
79 | | pwexg 4585 |
. . . . . 6
 
  |
80 | 79 | adantr 472 |
. . . . 5
 
    |
81 | | rabexg 4549 |
. . . . 5
         |
82 | 80, 81 | syl 17 |
. . . 4
 
  

    |
83 | | istopg 20002 |
. . . 4
           
           

     

   
                |
84 | 82, 83 | syl 17 |
. . 3
 
      
           

     

   
                |
85 | 37, 78, 84 | mpbir2and 936 |
. 2
 
  

    |
86 | | pwidg 3955 |
. . . . . 6
    |
87 | 86 | adantr 472 |
. . . . 5
 
    |
88 | | simpr 468 |
. . . . . 6
 
   |
89 | 88 | orcd 399 |
. . . . 5
 
 
   |
90 | | eleq2 2538 |
. . . . . . 7
 
   |
91 | | eqeq1 2475 |
. . . . . . 7
 
   |
92 | 90, 91 | orbi12d 724 |
. . . . . 6
  


    |
93 | 92 | elrab 3184 |
. . . . 5
             |
94 | 87, 89, 93 | sylanbrc 677 |
. . . 4
 
        |
95 | | elssuni 4219 |
. . . 4
              |
96 | 94, 95 | syl 17 |
. . 3
 

        |
97 | | ssrab2 3500 |
. . . . 5
       |
98 | | sspwuni 4360 |
. . . . 5
               |
99 | 97, 98 | mpbi 213 |
. . . 4
       |
100 | 99 | a1i 11 |
. . 3
 
         |
101 | 96, 100 | eqssd 3435 |
. 2
 
         |
102 | | istopon 20017 |
. 2
      TopOn 
               |
103 | 85, 101, 102 | sylanbrc 677 |
1
 
  

  TopOn    |