Step | Hyp | Ref
| Expression |
1 | | reltpos 5806 |
. . . 4
tpos  |
2 | 1 | brrelexi 4327 |
. . 3
 tpos    |
3 | 2 | a1i 9 |
. 2
  tpos     |
4 | | elex 2560 |
. . . 4
        |
5 | 4 | adantr 261 |
. . 3
             
  |
6 | 5 | a1i 9 |
. 2
  
           
   |
7 | | df-tpos 5801 |
. . . . . 6
tpos  
            |
8 | 7 | breqi 3761 |
. . . . 5
 tpos                   |
9 | | brcog 4445 |
. . . . 5
 
                                       |
10 | 8, 9 | syl5bb 181 |
. . . 4
 
  tpos                        |
11 | | funmpt 4881 |
. . . . . . . . . . 11

           |
12 | | funbrfv2b 5161 |
. . . . . . . . . . 11
                                                    
    |
13 | 11, 12 | ax-mp 7 |
. . . . . . . . . 10
               
                        
   |
14 | | vex 2554 |
. . . . . . . . . . . . . . . . 17
 |
15 | | snexg 3927 |
. . . . . . . . . . . . . . . . 17
  
  |
16 | 14, 15 | ax-mp 7 |
. . . . . . . . . . . . . . . 16
 
 |
17 | 16 | cnvex 4799 |
. . . . . . . . . . . . . . 15
  
 |
18 | 17 | uniex 4140 |
. . . . . . . . . . . . . 14
     |
19 | | eqid 2037 |
. . . . . . . . . . . . . 14
          

           |
20 | 18, 19 | dmmpti 4971 |
. . . . . . . . . . . . 13

         
      |
21 | 20 | eleq2i 2101 |
. . . . . . . . . . . 12
           
       |
22 | | eqcom 2039 |
. . . . . . . . . . . 12
               
 
               |
23 | 21, 22 | anbi12i 433 |
. . . . . . . . . . 11
  
         
 
            
                         |
24 | | snexg 3927 |
. . . . . . . . . . . . . . . 16
          |
25 | | cnvexg 4798 |
. . . . . . . . . . . . . . . 16
  
     |
26 | 24, 25 | syl 14 |
. . . . . . . . . . . . . . 15
           |
27 | | uniexg 4141 |
. . . . . . . . . . . . . . 15
       
  |
28 | 26, 27 | syl 14 |
. . . . . . . . . . . . . 14
         
  |
29 | | sneq 3378 |
. . . . . . . . . . . . . . . . 17
  
    |
30 | 29 | cnveqd 4454 |
. . . . . . . . . . . . . . . 16
         |
31 | 30 | unieqd 3582 |
. . . . . . . . . . . . . . 15
           |
32 | 31, 19 | fvmptg 5191 |
. . . . . . . . . . . . . 14
           
 
            
      |
33 | 28, 32 | mpdan 398 |
. . . . . . . . . . . . 13
                           |
34 | 33 | eqeq2d 2048 |
. . . . . . . . . . . 12
                     
       |
35 | 34 | pm5.32i 427 |
. . . . . . . . . . 11
                                    |
36 | 23, 35 | bitri 173 |
. . . . . . . . . 10
  
         
 
            
              |
37 | 13, 36 | bitri 173 |
. . . . . . . . 9
                           |
38 | | ancom 253 |
. . . . . . . . 9
           
             |
39 | 37, 38 | bitri 173 |
. . . . . . . 8
                  
        |
40 | 39 | anbi1i 431 |
. . . . . . 7
                                   |
41 | | anass 381 |
. . . . . . 7
      
             

           |
42 | 40, 41 | bitri 173 |
. . . . . 6
                      

           |
43 | 42 | exbii 1493 |
. . . . 5
                      
    
           |
44 | | exsimpr 1506 |
. . . . . . 7
        
                      |
45 | | exsimpl 1505 |
. . . . . . . 8
            
       |
46 | | 19.9v 1748 |
. . . . . . . 8
 
            |
47 | 45, 46 | sylib 127 |
. . . . . . 7
                   |
48 | 44, 47 | syl 14 |
. . . . . 6
        
        
       |
49 | | simpl 102 |
. . . . . 6
             
       |
50 | | breq1 3758 |
. . . . . . . . 9
    
            |
51 | 50 | anbi2d 437 |
. . . . . . . 8
    
 
                        |
52 | 51 | ceqsexgv 2667 |
. . . . . . 7
        
    
                         |
53 | 28, 52 | syl 14 |
. . . . . 6
              
                         |
54 | 48, 49, 53 | pm5.21nii 619 |
. . . . 5
        
                        |
55 | 43, 54 | bitri 173 |
. . . 4
                                   |
56 | 10, 55 | syl6bb 185 |
. . 3
 
  tpos                  |
57 | 56 | expcom 109 |
. 2
 
 tpos                   |
58 | 3, 6, 57 | pm5.21ndd 620 |
1
  tpos                  |