Step | Hyp | Ref
| Expression |
1 | | fpwrelmapffslem.4 |
. . 3
     
        |
2 | | relopab 4965 |
. . . 4
            |
3 | | releq 4922 |
. . . 4
     
          

         |
4 | 2, 3 | mpbiri 241 |
. . 3
     
     
  |
5 | | relfi 28289 |
. . 3

      |
6 | 1, 4, 5 | 3syl 18 |
. 2
       |
7 | | rexcom4 3053 |
. . . . . . . . . . . . 13
         
  

       |
8 | | ancom 457 |
. . . . . . . . . . . . . . . 16
     
 
       |
9 | 8 | exbii 1726 |
. . . . . . . . . . . . . . 15
       

          |
10 | | fvex 5889 |
. . . . . . . . . . . . . . . 16
     |
11 | | eleq2 2538 |
. . . . . . . . . . . . . . . 16
     
       |
12 | 10, 11 | ceqsexv 3070 |
. . . . . . . . . . . . . . 15
       

      |
13 | 9, 12 | bitr3i 259 |
. . . . . . . . . . . . . 14
        
      |
14 | 13 | rexbii 2881 |
. . . . . . . . . . . . 13
         

      |
15 | | r19.42v 2931 |
. . . . . . . . . . . . . 14
  
    


       |
16 | 15 | exbii 1726 |
. . . . . . . . . . . . 13
         
           |
17 | 7, 14, 16 | 3bitr3ri 284 |
. . . . . . . . . . . 12
    
     
      |
18 | | df-rex 2762 |
. . . . . . . . . . . 12
     
  
       |
19 | 17, 18 | bitr2i 258 |
. . . . . . . . . . 11
        
           |
20 | 19 | a1i 11 |
. . . . . . . . . 10
    
    
            |
21 | | vex 3034 |
. . . . . . . . . . 11
 |
22 | | eleq1 2537 |
. . . . . . . . . . . . 13
     
       |
23 | 22 | anbi2d 718 |
. . . . . . . . . . . 12
  
              |
24 | 23 | exbidv 1776 |
. . . . . . . . . . 11
         
  
        |
25 | 21, 24 | elab 3173 |
. . . . . . . . . 10
          
  
       |
26 | | eluniab 4201 |
. . . . . . . . . 10
            
       |
27 | 20, 25, 26 | 3bitr4g 296 |
. . . . . . . . 9
     
     
  
        |
28 | 27 | eqrdv 2469 |
. . . . . . . 8
             
       |
29 | 28 | eleq1d 2533 |
. . . . . . 7
              
        |
30 | 29 | adantr 472 |
. . . . . 6
 
              
        |
31 | | fpwrelmapffslem.3 |
. . . . . . . . . . 11
        |
32 | | ffn 5739 |
. . . . . . . . . . 11
        |
33 | | fnrnfv 5925 |
. . . . . . . . . . 11
  
       |
34 | 31, 32, 33 | 3syl 18 |
. . . . . . . . . 10
  
       |
35 | 34 | adantr 472 |
. . . . . . . . 9
 
  
       |
36 | | 0ex 4528 |
. . . . . . . . . . 11
 |
37 | 36 | a1i 11 |
. . . . . . . . . 10
 
   |
38 | | fpwrelmapffslem.1 |
. . . . . . . . . . . 12
 |
39 | | fex 6155 |
. . . . . . . . . . . 12
      
   |
40 | 31, 38, 39 | sylancl 675 |
. . . . . . . . . . 11
   |
41 | 40 | adantr 472 |
. . . . . . . . . 10
 
   |
42 | | ffun 5742 |
. . . . . . . . . . . 12
        |
43 | 31, 42 | syl 17 |
. . . . . . . . . . 11
   |
44 | 43 | adantr 472 |
. . . . . . . . . 10
 
   |
45 | | opabdm 28295 |
. . . . . . . . . . . . . 14
     
     

           |
46 | 1, 45 | syl 17 |
. . . . . . . . . . . . 13
    
        |
47 | 38, 39 | mpan2 685 |
. . . . . . . . . . . . . . . . 17
        |
48 | | suppimacnv 6944 |
. . . . . . . . . . . . . . . . . 18
    supp             |
49 | 36, 48 | mpan2 685 |
. . . . . . . . . . . . . . . . 17
  supp             |
50 | 31, 47, 49 | 3syl 18 |
. . . . . . . . . . . . . . . 16
  supp             |
51 | 31 | feqmptd 5932 |
. . . . . . . . . . . . . . . . . 18
         |
52 | 51 | cnveqd 5015 |
. . . . . . . . . . . . . . . . 17
 
 
       |
53 | 52 | imaeq1d 5173 |
. . . . . . . . . . . . . . . 16
                           |
54 | 50, 53 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
  supp                   |
55 | | eqid 2471 |
. . . . . . . . . . . . . . . 16
             |
56 | 55 | mptpreima 5335 |
. . . . . . . . . . . . . . 15
               
          |
57 | 54, 56 | syl6eq 2521 |
. . . . . . . . . . . . . 14
  supp              |
58 | | suppvalfn 6940 |
. . . . . . . . . . . . . . . . 17
 
  supp          |
59 | 38, 36, 58 | mp3an23 1382 |
. . . . . . . . . . . . . . . 16
  supp          |
60 | 31, 32, 59 | 3syl 18 |
. . . . . . . . . . . . . . 15
  supp          |
61 | | n0 3732 |
. . . . . . . . . . . . . . . . . 18
            |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . 17
     
        |
63 | 62 | rabbiia 3019 |
. . . . . . . . . . . . . . . 16

      
      |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . 15
       
        |
65 | 60, 57, 64 | 3eqtr3d 2513 |
. . . . . . . . . . . . . 14
            
       |
66 | | df-rab 2765 |
. . . . . . . . . . . . . . . 16


    
          |
67 | | 19.42v 1842 |
. . . . . . . . . . . . . . . . 17
        

        |
68 | 67 | abbii 2587 |
. . . . . . . . . . . . . . . 16
          
         |
69 | 66, 68 | eqtr4i 2496 |
. . . . . . . . . . . . . . 15


    
           |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
           
        |
71 | 57, 65, 70 | 3eqtrd 2509 |
. . . . . . . . . . . . 13
  supp              |
72 | 46, 71 | eqtr4d 2508 |
. . . . . . . . . . . 12
  supp    |
73 | 72 | eleq1d 2533 |
. . . . . . . . . . 11
   supp     |
74 | 73 | biimpa 492 |
. . . . . . . . . 10
 
  supp    |
75 | 37, 41, 44, 74 | ffsrn 28389 |
. . . . . . . . 9
 
   |
76 | 35, 75 | eqeltrrd 2550 |
. . . . . . . 8
 
          |
77 | | unifi 7881 |
. . . . . . . . 9
   
      
     
  
       |
78 | 77 | ex 441 |
. . . . . . . 8
  
       
       
        |
79 | 76, 78 | syl 17 |
. . . . . . 7
 
   
       
        |
80 | | unifi3 28368 |
. . . . . . 7
   
      
       |
81 | 79, 80 | impbid1 208 |
. . . . . 6
 
   
       
        |
82 | 30, 81 | bitr4d 264 |
. . . . 5
 
             
        |
83 | | opabrn 28296 |
. . . . . . . 8
     
     
            |
84 | 1, 83 | syl 17 |
. . . . . . 7
    
        |
85 | 84 | eleq1d 2533 |
. . . . . 6
               |
86 | 85 | adantr 472 |
. . . . 5
 
 
             |
87 | 35 | sseq1d 3445 |
. . . . 5
 
 
 
        |
88 | 82, 86, 87 | 3bitr4d 293 |
. . . 4
 
 
   |
89 | 88 | pm5.32da 653 |
. . 3
   
     |
90 | 73 | anbi1d 719 |
. . 3
   
  supp 
    |
91 | 89, 90 | bitrd 261 |
. 2
   
  supp 
    |
92 | | ancom 457 |
. . 3
   supp 


 supp     |
93 | 92 | a1i 11 |
. 2
    supp 
   supp      |
94 | 6, 91, 93 | 3bitrd 287 |
1
  
 supp      |