Step | Hyp | Ref
| Expression |
1 | | relres 5132 |
. 2
  Image
Singleton      |
2 | | vex 3048 |
. . . . . . 7
 |
3 | 2 | brres 5111 |
. . . . . 6
    Image
Singleton          Image Singleton       |
4 | 3 | simplbi 462 |
. . . . 5
    Image
Singleton     
    |
5 | | vex 3048 |
. . . . . . . 8
 |
6 | 5 | brres 5111 |
. . . . . . 7
    Image
Singleton          Image Singleton       |
7 | | ancom 452 |
. . . . . . . 8
   
 Image
Singleton       Image Singleton         |
8 | | funpartlem 30709 |
. . . . . . . . 9
  Image
Singleton   
            |
9 | 8 | anbi1i 701 |
. . . . . . . 8
   Image
Singleton      
                |
10 | 7, 9 | bitri 253 |
. . . . . . 7
   
 Image
Singleton                     |
11 | 6, 10 | bitri 253 |
. . . . . 6
    Image
Singleton                      |
12 | | df-br 4403 |
. . . . . . . . . . 11
  
  
  |
13 | | df-br 4403 |
. . . . . . . . . . 11
  
  
  |
14 | 12, 13 | anbi12i 703 |
. . . . . . . . . 10
      
          |
15 | | vex 3048 |
. . . . . . . . . . . 12
 |
16 | 15, 5 | elimasn 5193 |
. . . . . . . . . . 11
            |
17 | 15, 2 | elimasn 5193 |
. . . . . . . . . . 11
            |
18 | 16, 17 | anbi12i 703 |
. . . . . . . . . 10
       
      
          |
19 | 14, 18 | bitr4i 256 |
. . . . . . . . 9
      
      
         |
20 | | eleq2 2518 |
. . . . . . . . . . 11
                     |
21 | | eleq2 2518 |
. . . . . . . . . . 11
                     |
22 | 20, 21 | anbi12d 717 |
. . . . . . . . . 10
                                 |
23 | | elsn 3982 |
. . . . . . . . . . 11
     |
24 | | elsn 3982 |
. . . . . . . . . . 11
     |
25 | | equtr2 1869 |
. . . . . . . . . . 11
 
   |
26 | 23, 24, 25 | syl2anb 482 |
. . . . . . . . . 10
         |
27 | 22, 26 | syl6bi 232 |
. . . . . . . . 9
                           |
28 | 19, 27 | syl5bi 221 |
. . . . . . . 8
               
   |
29 | 28 | exlimiv 1776 |
. . . . . . 7
                     |
30 | 29 | impl 626 |
. . . . . 6
                     |
31 | 11, 30 | sylanb 475 |
. . . . 5
     Image Singleton           |
32 | 4, 31 | sylan2 477 |
. . . 4
     Image Singleton         Image Singleton         |
33 | 32 | gen2 1670 |
. . 3
         Image
Singleton       
 Image
Singleton         |
34 | 33 | ax-gen 1669 |
. 2
           Image Singleton       
 Image
Singleton         |
35 | | df-funpart 30640 |
. . . 4
Funpart   Image
Singleton      |
36 | 35 | funeqi 5602 |
. . 3
 Funpart   Image Singleton       |
37 | | dffun2 5592 |
. . 3
   Image
Singleton     
  Image Singleton                Image Singleton         Image Singleton           |
38 | 36, 37 | bitri 253 |
. 2
 Funpart    Image Singleton                Image Singleton         Image Singleton           |
39 | 1, 34, 38 | mpbir2an 931 |
1
Funpart |