Step | Hyp | Ref
| Expression |
1 | | utopreg.1 |
. . 3
unifTop   |
2 | | utoptop 21304 |
. . . 4
 UnifOn 
unifTop    |
3 | 2 | adantr 471 |
. . 3
  UnifOn   unifTop    |
4 | 1, 3 | syl5eqel 2544 |
. 2
  UnifOn     |
5 | | simp-4l 781 |
. . . . . . . . 9
        UnifOn 
 
           
   
 
   UnifOn       |
6 | 4 | ad2antrr 737 |
. . . . . . . . 9
    UnifOn 
 
   |
7 | 5, 6 | syl 17 |
. . . . . . . 8
        UnifOn 
 
           
   
 
  |
8 | | simplr 767 |
. . . . . . . . 9
        UnifOn 
 
           
   
 
  |
9 | | simp-4l 781 |
. . . . . . . . . 10
     UnifOn 
    UnifOn    |
10 | | simpr 467 |
. . . . . . . . . 10
     UnifOn 
      |
11 | 4 | ad3antrrr 741 |
. . . . . . . . . . . . 13
     UnifOn 
      |
12 | | simpllr 774 |
. . . . . . . . . . . . 13
     UnifOn 
      |
13 | | eqid 2462 |
. . . . . . . . . . . . . 14
   |
14 | 13 | eltopss 19992 |
. . . . . . . . . . . . 13
 

   |
15 | 11, 12, 14 | syl2anc 671 |
. . . . . . . . . . . 12
     UnifOn 
       |
16 | | utopbas 21305 |
. . . . . . . . . . . . . 14
 UnifOn 
 unifTop    |
17 | 1 | unieqi 4221 |
. . . . . . . . . . . . . 14
  unifTop   |
18 | 16, 17 | syl6eqr 2514 |
. . . . . . . . . . . . 13
 UnifOn 
   |
19 | 9, 18 | syl 17 |
. . . . . . . . . . . 12
     UnifOn 
       |
20 | 15, 19 | sseqtr4d 3481 |
. . . . . . . . . . 11
     UnifOn 
      |
21 | | simplr 767 |
. . . . . . . . . . 11
     UnifOn 
      |
22 | 20, 21 | sseldd 3445 |
. . . . . . . . . 10
     UnifOn 
      |
23 | 1 | utopsnnei 21319 |
. . . . . . . . . 10
  UnifOn 
                   |
24 | 9, 10, 22, 23 | syl3anc 1276 |
. . . . . . . . 9
     UnifOn 
                      |
25 | 5, 8, 24 | syl2anc 671 |
. . . . . . . 8
        UnifOn 
 
           
   
 
                  |
26 | | neii2 20179 |
. . . . . . . 8
                   
            |
27 | 7, 25, 26 | syl2anc 671 |
. . . . . . 7
        UnifOn 
 
           
   
 

  
         |
28 | | simprl 769 |
. . . . . . . . . . 11
          UnifOn               
   
 
                |
29 | | vex 3060 |
. . . . . . . . . . . 12
 |
30 | 29 | snss 4109 |
. . . . . . . . . . 11

    |
31 | 28, 30 | sylibr 217 |
. . . . . . . . . 10
          UnifOn               
   
 
              |
32 | 7 | ad2antrr 737 |
. . . . . . . . . . . . 13
          UnifOn               
   
 
              |
33 | | simplll 773 |
. . . . . . . . . . . . . . . . 17
    UnifOn 
 
 UnifOn    |
34 | 5, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
        UnifOn 
 
           
   
 
UnifOn    |
35 | 34 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
          UnifOn               
   
 
            UnifOn    |
36 | 8 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
          UnifOn               
   
 
              |
37 | | simplr 767 |
. . . . . . . . . . . . . . . . . . 19
    UnifOn 
 
   |
38 | 6, 37, 14 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
    UnifOn 
 
    |
39 | 33, 18 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    UnifOn 
 
    |
40 | 38, 39 | sseqtr4d 3481 |
. . . . . . . . . . . . . . . . 17
    UnifOn 
 
   |
41 | | simpr 467 |
. . . . . . . . . . . . . . . . 17
    UnifOn 
 
   |
42 | 40, 41 | sseldd 3445 |
. . . . . . . . . . . . . . . 16
    UnifOn 
 
   |
43 | 42 | ad6antr 747 |
. . . . . . . . . . . . . . 15
          UnifOn               
   
 
              |
44 | | ustimasn 21298 |
. . . . . . . . . . . . . . 15
  UnifOn 
         |
45 | 35, 36, 43, 44 | syl3anc 1276 |
. . . . . . . . . . . . . 14
          UnifOn               
   
 
                    |
46 | 35, 18 | syl 17 |
. . . . . . . . . . . . . 14
          UnifOn               
   
 
               |
47 | 45, 46 | sseqtrd 3480 |
. . . . . . . . . . . . 13
          UnifOn               
   
 
                     |
48 | | simprr 771 |
. . . . . . . . . . . . 13
          UnifOn               
   
 
                    |
49 | 13 | clsss 20124 |
. . . . . . . . . . . . 13
                       
                |
50 | 32, 47, 48, 49 | syl3anc 1276 |
. . . . . . . . . . . 12
          UnifOn               
   
 
                   
                |
51 | | ustssxp 21274 |
. . . . . . . . . . . . . . . . 17
  UnifOn       |
52 | 34, 8, 51 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
        UnifOn 
 
           
   
 
    |
53 | 34, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
        UnifOn 
 
           
   
 
   |
54 | 53 | sqxpeqd 4882 |
. . . . . . . . . . . . . . . 16
        UnifOn 
 
           
   
 
        |
55 | 52, 54 | sseqtrd 3480 |
. . . . . . . . . . . . . . 15
        UnifOn 
 
           
   
 
 
    |
56 | 5, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
        UnifOn 
 
           
   
 
   |
57 | | simp-5r 784 |
. . . . . . . . . . . . . . . 16
        UnifOn 
 
           
   
 
  |
58 | 56, 57 | sseldd 3445 |
. . . . . . . . . . . . . . 15
        UnifOn 
 
           
   
 
   |
59 | 13, 13 | imasncls 20762 |
. . . . . . . . . . . . . . 15
      
 
                
                  |
60 | 7, 7, 55, 58, 59 | syl22anc 1277 |
. . . . . . . . . . . . . 14
        UnifOn 
 
           
   
 
                                |
61 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
        UnifOn 
 
           
   
 
   |
62 | 1 | utop3cls 21321 |
. . . . . . . . . . . . . . . . 17
   UnifOn      
            
     |
63 | 34, 52, 8, 61, 62 | syl22anc 1277 |
. . . . . . . . . . . . . . . 16
        UnifOn 
 
           
   
 
                |
64 | | simprr 771 |
. . . . . . . . . . . . . . . 16
        UnifOn 
 
           
   
 
      |
65 | 63, 64 | sstrd 3454 |
. . . . . . . . . . . . . . 15
        UnifOn 
 
           
   
 
            |
66 | | imass1 5225 |
. . . . . . . . . . . . . . 15
                                   |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . 14
        UnifOn 
 
           
   
 
                        |
68 | 60, 67 | sstrd 3454 |
. . . . . . . . . . . . 13
        UnifOn 
 
           
   
 
                      |
69 | 68 | ad2antrr 737 |
. . . . . . . . . . . 12
          UnifOn               
   
 
                                  |
70 | 50, 69 | sstrd 3454 |
. . . . . . . . . . 11
          UnifOn               
   
 
                   
        |
71 | | simp-5r 784 |
. . . . . . . . . . 11
          UnifOn               
   
 
                    |
72 | 70, 71 | sseqtr4d 3481 |
. . . . . . . . . 10
          UnifOn               
   
 
                   
  |
73 | 31, 72 | jca 539 |
. . . . . . . . 9
          UnifOn               
   
 
                        |
74 | 73 | ex 440 |
. . . . . . . 8
         UnifOn 
             
   
 
                         |
75 | 74 | reximdva 2874 |
. . . . . . 7
        UnifOn 
 
           
   
 
 
          

            |
76 | 27, 75 | mpd 15 |
. . . . . 6
        UnifOn 
 
           
   
 


           |
77 | | simp-5l 783 |
. . . . . . 7
      UnifOn            
UnifOn    |
78 | | simplr 767 |
. . . . . . 7
      UnifOn            
  |
79 | | ustex3sym 21287 |
. . . . . . 7
  UnifOn   
 

  
   |
80 | 77, 78, 79 | syl2anc 671 |
. . . . . 6
      UnifOn            

 

  
   |
81 | 76, 80 | r19.29a 2944 |
. . . . 5
      UnifOn            


           |
82 | | opnneip 20190 |
. . . . . . . 8
 
             |
83 | 6, 37, 41, 82 | syl3anc 1276 |
. . . . . . 7
    UnifOn 
 
             |
84 | 1 | utopsnneip 21318 |
. . . . . . . 8
  UnifOn                       |
85 | 33, 42, 84 | syl2anc 671 |
. . . . . . 7
    UnifOn 
 
                     |
86 | 83, 85 | eleqtrd 2542 |
. . . . . 6
    UnifOn 
 
           |
87 | | eqid 2462 |
. . . . . . . 8
                 |
88 | 87 | elrnmpt 5103 |
. . . . . . 7
         

         |
89 | 37, 88 | syl 17 |
. . . . . 6
    UnifOn 
 
         

         |
90 | 86, 89 | mpbid 215 |
. . . . 5
    UnifOn 
 
 
        |
91 | 81, 90 | r19.29a 2944 |
. . . 4
    UnifOn 
 
 

           |
92 | 91 | ralrimiva 2814 |
. . 3
   UnifOn    


           |
93 | 92 | ralrimiva 2814 |
. 2
  UnifOn   



           |
94 | | isreg 20403 |
. 2

 



            |
95 | 4, 93, 94 | sylanbrc 675 |
1
  UnifOn     |