Proof of Theorem topjoin
Step | Hyp | Ref
| Expression |
1 | | topontop 20018 |
. . . . . . 7
 TopOn 
  |
2 | 1 | ad2antrl 742 |
. . . . . 6
  
TopOn    TopOn  
    |
3 | | toponmax 20020 |
. . . . . . . . 9
 TopOn 
  |
4 | 3 | ad2antrl 742 |
. . . . . . . 8
  
TopOn    TopOn  
 
  |
5 | 4 | snssd 4108 |
. . . . . . 7
  
TopOn    TopOn  
      |
6 | | simprr 774 |
. . . . . . . 8
  
TopOn    TopOn  
  
  |
7 | | unissb 4221 |
. . . . . . . 8
 

  |
8 | 6, 7 | sylibr 217 |
. . . . . . 7
  
TopOn    TopOn  
  
  |
9 | 5, 8 | unssd 3601 |
. . . . . 6
  
TopOn    TopOn  
         |
10 | | tgfiss 20084 |
. . . . . 6
       
               |
11 | 2, 9, 10 | syl2anc 673 |
. . . . 5
  
TopOn    TopOn  
              
  |
12 | 11 | expr 626 |
. . . 4
  
TopOn  
TopOn    
                |
13 | 12 | ralrimiva 2809 |
. . 3
  TopOn    TopOn                 
   |
14 | | ssintrab 4249 |
. . 3
                TopOn   
 TopOn                 
   |
15 | 13, 14 | sylibr 217 |
. 2
  TopOn                  TopOn      |
16 | | fibas 20070 |
. . . . . 6
     
    |
17 | | tgtopon 20064 |
. . . . . 6
                       TopOn              |
18 | 16, 17 | ax-mp 5 |
. . . . 5
             TopOn             |
19 | | uniun 4209 |
. . . . . . . 8
              |
20 | | unisng 4206 |
. . . . . . . . . 10
   
  |
21 | 20 | adantr 472 |
. . . . . . . . 9
  TopOn     
  |
22 | 21 | uneq1d 3578 |
. . . . . . . 8
  TopOn                |
23 | 19, 22 | syl5req 2518 |
. . . . . . 7
  TopOn   
           |
24 | | simpr 468 |
. . . . . . . . . . 11
  TopOn   TopOn    |
25 | | toponuni 20019 |
. . . . . . . . . . . . . . 15
 TopOn 
   |
26 | | eqimss2 3471 |
. . . . . . . . . . . . . . 15
  
  |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
 TopOn 
   |
28 | | sspwuni 4360 |
. . . . . . . . . . . . . 14
 
   |
29 | 27, 28 | sylibr 217 |
. . . . . . . . . . . . 13
 TopOn 
   |
30 | | selpw 3949 |
. . . . . . . . . . . . 13
      |
31 | 29, 30 | sylibr 217 |
. . . . . . . . . . . 12
 TopOn 
    |
32 | 31 | ssriv 3422 |
. . . . . . . . . . 11
TopOn     |
33 | 24, 32 | syl6ss 3430 |
. . . . . . . . . 10
  TopOn       |
34 | | sspwuni 4360 |
. . . . . . . . . 10
  
    |
35 | 33, 34 | sylib 201 |
. . . . . . . . 9
  TopOn       |
36 | | sspwuni 4360 |
. . . . . . . . 9
  
    |
37 | 35, 36 | sylib 201 |
. . . . . . . 8
  TopOn       |
38 | | ssequn2 3598 |
. . . . . . . 8
  
      |
39 | 37, 38 | sylib 201 |
. . . . . . 7
  TopOn   
     |
40 | | snex 4641 |
. . . . . . . . 9
 
 |
41 | | fvex 5889 |
. . . . . . . . . . . 12
TopOn   |
42 | 41 | ssex 4540 |
. . . . . . . . . . 11
 TopOn    |
43 | 42 | adantl 473 |
. . . . . . . . . 10
  TopOn     |
44 | | uniexg 6607 |
. . . . . . . . . 10
    |
45 | 43, 44 | syl 17 |
. . . . . . . . 9
  TopOn      |
46 | | unexg 6611 |
. . . . . . . . 9
             |
47 | 40, 45, 46 | sylancr 676 |
. . . . . . . 8
  TopOn          |
48 | | fiuni 7960 |
. . . . . . . 8
         
        
     |
49 | 47, 48 | syl 17 |
. . . . . . 7
  TopOn                     |
50 | 23, 39, 49 | 3eqtr3d 2513 |
. . . . . 6
  TopOn               |
51 | 50 | fveq2d 5883 |
. . . . 5
  TopOn   TopOn  TopOn              |
52 | 18, 51 | syl5eleqr 2556 |
. . . 4
  TopOn                TopOn    |
53 | | elssuni 4219 |
. . . . . . . 8
    |
54 | | ssun2 3589 |
. . . . . . . 8
       |
55 | 53, 54 | syl6ss 3430 |
. . . . . . 7
        |
56 | | ssfii 7951 |
. . . . . . . 8
                      |
57 | 47, 56 | syl 17 |
. . . . . . 7
  TopOn             
     |
58 | 55, 57 | sylan9ssr 3432 |
. . . . . 6
  
TopOn  

           |
59 | | bastg 20058 |
. . . . . . 7
                                  |
60 | 16, 59 | ax-mp 5 |
. . . . . 6
     
  
              |
61 | 58, 60 | syl6ss 3430 |
. . . . 5
  
TopOn  

               |
62 | 61 | ralrimiva 2809 |
. . . 4
  TopOn   
               |
63 | | sseq2 3440 |
. . . . . 6
         
    
                |
64 | 63 | ralbidv 2829 |
. . . . 5
         
     

                |
65 | 64 | elrab 3184 |
. . . 4
               TopOn   
              TopOn 

                |
66 | 52, 62, 65 | sylanbrc 677 |
. . 3
  TopOn                 TopOn      |
67 | | intss1 4241 |
. . 3
               TopOn      TopOn  
                |
68 | 66, 67 | syl 17 |
. 2
  TopOn     TopOn  

               |
69 | 15, 68 | eqssd 3435 |
1
  TopOn                  TopOn  
   |