Step | Hyp | Ref
| Expression |
1 | | txdis1cn.f |
. . 3
     |
2 | | txdis1cn.j |
. . . . . . 7
 TopOn    |
3 | 2 | adantr 276 |
. . . . . 6
 
 TopOn    |
4 | | txdis1cn.k |
. . . . . . . 8
   |
5 | | toptopon2 13150 |
. . . . . . . 8

TopOn     |
6 | 4, 5 | sylib 122 |
. . . . . . 7
 TopOn     |
7 | 6 | adantr 276 |
. . . . . 6
 
 TopOn     |
8 | | txdis1cn.1 |
. . . . . 6
 
           |
9 | | cnf2 13338 |
. . . . . 6
  TopOn  TopOn                         |
10 | 3, 7, 8, 9 | syl3anc 1238 |
. . . . 5
 
              |
11 | | eqid 2177 |
. . . . . 6
             |
12 | 11 | fmpt 5661 |
. . . . 5
 
    

            |
13 | 10, 12 | sylibr 134 |
. . . 4
 
 
       |
14 | 13 | ralrimiva 2550 |
. . 3
  
       |
15 | | ffnov 5972 |
. . 3
            
        |
16 | 1, 14, 15 | sylanbrc 417 |
. 2
          |
17 | | cnvimass 4986 |
. . . . . . . 8
    
 |
18 | 1 | adantr 276 |
. . . . . . . . 9
 
     |
19 | | fndm 5310 |
. . . . . . . . 9
       |
20 | 18, 19 | syl 14 |
. . . . . . . 8
 
     |
21 | 17, 20 | sseqtrid 3205 |
. . . . . . 7
 
          |
22 | | relxp 4731 |
. . . . . . 7
   |
23 | | relss 4709 |
. . . . . . 7
          
        |
24 | 21, 22, 23 | mpisyl 1446 |
. . . . . 6
 
        |
25 | | elpreima 5630 |
. . . . . . . 8
           
                 |
26 | 18, 25 | syl 14 |
. . . . . . 7
 
         
                 |
27 | | opelxp 4652 |
. . . . . . . . 9
          |
28 | | df-ov 5871 |
. . . . . . . . . . 11
            |
29 | 28 | eqcomi 2181 |
. . . . . . . . . 10
      
     |
30 | 29 | eleq1i 2243 |
. . . . . . . . 9
       
      |
31 | 27, 30 | anbi12i 460 |
. . . . . . . 8
      
      
           |
32 | | simprll 537 |
. . . . . . . . . . . 12
     

     
  |
33 | | snelpwi 4208 |
. . . . . . . . . . . 12
  
   |
34 | 32, 33 | syl 14 |
. . . . . . . . . . 11
     

           |
35 | 11 | mptpreima 5117 |
. . . . . . . . . . . 12
                  |
36 | 8 | adantrr 479 |
. . . . . . . . . . . . . 14
 

            |
37 | 36 | ad2ant2r 509 |
. . . . . . . . . . . . 13
     

                |
38 | | simplr 528 |
. . . . . . . . . . . . 13
     

     
  |
39 | | cnima 13353 |
. . . . . . . . . . . . 13
          
             |
40 | 37, 38, 39 | syl2anc 411 |
. . . . . . . . . . . 12
     

                   |
41 | 35, 40 | eqeltrrid 2265 |
. . . . . . . . . . 11
     

           
  |
42 | | simprlr 538 |
. . . . . . . . . . . 12
     

        |
43 | | simprr 531 |
. . . . . . . . . . . 12
     

            |
44 | | vsnid 3623 |
. . . . . . . . . . . . . 14
   |
45 | | opelxp 4652 |
. . . . . . . . . . . . . 14
             
  

        |
46 | 44, 45 | mpbiran 940 |
. . . . . . . . . . . . 13
             
        |
47 | | oveq2 5876 |
. . . . . . . . . . . . . . 15
           |
48 | 47 | eleq1d 2246 |
. . . . . . . . . . . . . 14
     
       |
49 | 48 | elrab 2893 |
. . . . . . . . . . . . 13
      

       |
50 | 46, 49 | bitri 184 |
. . . . . . . . . . . 12
             

       |
51 | 42, 43, 50 | sylanbrc 417 |
. . . . . . . . . . 11
     

                     |
52 | | relxp 4731 |
. . . . . . . . . . . . 13
           |
53 | 52 | a1i 9 |
. . . . . . . . . . . 12
     

                  |
54 | | opelxp 4652 |
. . . . . . . . . . . . 13
             
  

        |
55 | 32 | snssd 3736 |
. . . . . . . . . . . . . . . . . 18
     

          |
56 | 55 | sselda 3155 |
. . . . . . . . . . . . . . . . 17
   
            
  |
57 | 56 | adantrr 479 |
. . . . . . . . . . . . . . . 16
   
            

      
  |
58 | | elrabi 2890 |
. . . . . . . . . . . . . . . . 17
         |
59 | 58 | ad2antll 491 |
. . . . . . . . . . . . . . . 16
   
            

      
  |
60 | 57, 59 | opelxpd 4655 |
. . . . . . . . . . . . . . 15
   
            

      
  
    |
61 | | df-ov 5871 |
. . . . . . . . . . . . . . . . 17
            |
62 | | elsni 3609 |
. . . . . . . . . . . . . . . . . . 19
     |
63 | 62 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . 18
   
            

      
  |
64 | 63 | oveq1d 5883 |
. . . . . . . . . . . . . . . . 17
   
            

      
          |
65 | 61, 64 | eqtr3id 2224 |
. . . . . . . . . . . . . . . 16
   
            

      
             |
66 | | oveq2 5876 |
. . . . . . . . . . . . . . . . . . . 20
           |
67 | 66 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . 19
     
       |
68 | 67 | elrab 2893 |
. . . . . . . . . . . . . . . . . 18
      

       |
69 | 68 | simprbi 275 |
. . . . . . . . . . . . . . . . 17
             |
70 | 69 | ad2antll 491 |
. . . . . . . . . . . . . . . 16
   
            

      
      |
71 | 65, 70 | eqeltrd 2254 |
. . . . . . . . . . . . . . 15
   
            

      
         |
72 | | elpreima 5630 |
. . . . . . . . . . . . . . . . 17
           
                 |
73 | 1, 72 | syl 14 |
. . . . . . . . . . . . . . . 16
         
                 |
74 | 73 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
   
            

      
                          |
75 | 60, 71, 74 | mpbir2and 944 |
. . . . . . . . . . . . . 14
   
            

      
  
       |
76 | 75 | ex 115 |
. . . . . . . . . . . . 13
     

         

                 |
77 | 54, 76 | biimtrid 152 |
. . . . . . . . . . . 12
     

                               |
78 | 53, 77 | relssdv 4714 |
. . . . . . . . . . 11
     

                       |
79 | | xpeq1 4636 |
. . . . . . . . . . . . . 14
           |
80 | 79 | eleq2d 2247 |
. . . . . . . . . . . . 13
        
  
       |
81 | 79 | sseq1d 3184 |
. . . . . . . . . . . . 13
                       |
82 | 80, 81 | anbi12d 473 |
. . . . . . . . . . . 12
                                       |
83 | | xpeq2 4637 |
. . . . . . . . . . . . . 14
                       |
84 | 83 | eleq2d 2247 |
. . . . . . . . . . . . 13
              
  
             |
85 | 83 | sseq1d 3184 |
. . . . . . . . . . . . 13
                                   |
86 | 84, 85 | anbi12d 473 |
. . . . . . . . . . . 12
                                                           |
87 | 82, 86 | rspc2ev 2856 |
. . . . . . . . . . 11
    
                                       
                |
88 | 34, 41, 51, 78, 87 | syl112anc 1242 |
. . . . . . . . . 10
     

      
                  |
89 | | vex 2740 |
. . . . . . . . . . . 12
 |
90 | | vex 2740 |
. . . . . . . . . . . 12
 |
91 | 89, 90 | opex 4225 |
. . . . . . . . . . 11
    |
92 | | eleq1 2240 |
. . . . . . . . . . . . 13
               |
93 | 92 | anbi1d 465 |
. . . . . . . . . . . 12
               
                 |
94 | 93 | 2rexbidv 2502 |
. . . . . . . . . . 11
       
  
                            |
95 | 91, 94 | elab 2881 |
. . . . . . . . . 10
     
 
           
  
                |
96 | 88, 95 | sylibr 134 |
. . . . . . . . 9
     

          
 
              |
97 | 96 | ex 115 |
. . . . . . . 8
 
              
 
               |
98 | 31, 97 | biimtrid 152 |
. . . . . . 7
 
               
  
   
  
            |
99 | 26, 98 | sylbid 150 |
. . . . . 6
 
                
  
            |
100 | 24, 99 | relssdv 4714 |
. . . . 5
 
                        |
101 | | ssabral 3226 |
. . . . 5
                     
         
  
          |
102 | 100, 101 | sylib 122 |
. . . 4
 
          
  
          |
103 | | txdis1cn.x |
. . . . . . 7
   |
104 | | distopon 13220 |
. . . . . . 7
 
TopOn    |
105 | 103, 104 | syl 14 |
. . . . . 6
  TopOn    |
106 | 105 | adantr 276 |
. . . . 5
 
 
TopOn    |
107 | 2 | adantr 276 |
. . . . 5
 
 TopOn    |
108 | | eltx 13392 |
. . . . 5
   TopOn  TopOn  
        
         
  
           |
109 | 106, 107,
108 | syl2anc 411 |
. . . 4
 
                                  |
110 | 102, 109 | mpbird 167 |
. . 3
 
           |
111 | 110 | ralrimiva 2550 |
. 2
            |
112 | | txtopon 13395 |
. . . 4
   TopOn  TopOn  
   TopOn      |
113 | 105, 2, 112 | syl2anc 411 |
. . 3
    TopOn      |
114 | | iscn 13330 |
. . 3
     TopOn    TopOn   
              
            |
115 | 113, 6, 114 | syl2anc 411 |
. 2
               
            |
116 | 16, 111, 115 | mpbir2and 944 |
1
        |