Step | Hyp | Ref
| Expression |
1 | | flimcls.2 |
. . 3
                       |
2 | | topontop 19934 |
. . . . . . . . 9
 TopOn 
  |
3 | 2 | 3ad2ant1 1028 |
. . . . . . . 8
  TopOn          
  |
4 | | eqid 2450 |
. . . . . . . . 9
   |
5 | 4 | neisspw 20116 |
. . . . . . . 8
               |
6 | 3, 5 | syl 17 |
. . . . . . 7
  TopOn          
              |
7 | | toponuni 19935 |
. . . . . . . . 9
 TopOn 
   |
8 | 7 | 3ad2ant1 1028 |
. . . . . . . 8
  TopOn          
   |
9 | 8 | pweqd 3955 |
. . . . . . 7
  TopOn          
     |
10 | 6, 9 | sseqtr4d 3468 |
. . . . . 6
  TopOn          
             |
11 | | toponmax 19936 |
. . . . . . . . . 10
 TopOn 
  |
12 | | elpw2g 4565 |
. . . . . . . . . 10
 
    |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
 TopOn 
 
   |
14 | 13 | biimpar 488 |
. . . . . . . 8
  TopOn      |
15 | 14 | 3adant3 1027 |
. . . . . . 7
  TopOn          
   |
16 | 15 | snssd 4116 |
. . . . . 6
  TopOn          
     |
17 | 10, 16 | unssd 3609 |
. . . . 5
  TopOn          
                 |
18 | | ssun2 3597 |
. . . . . 6
                 |
19 | 11 | 3ad2ant1 1028 |
. . . . . . . 8
  TopOn          
  |
20 | | simp2 1008 |
. . . . . . . 8
  TopOn          
  |
21 | 19, 20 | ssexd 4549 |
. . . . . . 7
  TopOn          
  |
22 | | snnzg 4088 |
. . . . . . 7
     |
23 | 21, 22 | syl 17 |
. . . . . 6
  TopOn          
    |
24 | | ssn0 3766 |
. . . . . 6
                   
                 |
25 | 18, 23, 24 | sylancr 668 |
. . . . 5
  TopOn          
                |
26 | 20, 8 | sseqtrd 3467 |
. . . . . . . . . . 11
  TopOn          
   |
27 | | simp3 1009 |
. . . . . . . . . . 11
  TopOn          
          |
28 | 4 | neindisj 20126 |
. . . . . . . . . . . 12
  
          
                |
29 | 28 | expr 619 |
. . . . . . . . . . 11
  
          
           
    |
30 | 3, 26, 27, 29 | syl21anc 1266 |
. . . . . . . . . 10
  TopOn          
           
    |
31 | 30 | imp 431 |
. . . . . . . . 9
   TopOn          
               |
32 | | elsni 3992 |
. . . . . . . . . . 11
     |
33 | 32 | ineq2d 3633 |
. . . . . . . . . 10
         |
34 | 33 | neeq1d 2682 |
. . . . . . . . 9
     
     |
35 | 31, 34 | syl5ibrcom 226 |
. . . . . . . 8
   TopOn          
             
     |
36 | 35 | ralrimiv 2799 |
. . . . . . 7
   TopOn          
           
      |
37 | 36 | ralrimiva 2801 |
. . . . . 6
  TopOn          
               
   |
38 | | simp1 1007 |
. . . . . . . . 9
  TopOn          
TopOn    |
39 | 4 | clsss3 20067 |
. . . . . . . . . . . . 13
           
   |
40 | 3, 26, 39 | syl2anc 666 |
. . . . . . . . . . . 12
  TopOn          
           |
41 | 40, 27 | sseldd 3432 |
. . . . . . . . . . 11
  TopOn          
   |
42 | 41, 8 | eleqtrrd 2531 |
. . . . . . . . . 10
  TopOn          
  |
43 | 42 | snssd 4116 |
. . . . . . . . 9
  TopOn          
    |
44 | | snnzg 4088 |
. . . . . . . . . 10
        
    |
45 | 44 | 3ad2ant3 1030 |
. . . . . . . . 9
  TopOn          
    |
46 | | neifil 20888 |
. . . . . . . . 9
  TopOn   
                   |
47 | 38, 43, 45, 46 | syl3anc 1267 |
. . . . . . . 8
  TopOn          
                |
48 | | filfbas 20856 |
. . . . . . . 8
                               |
49 | 47, 48 | syl 17 |
. . . . . . 7
  TopOn          
                |
50 | | ne0i 3736 |
. . . . . . . . . . 11
        
          |
51 | 50 | 3ad2ant3 1030 |
. . . . . . . . . 10
  TopOn          
          |
52 | | cls0 20089 |
. . . . . . . . . . 11
           |
53 | 3, 52 | syl 17 |
. . . . . . . . . 10
  TopOn          
          |
54 | 51, 53 | neeqtrrd 2697 |
. . . . . . . . 9
  TopOn          
                  |
55 | | fveq2 5863 |
. . . . . . . . . 10

                  |
56 | 55 | necon3i 2655 |
. . . . . . . . 9
                   |
57 | 54, 56 | syl 17 |
. . . . . . . 8
  TopOn          
  |
58 | | snfbas 20874 |
. . . . . . . 8
 
  
      |
59 | 20, 57, 19, 58 | syl3anc 1267 |
. . . . . . 7
  TopOn          
 
      |
60 | | fbunfip 20877 |
. . . . . . 7
                      
                  
               
    |
61 | 49, 59, 60 | syl2anc 666 |
. . . . . 6
  TopOn          
                  
               
    |
62 | 37, 61 | mpbird 236 |
. . . . 5
  TopOn          
                    |
63 | | fsubbas 20875 |
. . . . . 6
                                                                            |
64 | 19, 63 | syl 17 |
. . . . 5
  TopOn          
                                                                           |
65 | 17, 25, 62, 64 | mpbir3and 1190 |
. . . 4
  TopOn          
                        |
66 | | fgcl 20886 |
. . . 4
                      
                            |
67 | 65, 66 | syl 17 |
. . 3
  TopOn          
                            |
68 | 1, 67 | syl5eqel 2532 |
. 2
  TopOn          
      |
69 | | fvex 5873 |
. . . . . 6
           |
70 | | snex 4640 |
. . . . . 6
 
 |
71 | 69, 70 | unex 6586 |
. . . . 5
               |
72 | | ssfii 7930 |
. . . . 5
                                                 |
73 | 71, 72 | ax-mp 5 |
. . . 4
                                 |
74 | | ssfg 20880 |
. . . . . 6
                      
                                          |
75 | 65, 74 | syl 17 |
. . . . 5
  TopOn          
                                          |
76 | 75, 1 | syl6sseqr 3478 |
. . . 4
  TopOn          
                    |
77 | 73, 76 | syl5ss 3442 |
. . 3
  TopOn          
                |
78 | | snssg 4104 |
. . . . 5
 
             
                   |
79 | 21, 78 | syl 17 |
. . . 4
  TopOn          
              
                   |
80 | 18, 79 | mpbiri 237 |
. . 3
  TopOn          
                |
81 | 77, 80 | sseldd 3432 |
. 2
  TopOn          
  |
82 | 77 | unssad 3610 |
. . 3
  TopOn          
            |
83 | | elflim 20979 |
. . . 4
  TopOn       
 

              |
84 | 38, 68, 83 | syl2anc 666 |
. . 3
  TopOn          
             
    |
85 | 42, 82, 84 | mpbir2and 932 |
. 2
  TopOn          

   |
86 | 68, 81, 85 | 3jca 1187 |
1
  TopOn          
    

    |