Step | Hyp | Ref
| Expression |
1 | | toponuni 20019 |
. . . . . 6
 TopOn 
   |
2 | | eqimss2 3471 |
. . . . . . 7
  
  |
3 | | sspwuni 4360 |
. . . . . . 7
 
   |
4 | 2, 3 | sylibr 217 |
. . . . . 6
 
   |
5 | 1, 4 | syl 17 |
. . . . 5
 TopOn 
   |
6 | | selpw 3949 |
. . . . 5
      |
7 | 5, 6 | sylibr 217 |
. . . 4
 TopOn 
    |
8 | 7 | ssriv 3422 |
. . 3
TopOn     |
9 | 8 | a1i 11 |
. 2
 TopOn      |
10 | | distopon 20089 |
. 2
 
TopOn    |
11 | | simpl 464 |
. . . . . . . . . . . . . 14
 
TopOn 

TopOn    |
12 | 11 | sselda 3418 |
. . . . . . . . . . . . 13
   TopOn    TopOn    |
13 | 12 | adantrl 730 |
. . . . . . . . . . . 12
   TopOn   

 
TopOn    |
14 | | topontop 20018 |
. . . . . . . . . . . 12
 TopOn 
  |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
   TopOn   

 
  |
16 | | simpl 464 |
. . . . . . . . . . . . 13
 


   |
17 | | intss1 4241 |
. . . . . . . . . . . . . 14
    |
18 | 17 | adantl 473 |
. . . . . . . . . . . . 13
 

    |
19 | 16, 18 | sstrd 3428 |
. . . . . . . . . . . 12
 


  |
20 | 19 | adantl 473 |
. . . . . . . . . . 11
   TopOn   

 
  |
21 | | uniopn 20004 |
. . . . . . . . . . 11
   
  |
22 | 15, 20, 21 | syl2anc 673 |
. . . . . . . . . 10
   TopOn   

 
   |
23 | 22 | expr 626 |
. . . . . . . . 9
   TopOn          |
24 | 23 | ralrimiv 2808 |
. . . . . . . 8
   TopOn     

  |
25 | | vex 3034 |
. . . . . . . . . 10
 |
26 | 25 | uniex 6606 |
. . . . . . . . 9
  |
27 | 26 | elint2 4233 |
. . . . . . . 8
 


   |
28 | 24, 27 | sylibr 217 |
. . . . . . 7
   TopOn     
   |
29 | 28 | ex 441 |
. . . . . 6
 
TopOn 

       |
30 | 29 | alrimiv 1781 |
. . . . 5
 
TopOn 

         |
31 | | simpll 768 |
. . . . . . . . . . 11
   TopOn    
   TopOn    |
32 | 31 | sselda 3418 |
. . . . . . . . . 10
    TopOn    
    TopOn    |
33 | | topontop 20018 |
. . . . . . . . . 10
 TopOn 
  |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
    TopOn    
      |
35 | | intss1 4241 |
. . . . . . . . . . 11
    |
36 | 35 | adantl 473 |
. . . . . . . . . 10
    TopOn    
       |
37 | | simplrl 778 |
. . . . . . . . . 10
    TopOn    
       |
38 | 36, 37 | sseldd 3419 |
. . . . . . . . 9
    TopOn    
      |
39 | | simplrr 779 |
. . . . . . . . . 10
    TopOn    
       |
40 | 36, 39 | sseldd 3419 |
. . . . . . . . 9
    TopOn    
      |
41 | | inopn 20006 |
. . . . . . . . 9
 
     |
42 | 34, 38, 40, 41 | syl3anc 1292 |
. . . . . . . 8
    TopOn    
    
   |
43 | 42 | ralrimiva 2809 |
. . . . . . 7
   TopOn    
   
    |
44 | 25 | inex1 4537 |
. . . . . . . 8
   |
45 | 44 | elint2 4233 |
. . . . . . 7
   

    |
46 | 43, 45 | sylibr 217 |
. . . . . 6
   TopOn    
   
    |
47 | 46 | ralrimivva 2814 |
. . . . 5
 
TopOn 

           |
48 | | intex 4557 |
. . . . . . . 8
    |
49 | 48 | biimpi 199 |
. . . . . . 7

   |
50 | 49 | adantl 473 |
. . . . . 6
 
TopOn 

   |
51 | | istopg 20002 |
. . . . . 6
 
      
      
         |
52 | 50, 51 | syl 17 |
. . . . 5
 
TopOn 

 
    
      
         |
53 | 30, 47, 52 | mpbir2and 936 |
. . . 4
 
TopOn 

   |
54 | 53 | 3adant1 1048 |
. . 3
  TopOn 

   |
55 | | n0 3732 |
. . . . . . . . . . 11
    |
56 | 55 | biimpi 199 |
. . . . . . . . . 10


  |
57 | 56 | ad2antlr 741 |
. . . . . . . . 9
   TopOn     
  |
58 | 17 | sselda 3418 |
. . . . . . . . . . . . . . 15
 
    |
59 | 58 | ancoms 460 |
. . . . . . . . . . . . . 14
  

  |
60 | | elssuni 4219 |
. . . . . . . . . . . . . 14
    |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . 13
  

   |
62 | 61 | adantl 473 |
. . . . . . . . . . . 12
   TopOn    
     |
63 | 12 | adantrl 730 |
. . . . . . . . . . . . 13
   TopOn    
  TopOn    |
64 | | toponuni 20019 |
. . . . . . . . . . . . 13
 TopOn 
   |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
   TopOn    
     |
66 | 62, 65 | sseqtr4d 3455 |
. . . . . . . . . . 11
   TopOn    
    |
67 | 66 | expr 626 |
. . . . . . . . . 10
   TopOn         |
68 | 67 | exlimdv 1787 |
. . . . . . . . 9
   TopOn          |
69 | 57, 68 | mpd 15 |
. . . . . . . 8
   TopOn    
  |
70 | 69 | ralrimiva 2809 |
. . . . . . 7
 
TopOn 

     |
71 | | unissb 4221 |
. . . . . . 7
  
     |
72 | 70, 71 | sylibr 217 |
. . . . . 6
 
TopOn 

    |
73 | 72 | 3adant1 1048 |
. . . . 5
  TopOn 

    |
74 | 11 | sselda 3418 |
. . . . . . . . . 10
   TopOn    TopOn    |
75 | | toponuni 20019 |
. . . . . . . . . 10
 TopOn 
   |
76 | 74, 75 | syl 17 |
. . . . . . . . 9
   TopOn       |
77 | | topontop 20018 |
. . . . . . . . . 10
 TopOn 
  |
78 | | eqid 2471 |
. . . . . . . . . . 11
   |
79 | 78 | topopn 20013 |
. . . . . . . . . 10
    |
80 | 74, 77, 79 | 3syl 18 |
. . . . . . . . 9
   TopOn       |
81 | 76, 80 | eqeltrd 2549 |
. . . . . . . 8
   TopOn      |
82 | 81 | ralrimiva 2809 |
. . . . . . 7
 
TopOn 


  |
83 | 82 | 3adant1 1048 |
. . . . . 6
  TopOn 


  |
84 | | elintg 4234 |
. . . . . . 7
 


   |
85 | 84 | 3ad2ant1 1051 |
. . . . . 6
  TopOn 

 

   |
86 | 83, 85 | mpbird 240 |
. . . . 5
  TopOn 

   |
87 | | unissel 4220 |
. . . . 5
       
  |
88 | 73, 86, 87 | syl2anc 673 |
. . . 4
  TopOn 

    |
89 | 88 | eqcomd 2477 |
. . 3
  TopOn 

    |
90 | | istopon 20017 |
. . 3
 
TopOn         |
91 | 54, 89, 90 | sylanbrc 677 |
. 2
  TopOn 

 TopOn    |
92 | 9, 10, 91 | ismred 15586 |
1
 TopOn  Moore     |