Step | Hyp | Ref
| Expression |
1 | | ucncn.5 |
. . . 4
  UnifSt 
Cnu UnifSt     |
2 | | ucncn.1 |
. . . . . 6

UnifSp |
3 | | eqid 2462 |
. . . . . . . 8
         |
4 | | eqid 2462 |
. . . . . . . 8
UnifSt  UnifSt   |
5 | | ucncn.j |
. . . . . . . 8
     |
6 | 3, 4, 5 | isusp 21325 |
. . . . . . 7
 UnifSp  UnifSt  UnifOn     
unifTop UnifSt      |
7 | 6 | simplbi 466 |
. . . . . 6
 UnifSp UnifSt  UnifOn        |
8 | 2, 7 | syl 17 |
. . . . 5
 UnifSt  UnifOn        |
9 | | ucncn.2 |
. . . . . 6

UnifSp |
10 | | eqid 2462 |
. . . . . . . 8
         |
11 | | eqid 2462 |
. . . . . . . 8
UnifSt  UnifSt   |
12 | | ucncn.k |
. . . . . . . 8
     |
13 | 10, 11, 12 | isusp 21325 |
. . . . . . 7
 UnifSp  UnifSt  UnifOn     
unifTop UnifSt      |
14 | 13 | simplbi 466 |
. . . . . 6
 UnifSp UnifSt  UnifOn        |
15 | 9, 14 | syl 17 |
. . . . 5
 UnifSt  UnifOn        |
16 | | isucn 21342 |
. . . . 5
  UnifSt  UnifOn      UnifSt  UnifOn         UnifSt  Cnu UnifSt                 UnifSt    UnifSt   
     
                       |
17 | 8, 15, 16 | syl2anc 671 |
. . . 4
   UnifSt  Cnu UnifSt  
            
 UnifSt   
UnifSt                 
               |
18 | 1, 17 | mpbid 215 |
. . 3
               UnifSt    UnifSt   
     
                      |
19 | 18 | simpld 465 |
. 2
               |
20 | | cnvimass 5207 |
. . . . 5
    
 |
21 | | fdm 5756 |
. . . . . . 7
            
      |
22 | 19, 21 | syl 17 |
. . . . . 6
       |
23 | 22 | adantr 471 |
. . . . 5
 
       |
24 | 20, 23 | syl5sseq 3492 |
. . . 4
 
            |
25 | | simplll 773 |
. . . . . . . . 9
   

      UnifSt  
  |
26 | | simpr 467 |
. . . . . . . . 9
   

      UnifSt  
UnifSt    |
27 | 24 | ad2antrr 737 |
. . . . . . . . . 10
   

      UnifSt  
           |
28 | | simplr 767 |
. . . . . . . . . 10
   

      UnifSt  
       |
29 | 27, 28 | sseldd 3445 |
. . . . . . . . 9
   

      UnifSt  
      |
30 | 18 | simprd 469 |
. . . . . . . . . . . 12
  UnifSt    UnifSt   
     
                     |
31 | 30 | r19.21bi 2769 |
. . . . . . . . . . 11
 
UnifSt    UnifSt                 
             |
32 | | r19.12 2928 |
. . . . . . . . . . 11
  UnifSt                 
          
       UnifSt   
                     |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
 
UnifSt         
UnifSt           
             |
34 | 33 | r19.21bi 2769 |
. . . . . . . . 9
   UnifSt  
    
 UnifSt   
                     |
35 | 25, 26, 29, 34 | syl21anc 1275 |
. . . . . . . 8
   

      UnifSt  
 UnifSt   
                     |
36 | 35 | adantr 471 |
. . . . . . 7
            UnifSt  
           
UnifSt           
             |
37 | 25 | ad3antrrr 741 |
. . . . . . . . . 10
             
UnifSt             
UnifSt           
              |
38 | 8 | ad5antr 745 |
. . . . . . . . . . . 12
     
      
UnifSt             
UnifSt   UnifSt  UnifOn        |
39 | | simpr 467 |
. . . . . . . . . . . 12
     
      
UnifSt             
UnifSt   UnifSt    |
40 | | ustrel 21275 |
. . . . . . . . . . . 12
  UnifSt  UnifOn     
UnifSt     |
41 | 38, 39, 40 | syl2anc 671 |
. . . . . . . . . . 11
     
      
UnifSt             
UnifSt  
  |
42 | 41 | adantr 471 |
. . . . . . . . . 10
             
UnifSt             
UnifSt           
              |
43 | 37, 8 | syl 17 |
. . . . . . . . . . 11
             
UnifSt             
UnifSt           
            UnifSt  UnifOn        |
44 | | simplr 767 |
. . . . . . . . . . 11
             
UnifSt             
UnifSt           
            UnifSt    |
45 | 29 | ad3antrrr 741 |
. . . . . . . . . . 11
             
UnifSt             
UnifSt           
                  |
46 | | ustimasn 21292 |
. . . . . . . . . . 11
  UnifSt  UnifOn     
UnifSt 
    
            |
47 | 43, 44, 45, 46 | syl3anc 1276 |
. . . . . . . . . 10
             
UnifSt             
UnifSt           
                        |
48 | | simpr 467 |
. . . . . . . . . . 11
             
UnifSt             
UnifSt           
                    
             |
49 | | simplr 767 |
. . . . . . . . . . . . . . 15
       

      UnifSt  
          
UnifSt                         |
50 | | simpllr 774 |
. . . . . . . . . . . . . . . . 17
             
UnifSt             
UnifSt             
            |
51 | 15 | ad5antr 745 |
. . . . . . . . . . . . . . . . . . . 20
     
      
UnifSt             
UnifSt   UnifSt  UnifOn        |
52 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . . 20
     
      
UnifSt             
UnifSt   UnifSt    |
53 | | ustrel 21275 |
. . . . . . . . . . . . . . . . . . . 20
  UnifSt  UnifOn     
UnifSt     |
54 | 51, 52, 53 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
     
      
UnifSt             
UnifSt  
  |
55 | | elrelimasn 5211 |
. . . . . . . . . . . . . . . . . . 19

              
             |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     
      
UnifSt             
UnifSt                 
             |
57 | 56 | biimpar 492 |
. . . . . . . . . . . . . . . . 17
             
UnifSt             
UnifSt             
                |
58 | 50, 57 | sseldd 3445 |
. . . . . . . . . . . . . . . 16
             
UnifSt             
UnifSt             
      |
59 | 58 | adantlr 726 |
. . . . . . . . . . . . . . 15
       

      UnifSt  
          
UnifSt                         |
60 | | ffn 5751 |
. . . . . . . . . . . . . . . . 17
            
      |
61 | | elpreima 6025 |
. . . . . . . . . . . . . . . . 17
    
     
    
        |
62 | 19, 60, 61 | 3syl 18 |
. . . . . . . . . . . . . . . 16
                    |
63 | 62 | ad7antr 749 |
. . . . . . . . . . . . . . 15
       

      UnifSt  
          
UnifSt                                      |
64 | 49, 59, 63 | mpbir2and 938 |
. . . . . . . . . . . . . 14
       

      UnifSt  
          
UnifSt                          |
65 | 64 | ex 440 |
. . . . . . . . . . . . 13
             
UnifSt             
UnifSt       
                   |
66 | 65 | ralrimiva 2814 |
. . . . . . . . . . . 12
     
      
UnifSt             
UnifSt                            |
67 | 66 | adantr 471 |
. . . . . . . . . . 11
             
UnifSt             
UnifSt           
                            
        |
68 | | r19.26 2929 |
. . . . . . . . . . . 12
 
                              
      
 
                                             |
69 | | pm3.33 593 |
. . . . . . . . . . . . 13
                                    
        |
70 | 69 | ralimi 2793 |
. . . . . . . . . . . 12
 
                              
               
        |
71 | 68, 70 | sylbir 218 |
. . . . . . . . . . 11
                                      
               
        |
72 | 48, 67, 71 | syl2anc 671 |
. . . . . . . . . 10
             
UnifSt             
UnifSt           
                    
        |
73 | | simpl2l 1067 |
. . . . . . . . . . . . . 14
   
                   
             
  |
74 | | simpr 467 |
. . . . . . . . . . . . . 14
   
                   
                      |
75 | | elrelimasn 5211 |
. . . . . . . . . . . . . . 15

      
     |
76 | 75 | biimpa 491 |
. . . . . . . . . . . . . 14
             |
77 | 73, 74, 76 | syl2anc 671 |
. . . . . . . . . . . . 13
   
                   
                  |
78 | | simpl2r 1068 |
. . . . . . . . . . . . . . 15
   
                   
                          |
79 | 78, 74 | sseldd 3445 |
. . . . . . . . . . . . . 14
   
                   
                    |
80 | | simpl3 1019 |
. . . . . . . . . . . . . 14
   
                   
                               |
81 | | breq2 4420 |
. . . . . . . . . . . . . . . 16
   
     |
82 | | eleq1 2528 |
. . . . . . . . . . . . . . . 16
               |
83 | 81, 82 | imbi12d 326 |
. . . . . . . . . . . . . . 15
             
         |
84 | 83 | rspcv 3158 |
. . . . . . . . . . . . . 14
    
 
                          |
85 | 79, 80, 84 | sylc 62 |
. . . . . . . . . . . . 13
   
                   
                
        |
86 | 77, 85 | mpd 15 |
. . . . . . . . . . . 12
   
                   
                     |
87 | 86 | ex 440 |
. . . . . . . . . . 11
 
            
                              |
88 | 87 | ssrdv 3450 |
. . . . . . . . . 10
 
            
                            |
89 | 37, 42, 47, 72, 88 | syl121anc 1281 |
. . . . . . . . 9
             
UnifSt             
UnifSt           
                         |
90 | 89 | ex 440 |
. . . . . . . 8
     
      
UnifSt             
UnifSt            
          
              |
91 | 90 | reximdva 2874 |
. . . . . . 7
            UnifSt  
             UnifSt   
                    UnifSt        
        |
92 | 36, 91 | mpd 15 |
. . . . . 6
            UnifSt  
           
UnifSt        
       |
93 | | elpreima 6025 |
. . . . . . . . . . 11
    
     
    
        |
94 | 19, 60, 93 | 3syl 18 |
. . . . . . . . . 10
                    |
95 | 94 | adantr 471 |
. . . . . . . . 9
 
                    |
96 | 95 | biimpa 491 |
. . . . . . . 8
                      |
97 | 96 | simprd 469 |
. . . . . . 7
                |
98 | | simpr 467 |
. . . . . . . . . . 11
 
   |
99 | 13 | simprbi 470 |
. . . . . . . . . . . . 13
 UnifSp unifTop UnifSt     |
100 | 9, 99 | syl 17 |
. . . . . . . . . . . 12
 unifTop UnifSt     |
101 | 100 | adantr 471 |
. . . . . . . . . . 11
 
 unifTop UnifSt     |
102 | 98, 101 | eleqtrd 2542 |
. . . . . . . . . 10
 
 unifTop UnifSt     |
103 | | elutop 21297 |
. . . . . . . . . . . 12
 UnifSt  UnifOn       unifTop UnifSt  
    

 UnifSt             |
104 | 15, 103 | syl 17 |
. . . . . . . . . . 11
  unifTop UnifSt          UnifSt        
    |
105 | 104 | adantr 471 |
. . . . . . . . . 10
 
  unifTop UnifSt  
    

 UnifSt             |
106 | 102, 105 | mpbid 215 |
. . . . . . . . 9
 
 
    

UnifSt            |
107 | 106 | simprd 469 |
. . . . . . . 8
 
 
 UnifSt           |
108 | 107 | adantr 471 |
. . . . . . 7
          

UnifSt        
  |
109 | | sneq 3990 |
. . . . . . . . . . 11
               |
110 | 109 | imaeq2d 5187 |
. . . . . . . . . 10
                       |
111 | 110 | sseq1d 3471 |
. . . . . . . . 9
                         |
112 | 111 | rexbidv 2913 |
. . . . . . . 8
      
UnifSt        
 UnifSt                |
113 | 112 | rspcv 3158 |
. . . . . . 7
      

UnifSt        
 UnifSt            
   |
114 | 97, 108, 113 | sylc 62 |
. . . . . 6
          
UnifSt            
  |
115 | 92, 114 | r19.29a 2944 |
. . . . 5
          
UnifSt        
       |
116 | 115 | ralrimiva 2814 |
. . . 4
 
         UnifSt                |
117 | 6 | simprbi 470 |
. . . . . . . 8
 UnifSp unifTop UnifSt     |
118 | 2, 117 | syl 17 |
. . . . . . 7
 unifTop UnifSt     |
119 | 118 | adantr 471 |
. . . . . 6
 
 unifTop UnifSt     |
120 | 119 | eleq2d 2525 |
. . . . 5
 
            unifTop UnifSt      |
121 | | elutop 21297 |
. . . . . . 7
 UnifSt  UnifOn            unifTop UnifSt            
        UnifSt                  |
122 | 8, 121 | syl 17 |
. . . . . 6
       unifTop UnifSt            
        UnifSt                  |
123 | 122 | adantr 471 |
. . . . 5
 
       unifTop UnifSt            
        UnifSt                  |
124 | 120, 123 | bitrd 261 |
. . . 4
 
                         UnifSt        
         |
125 | 24, 116, 124 | mpbir2and 938 |
. . 3
 
        |
126 | 125 | ralrimiva 2814 |
. 2
         |
127 | | ucncn.3 |
. . . 4
   |
128 | 3, 5 | istps 20000 |
. . . 4
 TopOn        |
129 | 127, 128 | sylib 201 |
. . 3
 TopOn        |
130 | | ucncn.4 |
. . . 4
   |
131 | 10, 12 | istps 20000 |
. . . 4
 TopOn        |
132 | 130, 131 | sylib 201 |
. . 3
 TopOn        |
133 | | iscn 20300 |
. . 3
  TopOn     
TopOn                                 |
134 | 129, 132,
133 | syl2anc 671 |
. 2
                           |
135 | 19, 126, 134 | mpbir2and 938 |
1
     |