Step | Hyp | Ref
| Expression |
1 | | fnmap 6655 |
. . 3

  |
2 | | xpmapen.1 |
. . . 4
 |
3 | | xpmapen.2 |
. . . 4
 |
4 | 2, 3 | xpex 4742 |
. . 3
   |
5 | | xpmapen.3 |
. . 3
 |
6 | | fnovex 5908 |
. . 3
    

      |
7 | 1, 4, 5, 6 | mp3an 1337 |
. 2
     |
8 | | fnovex 5908 |
. . . 4
        |
9 | 1, 2, 5, 8 | mp3an 1337 |
. . 3
   |
10 | | fnovex 5908 |
. . . 4
        |
11 | 1, 3, 5, 10 | mp3an 1337 |
. . 3
   |
12 | 9, 11 | xpex 4742 |
. 2
       |
13 | 4, 5 | elmap 6677 |
. . . . . . 7
    
        |
14 | | ffvelcdm 5650 |
. . . . . . 7
       
         |
15 | 13, 14 | sylanb 284 |
. . . . . 6
     
         |
16 | | xp1st 6166 |
. . . . . 6
                 |
17 | 15, 16 | syl 14 |
. . . . 5
     
           |
18 | | xpmapenlem.4 |
. . . . 5
           |
19 | 17, 18 | fmptd 5671 |
. . . 4
           |
20 | 2, 5 | elmap 6677 |
. . . 4
  
      |
21 | 19, 20 | sylibr 134 |
. . 3
         |
22 | | xp2nd 6167 |
. . . . . 6
                 |
23 | 15, 22 | syl 14 |
. . . . 5
     
           |
24 | | xpmapenlem.5 |
. . . . 5
           |
25 | 23, 24 | fmptd 5671 |
. . . 4
           |
26 | 3, 5 | elmap 6677 |
. . . 4
  
      |
27 | 25, 26 | sylibr 134 |
. . 3
         |
28 | | opelxpi 4659 |
. . 3
   
              |
29 | 21, 27, 28 | syl2anc 411 |
. 2
                |
30 | | xp1st 6166 |
. . . . . . 7
               |
31 | 2, 5 | elmap 6677 |
. . . . . . 7
      
          |
32 | 30, 31 | sylib 122 |
. . . . . 6
                 |
33 | 32 | ffvelcdmda 5652 |
. . . . 5
       
           |
34 | | xp2nd 6167 |
. . . . . . 7
               |
35 | 3, 5 | elmap 6677 |
. . . . . . 7
      
          |
36 | 34, 35 | sylib 122 |
. . . . . 6
                 |
37 | 36 | ffvelcdmda 5652 |
. . . . 5
       
           |
38 | | opelxpi 4659 |
. . . . 5
         
                                |
39 | 33, 37, 38 | syl2anc 411 |
. . . 4
       
                        |
40 | | xpmapenlem.6 |
. . . 4
                      |
41 | 39, 40 | fmptd 5671 |
. . 3
               |
42 | 4, 5 | elmap 6677 |
. . 3
    
        |
43 | 41, 42 | sylibr 134 |
. 2
             |
44 | | 1st2nd2 6176 |
. . . . 5
                    |
45 | 44 | ad2antlr 489 |
. . . 4
     

                     |
46 | 32 | feqmptd 5570 |
. . . . . . 7
                       |
47 | 46 | ad2antlr 489 |
. . . . . 6
     

                        |
48 | | simplr 528 |
. . . . . . . . . . . 12
       
           |
49 | 48 | fveq1d 5518 |
. . . . . . . . . . 11
       
                   |
50 | | vex 2741 |
. . . . . . . . . . . . . . . 16
 |
51 | | 1stexg 6168 |
. . . . . . . . . . . . . . . 16
       |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     |
53 | | vex 2741 |
. . . . . . . . . . . . . . 15
 |
54 | 52, 53 | fvex 5536 |
. . . . . . . . . . . . . 14
         |
55 | | 2ndexg 6169 |
. . . . . . . . . . . . . . . 16
       |
56 | 50, 55 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     |
57 | 56, 53 | fvex 5536 |
. . . . . . . . . . . . . 14
         |
58 | 54, 57 | opex 4230 |
. . . . . . . . . . . . 13
                    |
59 | 40 | fvmpt2 5600 |
. . . . . . . . . . . . 13
                                               |
60 | 58, 59 | mpan2 425 |
. . . . . . . . . . . 12
                          |
61 | 60 | adantl 277 |
. . . . . . . . . . 11
       
                                  |
62 | 49, 61 | eqtrd 2210 |
. . . . . . . . . 10
       
                                  |
63 | 62 | fveq2d 5520 |
. . . . . . . . 9
       
                                          |
64 | 54, 57 | op1st 6147 |
. . . . . . . . 9
                                |
65 | 63, 64 | eqtrdi 2226 |
. . . . . . . 8
       
                           |
66 | 65 | mpteq2dva 4094 |
. . . . . . 7
     

                              |
67 | 18, 66 | eqtrid 2222 |
. . . . . 6
     

                    |
68 | 47, 67 | eqtr4d 2213 |
. . . . 5
     

              |
69 | 36 | feqmptd 5570 |
. . . . . . 7
                       |
70 | 69 | ad2antlr 489 |
. . . . . 6
     

                        |
71 | 62 | fveq2d 5520 |
. . . . . . . . 9
       
                                          |
72 | 54, 57 | op2nd 6148 |
. . . . . . . . 9
                                |
73 | 71, 72 | eqtrdi 2226 |
. . . . . . . 8
       
                           |
74 | 73 | mpteq2dva 4094 |
. . . . . . 7
     

                              |
75 | 24, 74 | eqtrid 2222 |
. . . . . 6
     

                    |
76 | 70, 75 | eqtr4d 2213 |
. . . . 5
     

              |
77 | 68, 76 | opeq12d 3787 |
. . . 4
     

                        |
78 | 45, 77 | eqtrd 2210 |
. . 3
     

             |
79 | | simpll 527 |
. . . . . 6
     

             
   |
80 | 79, 13 | sylib 122 |
. . . . 5
     

               
   |
81 | 80 | feqmptd 5570 |
. . . 4
     

                   |
82 | | simpr 110 |
. . . . . . . . . . . 12
     

                |
83 | 82 | fveq2d 5520 |
. . . . . . . . . . 11
     

                        |
84 | 21 | ad2antrr 488 |
. . . . . . . . . . . 12
     

               |
85 | 27 | ad2antrr 488 |
. . . . . . . . . . . 12
     

               |
86 | | op1stg 6151 |
. . . . . . . . . . . 12
   
            |
87 | 84, 85, 86 | syl2anc 411 |
. . . . . . . . . . 11
     

                    |
88 | 83, 87 | eqtrd 2210 |
. . . . . . . . . 10
     

                 |
89 | 88 | fveq1d 5518 |
. . . . . . . . 9
     

                         |
90 | | vex 2741 |
. . . . . . . . . . . 12
 |
91 | 90, 53 | fvex 5536 |
. . . . . . . . . . 11
     |
92 | | 1stexg 6168 |
. . . . . . . . . . 11
               |
93 | 91, 92 | ax-mp 5 |
. . . . . . . . . 10
         |
94 | 18 | fvmpt2 5600 |
. . . . . . . . . 10
                         |
95 | 93, 94 | mpan2 425 |
. . . . . . . . 9
               |
96 | 89, 95 | sylan9eq 2230 |
. . . . . . . 8
       
           
                  |
97 | 82 | fveq2d 5520 |
. . . . . . . . . . 11
     

                        |
98 | | op2ndg 6152 |
. . . . . . . . . . . 12
   
            |
99 | 84, 85, 98 | syl2anc 411 |
. . . . . . . . . . 11
     

                    |
100 | 97, 99 | eqtrd 2210 |
. . . . . . . . . 10
     

                 |
101 | 100 | fveq1d 5518 |
. . . . . . . . 9
     

                         |
102 | | 2ndexg 6169 |
. . . . . . . . . . 11
               |
103 | 91, 102 | ax-mp 5 |
. . . . . . . . . 10
         |
104 | 24 | fvmpt2 5600 |
. . . . . . . . . 10
                         |
105 | 103, 104 | mpan2 425 |
. . . . . . . . 9
               |
106 | 101, 105 | sylan9eq 2230 |
. . . . . . . 8
       
           
                  |
107 | 96, 106 | opeq12d 3787 |
. . . . . . 7
       
           
                                        |
108 | 80 | ffvelcdmda 5652 |
. . . . . . . 8
       
           
        |
109 | | 1st2nd2 6176 |
. . . . . . . 8
                                |
110 | 108, 109 | syl 14 |
. . . . . . 7
       
           
                         |
111 | 107, 110 | eqtr4d 2213 |
. . . . . 6
       
           
                         |
112 | 111 | mpteq2dva 4094 |
. . . . 5
     

                                        |
113 | 40, 112 | eqtrid 2222 |
. . . 4
     

                   |
114 | 81, 113 | eqtr4d 2213 |
. . 3
     

             |
115 | 78, 114 | impbida 596 |
. 2
     
              |
116 | 7, 12, 29, 43, 115 | en3i 6771 |
1
           |