Proof of Theorem dfcon2
Step | Hyp | Ref
| Expression |
1 | | eqid 2451 |
. . . . . 6
   |
2 | | simpll 760 |
. . . . . 6
   
         |
3 | | simplrl 770 |
. . . . . 6
   
         |
4 | | simpr1 1014 |
. . . . . 6
   
         |
5 | | simplrr 771 |
. . . . . 6
   
         |
6 | | simpr2 1015 |
. . . . . 6
   
         |
7 | | simpr3 1016 |
. . . . . 6
   
       
   |
8 | 1, 2, 3, 4, 5, 6, 7 | conndisj 20431 |
. . . . 5
   
            |
9 | 8 | ex 436 |
. . . 4
  
      
      |
10 | 9 | ralrimivva 2809 |
. . 3
 

    
      |
11 | | topontop 19941 |
. . . 4
 TopOn 
  |
12 | 1 | cldopn 20046 |
. . . . . . . . . . . . . 14
    
     |
13 | 12 | adantl 468 |
. . . . . . . . . . . . 13
 
          |
14 | | df-3an 987 |
. . . . . . . . . . . . . . . 16
    
  

    |
15 | | ineq2 3628 |
. . . . . . . . . . . . . . . . . . 19
    
        |
16 | | disjdif 3839 |
. . . . . . . . . . . . . . . . . . 19
      |
17 | 15, 16 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . 18
    
   |
18 | 17 | biantrud 510 |
. . . . . . . . . . . . . . . . 17
      
   
     |
19 | | neeq1 2686 |
. . . . . . . . . . . . . . . . . 18
    
      |
20 | 19 | anbi2d 710 |
. . . . . . . . . . . . . . . . 17
      
        |
21 | 18, 20 | bitr3d 259 |
. . . . . . . . . . . . . . . 16
        
 
        |
22 | 14, 21 | syl5bb 261 |
. . . . . . . . . . . . . . 15
        
        |
23 | | uneq2 3582 |
. . . . . . . . . . . . . . . . 17
             |
24 | | undif2 3843 |
. . . . . . . . . . . . . . . . 17
         |
25 | 23, 24 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
           |
26 | 25 | neeq1d 2683 |
. . . . . . . . . . . . . . 15
               |
27 | 22, 26 | imbi12d 322 |
. . . . . . . . . . . . . 14
       
                    |
28 | 27 | rspcv 3146 |
. . . . . . . . . . . . 13
                  
          |
29 | 13, 28 | syl 17 |
. . . . . . . . . . . 12
 
                   
          |
30 | 1 | cldss 20044 |
. . . . . . . . . . . . . . . . 17
    
   |
31 | 30 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
        |
32 | | ssequn1 3604 |
. . . . . . . . . . . . . . . 16
 
      |
33 | 31, 32 | sylib 200 |
. . . . . . . . . . . . . . 15
 
           |
34 | | ssdif0 3823 |
. . . . . . . . . . . . . . . 16
 
     |
35 | | idd 25 |
. . . . . . . . . . . . . . . . . 18
 
           |
36 | 35, 31 | jctild 546 |
. . . . . . . . . . . . . . . . 17
 
              |
37 | | eqss 3447 |
. . . . . . . . . . . . . . . . 17
 
      |
38 | 36, 37 | syl6ibr 231 |
. . . . . . . . . . . . . . . 16
 
           |
39 | 34, 38 | syl5bir 222 |
. . . . . . . . . . . . . . 15
 
             |
40 | 33, 39 | embantd 56 |
. . . . . . . . . . . . . 14
 
                   |
41 | 40 | orim2d 851 |
. . . . . . . . . . . . 13
 
                       |
42 | | impexp 448 |
. . . . . . . . . . . . . 14
    
      

  
         |
43 | | df-ne 2624 |
. . . . . . . . . . . . . . . 16

  |
44 | | id 22 |
. . . . . . . . . . . . . . . . . 18
         
  
        |
45 | 44 | necon4d 2648 |
. . . . . . . . . . . . . . . . 17
         
           |
46 | | id 22 |
. . . . . . . . . . . . . . . . . 18
                     |
47 | 46 | necon3d 2645 |
. . . . . . . . . . . . . . . . 17
                     |
48 | 45, 47 | impbii 191 |
. . . . . . . . . . . . . . . 16
                     |
49 | 43, 48 | imbi12i 328 |
. . . . . . . . . . . . . . 15
           

            |
50 | | pm4.64 374 |
. . . . . . . . . . . . . . 15
        
          
     |
51 | 49, 50 | bitri 253 |
. . . . . . . . . . . . . 14
           
             |
52 | 42, 51 | bitri 253 |
. . . . . . . . . . . . 13
    
      
             |
53 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
54 | 53 | elpr 3986 |
. . . . . . . . . . . . 13
    
     |
55 | 41, 52, 54 | 3imtr4g 274 |
. . . . . . . . . . . 12
 
           
            |
56 | 29, 55 | syld 45 |
. . . . . . . . . . 11
 
                       |
57 | 56 | ex 436 |
. . . . . . . . . 10
       
  
              |
58 | 57 | com23 81 |
. . . . . . . . 9
  
  
          
 
      |
59 | 58 | imim2d 54 |
. . . . . . . 8
      
      

    
 
       |
60 | | elin 3617 |
. . . . . . . . . 10
               |
61 | 60 | imbi1i 327 |
. . . . . . . . 9
            
 
    
       |
62 | | impexp 448 |
. . . . . . . . 9
  
                        |
63 | 61, 62 | bitri 253 |
. . . . . . . 8
            

    
 
      |
64 | 59, 63 | syl6ibr 231 |
. . . . . . 7
      
      
               |
65 | 64 | alimdv 1763 |
. . . . . 6
    

    
                      |
66 | | df-ral 2742 |
. . . . . 6
 

    
   
      
         |
67 | | dfss2 3421 |
. . . . . 6
        
                  |
68 | 65, 66, 67 | 3imtr4g 274 |
. . . . 5
  

  
           
       |
69 | 1 | iscon2 20429 |
. . . . . 6

              |
70 | 69 | baib 914 |
. . . . 5
 
             |
71 | 68, 70 | sylibrd 238 |
. . . 4
  

  
         |
72 | 11, 71 | syl 17 |
. . 3
 TopOn 
 

    
       |
73 | 10, 72 | impbid2 208 |
. 2
 TopOn 
  
  
         |
74 | | toponuni 19942 |
. . . . 5
 TopOn 
   |
75 | 74 | neeq2d 2684 |
. . . 4
 TopOn 
  
      |
76 | 75 | imbi2d 318 |
. . 3
 TopOn 
     
  
    
       |
77 | 76 | 2ralbidv 2832 |
. 2
 TopOn 
 

    
  


    
       |
78 | 73, 77 | bitr4d 260 |
1
 TopOn 
  
  
        |