Step | Hyp | Ref
| Expression |
1 | | nfv 1769 |
. . . . 5

 |
2 | | nfab1 2614 |
. . . . 5
  

    |
3 | | nfcv 2612 |
. . . . 5
   |
4 | | abid 2459 |
. . . . . . . . . . 11
  
  

    |
5 | | df-rex 2762 |
. . . . . . . . . . 11
            |
6 | 4, 5 | bitri 257 |
. . . . . . . . . 10
  
  
        |
7 | | eqid 2471 |
. . . . . . . . . . . . . . 15
     |
8 | | snex 4641 |
. . . . . . . . . . . . . . . . . 18
   |
9 | | snelpwi 4645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      |
10 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
 
    |
11 | 9, 10 | syl5ibr 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
    |
12 | 11 | imdistani 704 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
13 | 12 | anim2i 579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
  
     |
14 | 13 | 3impb 1227 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
        |
15 | | 3anass 1011 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

        |
16 | 14, 15 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . 22
     
      |
17 | | snfi 7668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
18 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
19 | 17, 18 | mpbiri 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
20 | | difinf 7859 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
21 | 19, 20 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
   |
22 | 21 | orcd 399 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
    |
23 | 22 | anim2i 579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
   
     
     |
24 | 23 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
         
      |
25 | 24 | 3impa 1226 |
. . . . . . . . . . . . . . . . . . . . . 22
          
      |
26 | 16, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
         
      |
27 | | topdifinf.t |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
    |
28 | 27 | rabeq2i 3028 |
. . . . . . . . . . . . . . . . . . . . 21

     
     |
29 | 26, 28 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . 20
       |
30 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . 21
         |
31 | 30 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . 20
     
 
   |
32 | 29, 31 | mpbid 215 |
. . . . . . . . . . . . . . . . . . 19
         |
33 | 32 | sbcth 3270 |
. . . . . . . . . . . . . . . . . 18
       ![]. ].](_drbrack.gif)  
 
      |
34 | 8, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
    ![]. ].](_drbrack.gif)    
     |
35 | | sbcimg 3297 |
. . . . . . . . . . . . . . . . . 18
        ![]. ].](_drbrack.gif)    
   
     ![]. ].](_drbrack.gif)   
     ![]. ].](_drbrack.gif)       |
36 | 8, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     ![]. ].](_drbrack.gif)  
  
 
      ![]. ].](_drbrack.gif) 
       ![]. ].](_drbrack.gif)      |
37 | 34, 36 | mpbi 213 |
. . . . . . . . . . . . . . . 16
     ![]. ].](_drbrack.gif)   
     ![]. ].](_drbrack.gif)     |
38 | | sbc3an 3313 |
. . . . . . . . . . . . . . . . . 18
     ![]. ].](_drbrack.gif)   
     
    ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
   |
39 | | sbcg 3321 |
. . . . . . . . . . . . . . . . . . . 20
       
   |
40 | 8, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
       |
41 | 40 | 3anbi1i 1221 |
. . . . . . . . . . . . . . . . . 18
     
    ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
   |
42 | | eqsbc3 3295 |
. . . . . . . . . . . . . . . . . . . 20
        ![]. ].](_drbrack.gif)
         |
43 | 8, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
     ![]. ].](_drbrack.gif)  
 
    |
44 | 43 | 3anbi2i 1222 |
. . . . . . . . . . . . . . . . . 18
      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)           ![]. ].](_drbrack.gif)
   |
45 | 38, 41, 44 | 3bitri 279 |
. . . . . . . . . . . . . . . . 17
     ![]. ].](_drbrack.gif)   
          ![]. ].](_drbrack.gif)    |
46 | | sbcg 3321 |
. . . . . . . . . . . . . . . . . . 19
        ![]. ].](_drbrack.gif)
   |
47 | 8, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
     ![]. ].](_drbrack.gif)   |
48 | 47 | 3anbi3i 1223 |
. . . . . . . . . . . . . . . . 17
          ![]. ].](_drbrack.gif)          |
49 | 45, 48 | bitri 257 |
. . . . . . . . . . . . . . . 16
     ![]. ].](_drbrack.gif)   
     
   |
50 | | sbcg 3321 |
. . . . . . . . . . . . . . . . 17
        ![]. ].](_drbrack.gif)        |
51 | 8, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
     ![]. ].](_drbrack.gif)  
 
  |
52 | 37, 49, 51 | 3imtr3i 273 |
. . . . . . . . . . . . . . 15
     
     |
53 | 7, 52 | mp3an2 1378 |
. . . . . . . . . . . . . 14
       |
54 | 53 | ex 441 |
. . . . . . . . . . . . 13
       |
55 | 54 | pm4.71d 646 |
. . . . . . . . . . . 12
 

      |
56 | 55 | anbi1d 719 |
. . . . . . . . . . 11
  
  
    
      |
57 | 56 | exbidv 1776 |
. . . . . . . . . 10
              
      |
58 | 6, 57 | syl5bb 265 |
. . . . . . . . 9
   
  
      
      |
59 | | anass 661 |
. . . . . . . . . . 11
                   |
60 | 59 | exbii 1726 |
. . . . . . . . . 10
       
        
      |
61 | | exsimpr 1738 |
. . . . . . . . . 10
      
        
     |
62 | 60, 61 | sylbi 200 |
. . . . . . . . 9
       
       
     |
63 | 58, 62 | syl6bi 236 |
. . . . . . . 8
   
  
           |
64 | | ancom 457 |
. . . . . . . . . 10
      
        |
65 | | eleq1 2537 |
. . . . . . . . . . 11
         |
66 | 65 | pm5.32i 649 |
. . . . . . . . . 10
    
        |
67 | 64, 66 | bitr4i 260 |
. . . . . . . . 9
      
  
   |
68 | 67 | exbii 1726 |
. . . . . . . 8
     
  
        |
69 | 63, 68 | syl6ib 234 |
. . . . . . 7
   
  
         |
70 | | exsimpr 1738 |
. . . . . . 7
     
    |
71 | 69, 70 | syl6 33 |
. . . . . 6
   
  

   |
72 | | ax5e 1768 |
. . . . . 6
    |
73 | 71, 72 | syl6 33 |
. . . . 5
   
  
   |
74 | 1, 2, 3, 73 | ssrd 3423 |
. . . 4
  
     |
75 | | eqid 2471 |
. . . . 5
 
  
 
    |
76 | 75 | dissneq 31813 |
. . . 4
   
   TopOn  
   |
77 | 74, 76 | sylan 479 |
. . 3
  TopOn  
   |
78 | | nfielex 7818 |
. . . . 5
    |
79 | 78 | adantr 472 |
. . . 4
  TopOn   
  |
80 | | difss 3549 |
. . . . . . 7
   
 |
81 | | elfvex 5906 |
. . . . . . . 8
 TopOn 
  |
82 | | difexg 4545 |
. . . . . . . 8
       |
83 | | elpwg 3950 |
. . . . . . . 8
          
       |
84 | 81, 82, 83 | 3syl 18 |
. . . . . . 7
 TopOn 
             |
85 | 80, 84 | mpbiri 241 |
. . . . . 6
 TopOn 
       |
86 | 85 | adantl 473 |
. . . . 5
  TopOn          |
87 | | difinf 7859 |
. . . . . . . . . . . 12
    
      |
88 | 17, 87 | mpan2 685 |
. . . . . . . . . . 11
       |
89 | | 0fin 7817 |
. . . . . . . . . . . 12
 |
90 | | eleq1 2537 |
. . . . . . . . . . . 12
         
   |
91 | 89, 90 | mpbiri 241 |
. . . . . . . . . . 11
           |
92 | 88, 91 | nsyl 125 |
. . . . . . . . . 10
       |
93 | 92 | ad2antrl 742 |
. . . . . . . . 9
  
TopOn   
      |
94 | | ssnid 3989 |
. . . . . . . . . . . . . 14
   |
95 | | inelcm 3823 |
. . . . . . . . . . . . . 14
 
         |
96 | 94, 95 | mpan2 685 |
. . . . . . . . . . . . 13
       |
97 | | disj4 3817 |
. . . . . . . . . . . . . 14
     
     |
98 | 97 | necon2abii 2693 |
. . . . . . . . . . . . 13
           |
99 | 96, 98 | sylibr 217 |
. . . . . . . . . . . 12
    
  |
100 | 99 | pssned 3517 |
. . . . . . . . . . 11
       |
101 | 100 | adantr 472 |
. . . . . . . . . 10
  
TopOn          |
102 | 101 | neneqd 2648 |
. . . . . . . . 9
  
TopOn   
      |
103 | 93, 102 | jca 541 |
. . . . . . . 8
  
TopOn         
      |
104 | | pm4.56 503 |
. . . . . . . 8
     
         
       |
105 | 103, 104 | sylib 201 |
. . . . . . 7
  
TopOn   
            |
106 | 85 | biantrurd 516 |
. . . . . . . . . 10
 TopOn 
            
                       
          |
107 | | difeq2 3534 |
. . . . . . . . . . . . . 14
               |
108 | 107 | eleq1d 2533 |
. . . . . . . . . . . . 13
                 |
109 | 108 | notbid 301 |
. . . . . . . . . . . 12
                 |
110 | | eqeq1 2475 |
. . . . . . . . . . . . 13
             |
111 | | eqeq1 2475 |
. . . . . . . . . . . . 13
             |
112 | 110, 111 | orbi12d 724 |
. . . . . . . . . . . 12
      

             |
113 | 109, 112 | orbi12d 724 |
. . . . . . . . . . 11
         
 
 
         
         |
114 | 113, 27 | elrab2 3186 |
. . . . . . . . . 10
                      
         |
115 | 106, 114 | syl6rbbr 272 |
. . . . . . . . 9
 TopOn 
    
 
         
         |
116 | | dfin4 3674 |
. . . . . . . . . . 11
           |
117 | | inss2 3644 |
. . . . . . . . . . . 12
   
   |
118 | | ssfi 7810 |
. . . . . . . . . . . 12
                 |
119 | 17, 117, 118 | mp2an 686 |
. . . . . . . . . . 11
     |
120 | 116, 119 | eqeltrri 2546 |
. . . . . . . . . 10
       |
121 | | biortn 413 |
. . . . . . . . . 10
                             
         |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . 9
          
 
         
        |
123 | 115, 122 | syl6bbr 271 |
. . . . . . . 8
 TopOn 
    
             |
124 | 123 | ad2antll 743 |
. . . . . . 7
  
TopOn        
             |
125 | 105, 124 | mtbird 308 |
. . . . . 6
  
TopOn   
      |
126 | 125 | expcom 442 |
. . . . 5
  TopOn           |
127 | | nelneq2 2574 |
. . . . . 6
       
   
   |
128 | | eqcom 2478 |
. . . . . 6
 
   |
129 | 127, 128 | sylnibr 312 |
. . . . 5
       
   
   |
130 | 86, 126, 129 | syl6an 554 |
. . . 4
  TopOn        |
131 | 79, 130 | exellimddv 31818 |
. . 3
  TopOn  
   |
132 | 77, 131 | pm2.65da 586 |
. 2
 TopOn    |
133 | 132 | con4i 135 |
1
 TopOn 
  |