Step | Hyp | Ref
| Expression |
1 | | simp2 1010 |
. . . . 5
  UnifSp

  |
2 | | neipcfilu.x |
. . . . . 6
     |
3 | | neipcfilu.j |
. . . . . 6
     |
4 | 2, 3 | istps 19962 |
. . . . 5
 TopOn    |
5 | 1, 4 | sylib 201 |
. . . 4
  UnifSp

TopOn    |
6 | | simp3 1011 |
. . . . 5
  UnifSp

  |
7 | 6 | snssd 4086 |
. . . 4
  UnifSp

    |
8 | | snnzg 4058 |
. . . . 5
     |
9 | 6, 8 | syl 17 |
. . . 4
  UnifSp

    |
10 | | neifil 20906 |
. . . 4
  TopOn   
                   |
11 | 5, 7, 9, 10 | syl3anc 1271 |
. . 3
  UnifSp

                |
12 | | filfbas 20874 |
. . 3
                               |
13 | 11, 12 | syl 17 |
. 2
  UnifSp

                |
14 | | eqid 2452 |
. . . . . . . . . 10
             |
15 | | imaeq1 5141 |
. . . . . . . . . . . 12
               |
16 | 15 | eqeq2d 2462 |
. . . . . . . . . . 11
             
               |
17 | 16 | rspcev 3118 |
. . . . . . . . . 10
               
              |
18 | 14, 17 | mpan2 682 |
. . . . . . . . 9
 
              |
19 | | vex 3016 |
. . . . . . . . . 10
 |
20 | | imaexg 6718 |
. . . . . . . . . 10
         |
21 | | eqid 2452 |
. . . . . . . . . . 11
                 |
22 | 21 | elrnmpt 5059 |
. . . . . . . . . 10
                      
               |
23 | 19, 20, 22 | mp2b 10 |
. . . . . . . . 9
              

              |
24 | 18, 23 | sylibr 217 |
. . . . . . . 8
                 |
25 | 24 | ad2antlr 738 |
. . . . . . 7
     UnifSp  
                                |
26 | | neipcfilu.u |
. . . . . . . . . . . . 13
UnifSt   |
27 | 2, 26, 3 | isusp 21287 |
. . . . . . . . . . . 12
 UnifSp  UnifOn  unifTop     |
28 | 27 | simplbi 466 |
. . . . . . . . . . 11
 UnifSp UnifOn    |
29 | 28 | 3ad2ant1 1030 |
. . . . . . . . . 10
  UnifSp

UnifOn    |
30 | | eqid 2452 |
. . . . . . . . . . 11
unifTop  unifTop   |
31 | 30 | utopsnneip 21274 |
. . . . . . . . . 10
  UnifOn       unifTop                  |
32 | 29, 6, 31 | syl2anc 671 |
. . . . . . . . 9
  UnifSp

    unifTop                  |
33 | 32 | eleq2d 2515 |
. . . . . . . 8
  UnifSp

           unifTop       
                 |
34 | 33 | ad3antrrr 741 |
. . . . . . 7
     UnifSp  
                           unifTop       
                 |
35 | 25, 34 | mpbird 240 |
. . . . . 6
     UnifSp  
                          unifTop          |
36 | | simpl1 1012 |
. . . . . . . . . 10
   UnifSp
 
               
UnifSp |
37 | 36 | 3anassrs 1235 |
. . . . . . . . 9
     UnifSp  
                UnifSp |
38 | 27 | simprbi 470 |
. . . . . . . . 9
 UnifSp unifTop    |
39 | 37, 38 | syl 17 |
. . . . . . . 8
     UnifSp  
                unifTop    |
40 | 39 | fveq2d 5852 |
. . . . . . 7
     UnifSp  
                       unifTop     |
41 | 40 | fveq1d 5850 |
. . . . . 6
     UnifSp  
                              unifTop          |
42 | 35, 41 | eleqtrrd 2533 |
. . . . 5
     UnifSp  
                                  |
43 | | simpr 467 |
. . . . 5
     UnifSp  
                                |
44 | | id 22 |
. . . . . . . 8
               |
45 | 44 | sqxpeqd 4838 |
. . . . . . 7
                         |
46 | 45 | sseq1d 3427 |
. . . . . 6
                           |
47 | 46 | rspcev 3118 |
. . . . 5
                                                 |
48 | 42, 43, 47 | syl2anc 671 |
. . . 4
     UnifSp  
                                |
49 | 29 | adantr 471 |
. . . . 5
   UnifSp
  UnifOn    |
50 | 6 | adantr 471 |
. . . . 5
   UnifSp
    |
51 | | simpr 467 |
. . . . 5
   UnifSp
    |
52 | | simpll1 1048 |
. . . . . . . 8
    UnifOn 

   
UnifOn    |
53 | | simplr 767 |
. . . . . . . 8
    UnifOn 

   
  |
54 | | ustexsym 21241 |
. . . . . . . 8
  UnifOn   
 
   |
55 | 52, 53, 54 | syl2anc 671 |
. . . . . . 7
    UnifOn 

    
 
   |
56 | 52 | ad2antrr 737 |
. . . . . . . . . . . 12
      UnifOn 
    
    
UnifOn    |
57 | | simplr 767 |
. . . . . . . . . . . 12
      UnifOn 
    
    
  |
58 | | ustssxp 21230 |
. . . . . . . . . . . 12
  UnifOn       |
59 | 56, 57, 58 | syl2anc 671 |
. . . . . . . . . . 11
      UnifOn 
    
         |
60 | | simpll2 1049 |
. . . . . . . . . . . 12
    UnifOn 

   
 
     |
61 | 60 | 3anassrs 1235 |
. . . . . . . . . . 11
      UnifOn 
    
    
  |
62 | | ustneism 21249 |
. . . . . . . . . . 11
 
                 
    |
63 | 59, 61, 62 | syl2anc 671 |
. . . . . . . . . 10
      UnifOn 
    
                   
    |
64 | | simprl 769 |
. . . . . . . . . . . 12
      UnifOn 
    
     
  |
65 | 64 | coeq2d 4975 |
. . . . . . . . . . 11
      UnifOn 
    
            |
66 | | coss1 4968 |
. . . . . . . . . . . . . 14
       |
67 | | coss2 4969 |
. . . . . . . . . . . . . 14
       |
68 | 66, 67 | sstrd 3410 |
. . . . . . . . . . . . 13
       |
69 | 68 | ad2antll 740 |
. . . . . . . . . . . 12
      UnifOn 
    
      
    |
70 | | simpllr 774 |
. . . . . . . . . . . 12
      UnifOn 
    
      
  |
71 | 69, 70 | sstrd 3410 |
. . . . . . . . . . 11
      UnifOn 
    
      
  |
72 | 65, 71 | eqsstrd 3434 |
. . . . . . . . . 10
      UnifOn 
    
          |
73 | 63, 72 | sstrd 3410 |
. . . . . . . . 9
      UnifOn 
    
                     |
74 | 73 | ex 440 |
. . . . . . . 8
     UnifOn 

   
   
                  |
75 | 74 | reximdva 2839 |
. . . . . . 7
    UnifOn 

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

    
                |
77 | | ustexhalf 21236 |
. . . . . . 7
  UnifOn   
    |
78 | 77 | 3adant2 1028 |
. . . . . 6
  UnifOn 
 
    |
79 | 76, 78 | r19.29a 2900 |
. . . . 5
  UnifOn 
 
                |
80 | 49, 50, 51, 79 | syl3anc 1271 |
. . . 4
   UnifSp
  
                |
81 | 48, 80 | r19.29a 2900 |
. . 3
   UnifSp
                  |
82 | 81 | ralrimiva 2790 |
. 2
  UnifSp


                |
83 | | iscfilu 21314 |
. . 3
 UnifOn 
           CauFilu 
                
                 |
84 | 29, 83 | syl 17 |
. 2
  UnifSp

           CauFilu 
                
                 |
85 | 13, 82, 84 | mpbir2and 933 |
1
  UnifSp

          CauFilu    |