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

 |
2 | | nfab1 2593 |
. . . . 5
  

    |
3 | | nfcv 2591 |
. . . . 5
   |
4 | | abid 2438 |
. . . . . . . . . . 11
  
  

    |
5 | | df-rex 2742 |
. . . . . . . . . . 11
            |
6 | 4, 5 | bitri 253 |
. . . . . . . . . 10
  
  
        |
7 | | eqid 2450 |
. . . . . . . . . . . . . . 15
     |
8 | | snex 4640 |
. . . . . . . . . . . . . . . . . 18
   |
9 | | snelpwi 4644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      |
10 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
 
    |
11 | 9, 10 | syl5ibr 225 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
    |
12 | 11 | imdistani 695 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
13 | 12 | anim2i 572 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
  
     |
14 | 13 | 3impb 1203 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
        |
15 | | 3anass 988 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

        |
16 | 14, 15 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . 22
     
      |
17 | | snfi 7647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
18 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
19 | 17, 18 | mpbiri 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
20 | | difinf 7838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
21 | 19, 20 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
   |
22 | 21 | orcd 394 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
    |
23 | 22 | anim2i 572 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
   
     
     |
24 | 23 | ancoms 455 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
         
      |
25 | 24 | 3impa 1202 |
. . . . . . . . . . . . . . . . . . . . . 22
          
      |
26 | 16, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
         
      |
27 | | topdifinf.t |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
 
    |
28 | 27 | rabeq2i 3041 |
. . . . . . . . . . . . . . . . . . . . 21

     
     |
29 | 26, 28 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . 20
       |
30 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . 21
         |
31 | 30 | 3ad2ant2 1029 |
. . . . . . . . . . . . . . . . . . . 20
     
 
   |
32 | 29, 31 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
         |
33 | 32 | sbcth 3281 |
. . . . . . . . . . . . . . . . . 18
       ![]. ].](_drbrack.gif)  
 
      |
34 | 8, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
    ![]. ].](_drbrack.gif)    
     |
35 | | sbcimg 3308 |
. . . . . . . . . . . . . . . . . 18
        ![]. ].](_drbrack.gif)    
   
     ![]. ].](_drbrack.gif)   
     ![]. ].](_drbrack.gif)       |
36 | 8, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     ![]. ].](_drbrack.gif)  
  
 
      ![]. ].](_drbrack.gif) 
       ![]. ].](_drbrack.gif)      |
37 | 34, 36 | mpbi 212 |
. . . . . . . . . . . . . . . 16
     ![]. ].](_drbrack.gif)   
     ![]. ].](_drbrack.gif)     |
38 | | sbc3an 3324 |
. . . . . . . . . . . . . . . . . 18
     ![]. ].](_drbrack.gif)   
     
    ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
   |
39 | | sbcg 3332 |
. . . . . . . . . . . . . . . . . . . 20
       
   |
40 | 8, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
       |
41 | 40 | 3anbi1i 1198 |
. . . . . . . . . . . . . . . . . 18
     
    ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
   |
42 | | eqsbc3 3306 |
. . . . . . . . . . . . . . . . . . . 20
        ![]. ].](_drbrack.gif)
         |
43 | 8, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
     ![]. ].](_drbrack.gif)  
 
    |
44 | 43 | 3anbi2i 1199 |
. . . . . . . . . . . . . . . . . 18
      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)           ![]. ].](_drbrack.gif)
   |
45 | 38, 41, 44 | 3bitri 275 |
. . . . . . . . . . . . . . . . 17
     ![]. ].](_drbrack.gif)   
          ![]. ].](_drbrack.gif)    |
46 | | sbcg 3332 |
. . . . . . . . . . . . . . . . . . 19
        ![]. ].](_drbrack.gif)
   |
47 | 8, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
     ![]. ].](_drbrack.gif)   |
48 | 47 | 3anbi3i 1200 |
. . . . . . . . . . . . . . . . 17
          ![]. ].](_drbrack.gif)          |
49 | 45, 48 | bitri 253 |
. . . . . . . . . . . . . . . 16
     ![]. ].](_drbrack.gif)   
     
   |
50 | | sbcg 3332 |
. . . . . . . . . . . . . . . . 17
        ![]. ].](_drbrack.gif)        |
51 | 8, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
     ![]. ].](_drbrack.gif)  
 
  |
52 | 37, 49, 51 | 3imtr3i 269 |
. . . . . . . . . . . . . . 15
     
     |
53 | 7, 52 | mp3an2 1351 |
. . . . . . . . . . . . . 14
       |
54 | 53 | ex 436 |
. . . . . . . . . . . . 13
       |
55 | 54 | pm4.71d 639 |
. . . . . . . . . . . 12
 

      |
56 | 55 | anbi1d 710 |
. . . . . . . . . . 11
  
  
    
      |
57 | 56 | exbidv 1767 |
. . . . . . . . . 10
              
      |
58 | 6, 57 | syl5bb 261 |
. . . . . . . . 9
   
  
      
      |
59 | | anass 654 |
. . . . . . . . . . 11
                   |
60 | 59 | exbii 1717 |
. . . . . . . . . 10
       
        
      |
61 | | exsimpr 1729 |
. . . . . . . . . 10
      
        
     |
62 | 60, 61 | sylbi 199 |
. . . . . . . . 9
       
       
     |
63 | 58, 62 | syl6bi 232 |
. . . . . . . 8
   
  
           |
64 | | ancom 452 |
. . . . . . . . . 10
      
        |
65 | | eleq1 2516 |
. . . . . . . . . . 11
         |
66 | 65 | pm5.32i 642 |
. . . . . . . . . 10
    
        |
67 | 64, 66 | bitr4i 256 |
. . . . . . . . 9
      
  
   |
68 | 67 | exbii 1717 |
. . . . . . . 8
     
  
        |
69 | 63, 68 | syl6ib 230 |
. . . . . . 7
   
  
         |
70 | | exsimpr 1729 |
. . . . . . 7
     
    |
71 | 69, 70 | syl6 34 |
. . . . . 6
   
  

   |
72 | | ax5e 1759 |
. . . . . 6
    |
73 | 71, 72 | syl6 34 |
. . . . 5
   
  
   |
74 | 1, 2, 3, 73 | ssrd 3436 |
. . . 4
  
     |
75 | | eqid 2450 |
. . . . 5
 
  
 
    |
76 | 75 | dissneq 31736 |
. . . 4
   
   TopOn  
   |
77 | 74, 76 | sylan 474 |
. . 3
  TopOn  
   |
78 | | nfielex 7797 |
. . . . 5
    |
79 | 78 | adantr 467 |
. . . 4
  TopOn   
  |
80 | | difss 3559 |
. . . . . . 7
   
 |
81 | | elfvex 5890 |
. . . . . . . 8
 TopOn 
  |
82 | | difexg 4550 |
. . . . . . . 8
       |
83 | | elpwg 3958 |
. . . . . . . 8
          
       |
84 | 81, 82, 83 | 3syl 18 |
. . . . . . 7
 TopOn 
             |
85 | 80, 84 | mpbiri 237 |
. . . . . 6
 TopOn 
       |
86 | 85 | adantl 468 |
. . . . 5
  TopOn          |
87 | | difinf 7838 |
. . . . . . . . . . . 12
    
      |
88 | 17, 87 | mpan2 676 |
. . . . . . . . . . 11
       |
89 | | 0fin 7796 |
. . . . . . . . . . . 12
 |
90 | | eleq1 2516 |
. . . . . . . . . . . 12
         
   |
91 | 89, 90 | mpbiri 237 |
. . . . . . . . . . 11
           |
92 | 88, 91 | nsyl 125 |
. . . . . . . . . 10
       |
93 | 92 | ad2antrl 733 |
. . . . . . . . 9
  
TopOn   
      |
94 | | ssnid 3996 |
. . . . . . . . . . . . . 14
   |
95 | | inelcm 3818 |
. . . . . . . . . . . . . 14
 
         |
96 | 94, 95 | mpan2 676 |
. . . . . . . . . . . . 13
       |
97 | | disj4 3812 |
. . . . . . . . . . . . . 14
     
     |
98 | 97 | necon2abii 2673 |
. . . . . . . . . . . . 13
           |
99 | 96, 98 | sylibr 216 |
. . . . . . . . . . . 12
    
  |
100 | 99 | pssned 3530 |
. . . . . . . . . . 11
       |
101 | 100 | adantr 467 |
. . . . . . . . . 10
  
TopOn          |
102 | 101 | neneqd 2628 |
. . . . . . . . 9
  
TopOn   
      |
103 | 93, 102 | jca 535 |
. . . . . . . 8
  
TopOn         
      |
104 | | pm4.56 498 |
. . . . . . . 8
     
         
       |
105 | 103, 104 | sylib 200 |
. . . . . . 7
  
TopOn   
            |
106 | 85 | biantrurd 511 |
. . . . . . . . . 10
 TopOn 
            
                       
          |
107 | | difeq2 3544 |
. . . . . . . . . . . . . 14
               |
108 | 107 | eleq1d 2512 |
. . . . . . . . . . . . 13
                 |
109 | 108 | notbid 296 |
. . . . . . . . . . . 12
                 |
110 | | eqeq1 2454 |
. . . . . . . . . . . . 13
             |
111 | | eqeq1 2454 |
. . . . . . . . . . . . 13
             |
112 | 110, 111 | orbi12d 715 |
. . . . . . . . . . . 12
      

             |
113 | 109, 112 | orbi12d 715 |
. . . . . . . . . . 11
         
 
 
         
         |
114 | 113, 27 | elrab2 3197 |
. . . . . . . . . 10
                      
         |
115 | 106, 114 | syl6rbbr 268 |
. . . . . . . . 9
 TopOn 
    
 
         
         |
116 | | dfin4 3682 |
. . . . . . . . . . 11
           |
117 | | inss2 3652 |
. . . . . . . . . . . 12
   
   |
118 | | ssfi 7789 |
. . . . . . . . . . . 12
                 |
119 | 17, 117, 118 | mp2an 677 |
. . . . . . . . . . 11
     |
120 | 116, 119 | eqeltrri 2525 |
. . . . . . . . . 10
       |
121 | | biortn 408 |
. . . . . . . . . 10
                             
         |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . 9
          
 
         
        |
123 | 115, 122 | syl6bbr 267 |
. . . . . . . 8
 TopOn 
    
             |
124 | 123 | ad2antll 734 |
. . . . . . 7
  
TopOn        
             |
125 | 105, 124 | mtbird 303 |
. . . . . 6
  
TopOn   
      |
126 | 125 | expcom 437 |
. . . . 5
  TopOn           |
127 | | nelneq2 2553 |
. . . . . 6
       
   
   |
128 | | eqcom 2457 |
. . . . . 6
 
   |
129 | 127, 128 | sylnibr 307 |
. . . . 5
       
   
   |
130 | 86, 126, 129 | syl6an 548 |
. . . 4
  TopOn        |
131 | 79, 130 | exellimddv 31741 |
. . 3
  TopOn  
   |
132 | 77, 131 | pm2.65da 579 |
. 2
 TopOn    |
133 | 132 | con4i 134 |
1
 TopOn 
  |