Step | Hyp | Ref
| Expression |
1 | | fpwrelmap.3 |
. . 3
        
        |
2 | | fpwrelmap.1 |
. . . . . 6
 |
3 | 2 | a1i 11 |
. . . . 5
      |
4 | | simpr 463 |
. . . . . . . . 9
     
            |
5 | | elmapi 7490 |
. . . . . . . . . . 11
           |
6 | 5 | ffvelrnda 6020 |
. . . . . . . . . 10
     
       |
7 | 6 | adantr 467 |
. . . . . . . . 9
     
             |
8 | | elelpwi 3961 |
. . . . . . . . 9
           
  |
9 | 4, 7, 8 | syl2anc 666 |
. . . . . . . 8
     
        |
10 | 9 | ex 436 |
. . . . . . 7
     
    
   |
11 | 10 | alrimiv 1772 |
. . . . . 6
     
          |
12 | | abss 3497 |
. . . . . . 7
             
   |
13 | | fpwrelmap.2 |
. . . . . . . 8
 |
14 | 13 | ssex 4546 |
. . . . . . 7
               |
15 | 12, 14 | sylbir 217 |
. . . . . 6
       
         |
16 | 11, 15 | syl 17 |
. . . . 5
     

    
  |
17 | 3, 16 | opabex3d 6768 |
. . . 4
        
        |
18 | 17 | adantl 468 |
. . 3
        

        |
19 | 2 | mptex 6134 |
. . . 4
       |
20 | 19 | a1i 11 |
. . 3
             |
21 | 10 | imdistanda 698 |
. . . . . . . . . 10
     
    

    |
22 | 21 | ssopab2dv 4729 |
. . . . . . . . 9
        
          
    |
23 | 22 | adantr 467 |
. . . . . . . 8
                     
          
    |
24 | | simpr 463 |
. . . . . . . 8
                              |
25 | | df-xp 4839 |
. . . . . . . . 9
     

   |
26 | 25 | a1i 11 |
. . . . . . . 8
                            |
27 | 23, 24, 26 | 3sstr4d 3474 |
. . . . . . 7
                     |
28 | | selpw 3957 |
. . . . . . 7
   

   |
29 | 27, 28 | sylibr 216 |
. . . . . 6
                  
   |
30 | 5 | feqmptd 5916 |
. . . . . . . 8
            |
31 | 30 | adantr 467 |
. . . . . . 7
                         |
32 | | nfv 1760 |
. . . . . . . . 9

    |
33 | | nfopab1 4468 |
. . . . . . . . . 10
     

       |
34 | 33 | nfeq2 2606 |
. . . . . . . . 9

    
       |
35 | 32, 34 | nfan 2010 |
. . . . . . . 8
     
   

        |
36 | | df-rab 2745 |
. . . . . . . . . 10
           |
37 | 36 | a1i 11 |
. . . . . . . . 9
     
   

       

           |
38 | | nfv 1760 |
. . . . . . . . . . . 12
     |
39 | | nfopab2 4469 |
. . . . . . . . . . . . 13
     

       |
40 | 39 | nfeq2 2606 |
. . . . . . . . . . . 12
     
       |
41 | 38, 40 | nfan 2010 |
. . . . . . . . . . 11
     
   

        |
42 | | nfv 1760 |
. . . . . . . . . . 11
  |
43 | 41, 42 | nfan 2010 |
. . . . . . . . . 10
          

         |
44 | 9 | adantllr 724 |
. . . . . . . . . . . . 13
          

       
       |
45 | | df-br 4402 |
. . . . . . . . . . . . . . . . 17
  
  
  |
46 | | eleq2 2517 |
. . . . . . . . . . . . . . . . . 18
     
                

         |
47 | | opabid 4707 |
. . . . . . . . . . . . . . . . . 18
       

     

       |
48 | 46, 47 | syl6bb 265 |
. . . . . . . . . . . . . . . . 17
     
          
        |
49 | 45, 48 | syl5bb 261 |
. . . . . . . . . . . . . . . 16
     
                  |
50 | 49 | ad2antlr 732 |
. . . . . . . . . . . . . . 15
     
   

       
  

        |
51 | | elfvdm 5889 |
. . . . . . . . . . . . . . . . . . . 20
       |
52 | 51 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
         
  |
53 | | fdm 5731 |
. . . . . . . . . . . . . . . . . . . . 21
        |
54 | 5, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   
  |
55 | 54 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
         
  |
56 | 52, 55 | eleqtrd 2530 |
. . . . . . . . . . . . . . . . . 18
         
  |
57 | 56 | ex 436 |
. . . . . . . . . . . . . . . . 17
        
   |
58 | 57 | pm4.71rd 640 |
. . . . . . . . . . . . . . . 16
        

        |
59 | 58 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
     
   

       
              |
60 | 50, 59 | bitr4d 260 |
. . . . . . . . . . . . . 14
     
   

       
  
       |
61 | 60 | biimpar 488 |
. . . . . . . . . . . . 13
          

       
         |
62 | 44, 61 | jca 535 |
. . . . . . . . . . . 12
          

       
           |
63 | 62 | ex 436 |
. . . . . . . . . . 11
     
   

       
    

      |
64 | 60 | biimpd 211 |
. . . . . . . . . . . 12
     
   

       
          |
65 | 64 | adantld 469 |
. . . . . . . . . . 11
     
   

       
            |
66 | 63, 65 | impbid 194 |
. . . . . . . . . 10
     
   

       
            |
67 | 43, 66 | abbid 2567 |
. . . . . . . . 9
     
   

       

    
        |
68 | | abid2 2572 |
. . . . . . . . . 10
           |
69 | 68 | a1i 11 |
. . . . . . . . 9
     
   

       

    
      |
70 | 37, 67, 69 | 3eqtr2rd 2491 |
. . . . . . . 8
     
   

       
          |
71 | 35, 70 | mpteq2da 4487 |
. . . . . . 7
                               |
72 | 31, 71 | eqtrd 2484 |
. . . . . 6
                         |
73 | 29, 72 | jca 535 |
. . . . 5
                              |
74 | | ssrab2 3513 |
. . . . . . . . . . . 12
     |
75 | 13 | elpw2 4566 |
. . . . . . . . . . . 12
     

     |
76 | 74, 75 | mpbir 213 |
. . . . . . . . . . 11
      |
77 | 76 | a1i 11 |
. . . . . . . . . 10
    
        |
78 | | eqid 2450 |
. . . . . . . . . 10
             |
79 | 77, 78 | fmptd 6044 |
. . . . . . . . 9
                 |
80 | 79 | adantr 467 |
. . . . . . . 8
    

     

            |
81 | | simpr 463 |
. . . . . . . . 9
    

     

       |
82 | 81 | feq1d 5712 |
. . . . . . . 8
    

     
     

             |
83 | 80, 82 | mpbird 236 |
. . . . . . 7
    

     
       |
84 | 13 | pwex 4585 |
. . . . . . . 8
  |
85 | 84, 2 | elmap 7497 |
. . . . . . 7
   
       |
86 | 83, 85 | sylibr 216 |
. . . . . 6
    

     
     |
87 | | elpwi 3959 |
. . . . . . . . . 10
   
    |
88 | 87 | adantr 467 |
. . . . . . . . 9
    

     

   |
89 | | xpss 4940 |
. . . . . . . . 9
  
  |
90 | 88, 89 | syl6ss 3443 |
. . . . . . . 8
    

     

   |
91 | | df-rel 4840 |
. . . . . . . 8
     |
92 | 90, 91 | sylibr 216 |
. . . . . . 7
    

     
  |
93 | | relopab 4959 |
. . . . . . . 8
            |
94 | 93 | a1i 11 |
. . . . . . 7
    

     
    
        |
95 | | id 22 |
. . . . . . 7
    

     
             |
96 | | nfv 1760 |
. . . . . . . . 9

    |
97 | | nfmpt1 4491 |
. . . . . . . . . 10
         |
98 | 97 | nfeq2 2606 |
. . . . . . . . 9


      |
99 | 96, 98 | nfan 2010 |
. . . . . . . 8
    


       |
100 | | nfv 1760 |
. . . . . . . . 9
     |
101 | 42 | nfci 2581 |
. . . . . . . . . . 11
   |
102 | | nfrab1 2970 |
. . . . . . . . . . 11
       |
103 | 101, 102 | nfmpt 4490 |
. . . . . . . . . 10
         |
104 | 103 | nfeq2 2606 |
. . . . . . . . 9
        |
105 | 100, 104 | nfan 2010 |
. . . . . . . 8
    


       |
106 | | nfcv 2591 |
. . . . . . . 8
   |
107 | | nfcv 2591 |
. . . . . . . 8
   |
108 | | brelg 28210 |
. . . . . . . . . . . . . . . 16
 
     
   |
109 | 87, 108 | sylan 474 |
. . . . . . . . . . . . . . 15
            |
110 | 109 | adantlr 720 |
. . . . . . . . . . . . . 14
    


         
   |
111 | 110 | simpld 461 |
. . . . . . . . . . . . 13
    


        
  |
112 | 110 | simprd 465 |
. . . . . . . . . . . . . 14
    


           |
113 | | simpr 463 |
. . . . . . . . . . . . . 14
    


             |
114 | 81 | fveq1d 5865 |
. . . . . . . . . . . . . . . . . 18
    

     
                |
115 | 13 | rabex 4553 |
. . . . . . . . . . . . . . . . . . 19
     |
116 | 78 | fvmpt2 5955 |
. . . . . . . . . . . . . . . . . . 19
                       |
117 | 115, 116 | mpan2 676 |
. . . . . . . . . . . . . . . . . 18
                 |
118 | 114, 117 | sylan9eq 2504 |
. . . . . . . . . . . . . . . . 17
    


                 |
119 | 118 | eleq2d 2513 |
. . . . . . . . . . . . . . . 16
    


           
       |
120 | | rabid 2966 |
. . . . . . . . . . . . . . . 16
    

     |
121 | 119, 120 | syl6bb 265 |
. . . . . . . . . . . . . . 15
    


           

      |
122 | 111, 121 | syldan 473 |
. . . . . . . . . . . . . 14
    


                     |
123 | 112, 113,
122 | mpbir2and 932 |
. . . . . . . . . . . . 13
    


               |
124 | 111, 123 | jca 535 |
. . . . . . . . . . . 12
    


         
       |
125 | 124 | ex 436 |
. . . . . . . . . . 11
    

     
   
        |
126 | 121 | simplbda 629 |
. . . . . . . . . . . 12
              
         |
127 | 126 | expl 623 |
. . . . . . . . . . 11
    

     
 
          |
128 | 125, 127 | impbid 194 |
. . . . . . . . . 10
    

     
  

        |
129 | 45, 128 | syl5bbr 263 |
. . . . . . . . 9
    

     
    
        |
130 | 129, 47 | syl6bbr 267 |
. . . . . . . 8
    

     
          

         |
131 | 99, 105, 106, 107, 33, 39, 130 | eqrelrd2 28215 |
. . . . . . 7
      

                  
   

        |
132 | 92, 94, 95, 131 | syl21anc 1266 |
. . . . . 6
    

     
   

        |
133 | 86, 132 | jca 535 |
. . . . 5
    

     
       

         |
134 | 73, 133 | impbii 191 |
. . . 4
                   


        |
135 | 134 | a1i 11 |
. . 3
        

         


         |
136 | 1, 18, 20, 135 | f1od 6516 |
. 2
            |
137 | 136 | trud 1452 |
1
           |