Step | Hyp | Ref
| Expression |
1 | | reltpos 6250 |
. . . 4
tpos  |
2 | 1 | brrelex1i 4669 |
. . 3
 tpos    |
3 | 2 | a1i 9 |
. 2
  tpos     |
4 | | elex 2748 |
. . . 4
        |
5 | 4 | adantr 276 |
. . 3
                |
6 | 5 | a1i 9 |
. 2
                  |
7 | | df-tpos 6245 |
. . . . . 6
tpos               |
8 | 7 | breqi 4009 |
. . . . 5
 tpos 
 
               |
9 | | brcog 4794 |
. . . . 5
 
                
                      |
10 | 8, 9 | bitrid 192 |
. . . 4
 
  tpos                        |
11 | | funmpt 5254 |
. . . . . . . . . . 11
            |
12 | | funbrfv2b 5560 |
. . . . . . . . . . 11
                                                         |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . 10
                                            |
14 | | vex 2740 |
. . . . . . . . . . . . . . . . 17
 |
15 | | snexg 4184 |
. . . . . . . . . . . . . . . . 17
  
  |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
 
 |
17 | 16 | cnvex 5167 |
. . . . . . . . . . . . . . 15
    |
18 | 17 | uniex 4437 |
. . . . . . . . . . . . . 14
     |
19 | | eqid 2177 |
. . . . . . . . . . . . . 14
                       |
20 | 18, 19 | dmmpti 5345 |
. . . . . . . . . . . . 13
                 |
21 | 20 | eleq2i 2244 |
. . . . . . . . . . . 12
           
       |
22 | | eqcom 2179 |
. . . . . . . . . . . 12
                                 |
23 | 21, 22 | anbi12i 460 |
. . . . . . . . . . 11
                                                     |
24 | | snexg 4184 |
. . . . . . . . . . . . . . . 16
          |
25 | | cnvexg 5166 |
. . . . . . . . . . . . . . . 16
        |
26 | 24, 25 | syl 14 |
. . . . . . . . . . . . . . 15
        
  |
27 | | uniexg 4439 |
. . . . . . . . . . . . . . 15
       
  |
28 | 26, 27 | syl 14 |
. . . . . . . . . . . . . 14
         
  |
29 | | sneq 3603 |
. . . . . . . . . . . . . . . . 17
  
    |
30 | 29 | cnveqd 4803 |
. . . . . . . . . . . . . . . 16
         |
31 | 30 | unieqd 3820 |
. . . . . . . . . . . . . . 15
           |
32 | 31, 19 | fvmptg 5592 |
. . . . . . . . . . . . . 14
           
                     |
33 | 28, 32 | mpdan 421 |
. . . . . . . . . . . . 13
                           |
34 | 33 | eqeq2d 2189 |
. . . . . . . . . . . 12
                     
       |
35 | 34 | pm5.32i 454 |
. . . . . . . . . . 11
                      
     
       |
36 | 23, 35 | bitri 184 |
. . . . . . . . . 10
                                          |
37 | 13, 36 | bitri 184 |
. . . . . . . . 9
                   
       |
38 | | ancom 266 |
. . . . . . . . 9
           
             |
39 | 37, 38 | bitri 184 |
. . . . . . . 8
                           |
40 | 39 | anbi1i 458 |
. . . . . . 7
                 
                 |
41 | | anass 401 |
. . . . . . 7
      
        
                 |
42 | 40, 41 | bitri 184 |
. . . . . 6
                 
                 |
43 | 42 | exbii 1605 |
. . . . 5
                   
       
           |
44 | | exsimpr 1618 |
. . . . . . 7
                               |
45 | | exsimpl 1617 |
. . . . . . . 8
            
       |
46 | | 19.9v 1871 |
. . . . . . . 8
      
       |
47 | 45, 46 | sylib 122 |
. . . . . . 7
           
       |
48 | 44, 47 | syl 14 |
. . . . . 6
                         |
49 | | simpl 109 |
. . . . . 6
                     |
50 | | breq1 4006 |
. . . . . . . . 9
    
  
         |
51 | 50 | anbi2d 464 |
. . . . . . . 8
    
         
                |
52 | 51 | ceqsexgv 2866 |
. . . . . . 7
             
        
                |
53 | 28, 52 | syl 14 |
. . . . . 6
              
        
                |
54 | 48, 49, 53 | pm5.21nii 704 |
. . . . 5
                                 |
55 | 43, 54 | bitri 184 |
. . . 4
                   
               |
56 | 10, 55 | bitrdi 196 |
. . 3
 
  tpos                  |
57 | 56 | expcom 116 |
. 2
 
 tpos 
                 |
58 | 3, 6, 57 | pm5.21ndd 705 |
1
  tpos 
                |