Step | Hyp | Ref
| Expression |
1 | | fvex 5873 |
. . . 4
             |
2 | | axcc2lem.3 |
. . . 4
               |
3 | 1, 2 | fnmpti 5704 |
. . 3
 |
4 | | snex 4640 |
. . . . . . . . . . . . . . 15
 
 |
5 | | fvex 5873 |
. . . . . . . . . . . . . . 15
     |
6 | 4, 5 | xpex 6592 |
. . . . . . . . . . . . . 14
         |
7 | | axcc2lem.2 |
. . . . . . . . . . . . . . 15
           |
8 | 7 | fvmpt2 5955 |
. . . . . . . . . . . . . 14
                         |
9 | 6, 8 | mpan2 676 |
. . . . . . . . . . . . 13
               |
10 | | vex 3047 |
. . . . . . . . . . . . . . 15
 |
11 | 10 | snnz 4089 |
. . . . . . . . . . . . . 14
   |
12 | | 0ex 4534 |
. . . . . . . . . . . . . . . . . 18
 |
13 | 12 | snnz 4089 |
. . . . . . . . . . . . . . . . 17
   |
14 | | iftrue 3886 |
. . . . . . . . . . . . . . . . . 18
    
                   |
15 | 14 | neeq1d 2682 |
. . . . . . . . . . . . . . . . 17
    
               
     |
16 | 13, 15 | mpbiri 237 |
. . . . . . . . . . . . . . . 16
    
                 |
17 | | iffalse 3889 |
. . . . . . . . . . . . . . . . 17
                          |
18 | | df-ne 2623 |
. . . . . . . . . . . . . . . . . 18
    
      |
19 | 18 | biimpri 210 |
. . . . . . . . . . . . . . . . 17
           |
20 | 17, 19 | eqnetrd 2690 |
. . . . . . . . . . . . . . . 16
                      |
21 | 16, 20 | pm2.61i 168 |
. . . . . . . . . . . . . . 15
                |
22 | | p0ex 4589 |
. . . . . . . . . . . . . . . . . 18
   |
23 | | fvex 5873 |
. . . . . . . . . . . . . . . . . 18
     |
24 | 22, 23 | ifex 3948 |
. . . . . . . . . . . . . . . . 17
                |
25 | | axcc2lem.1 |
. . . . . . . . . . . . . . . . . 18
                  |
26 | 25 | fvmpt2 5955 |
. . . . . . . . . . . . . . . . 17
                                       |
27 | 24, 26 | mpan2 676 |
. . . . . . . . . . . . . . . 16
                      |
28 | 27 | neeq1d 2682 |
. . . . . . . . . . . . . . 15
     
                  |
29 | 21, 28 | mpbiri 237 |
. . . . . . . . . . . . . 14
       |
30 | | xpnz 5255 |
. . . . . . . . . . . . . . 15
        
          |
31 | 30 | biimpi 198 |
. . . . . . . . . . . . . 14
                   |
32 | 11, 29, 31 | sylancr 668 |
. . . . . . . . . . . . 13
           |
33 | 9, 32 | eqnetrd 2690 |
. . . . . . . . . . . 12
       |
34 | 6, 7 | fnmpti 5704 |
. . . . . . . . . . . . . 14
 |
35 | | fnfvelrn 6017 |
. . . . . . . . . . . . . 14
 
       |
36 | 34, 35 | mpan 675 |
. . . . . . . . . . . . 13
       |
37 | | neeq1 2685 |
. . . . . . . . . . . . . . 15
     
       |
38 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
                   |
39 | | id 22 |
. . . . . . . . . . . . . . . 16
           |
40 | 38, 39 | eleq12d 2522 |
. . . . . . . . . . . . . . 15
         
               |
41 | 37, 40 | imbi12d 322 |
. . . . . . . . . . . . . 14
           
    
                |
42 | 41 | rspccv 3146 |
. . . . . . . . . . . . 13
 
                                 |
43 | 36, 42 | syl5 33 |
. . . . . . . . . . . 12
 
                             |
44 | 33, 43 | mpdi 43 |
. . . . . . . . . . 11
 
                       |
45 | 44 | impcom 432 |
. . . . . . . . . 10
                         |
46 | 9 | eleq2d 2513 |
. . . . . . . . . . 11
             
                   |
47 | 46 | adantr 467 |
. . . . . . . . . 10
                       
                   |
48 | 45, 47 | mpbid 214 |
. . . . . . . . 9
                             |
49 | | xp2nd 6821 |
. . . . . . . . 9
                                   |
50 | 48, 49 | syl 17 |
. . . . . . . 8
                             |
51 | 50 | 3adant3 1027 |
. . . . . . 7
                                 |
52 | 2 | fvmpt2 5955 |
. . . . . . . . . 10
                                 |
53 | 1, 52 | mpan2 676 |
. . . . . . . . 9
                   |
54 | 53 | 3ad2ant1 1028 |
. . . . . . . 8
                                 |
55 | 54 | eqcomd 2456 |
. . . . . . 7
                                 |
56 | 27 | 3ad2ant1 1028 |
. . . . . . . 8
                                    |
57 | | ifnefalse 3892 |
. . . . . . . . 9
    
                     |
58 | 57 | 3ad2ant3 1030 |
. . . . . . . 8
                                    |
59 | 56, 58 | eqtrd 2484 |
. . . . . . 7
                         |
60 | 51, 55, 59 | 3eltr3d 2542 |
. . . . . 6
                         |
61 | 60 | 3expia 1209 |
. . . . 5
                           |
62 | 61 | expcom 437 |
. . . 4
 
                         |
63 | 62 | ralrimiv 2799 |
. . 3
 
                        |
64 | | omex 8145 |
. . . . 5
 |
65 | | fnex 6130 |
. . . . 5
  
  |
66 | 3, 64, 65 | mp2an 677 |
. . . 4
 |
67 | | fneq1 5662 |
. . . . 5
 
   |
68 | | fveq1 5862 |
. . . . . . . 8
           |
69 | 68 | eleq1d 2512 |
. . . . . . 7
         
           |
70 | 69 | imbi2d 318 |
. . . . . 6
               
    
            |
71 | 70 | ralbidv 2826 |
. . . . 5
  
             
                  |
72 | 67, 71 | anbi12d 716 |
. . . 4
                  
                    |
73 | 66, 72 | spcev 3140 |
. . 3
                    
                  |
74 | 3, 63, 73 | sylancr 668 |
. 2
 
                            |
75 | 6 | a1i 11 |
. . . . . 6
 
           |
76 | 75, 7 | fmptd 6044 |
. . . . 5
       |
77 | 64, 76 | ax-mp 5 |
. . . 4
     |
78 | | sneq 3977 |
. . . . . . . . . 10
  
    |
79 | | fveq2 5863 |
. . . . . . . . . 10
           |
80 | 78, 79 | xpeq12d 4858 |
. . . . . . . . 9
                   |
81 | 80, 7, 6 | fvmpt3i 5951 |
. . . . . . . 8
               |
82 | 81 | adantl 468 |
. . . . . . 7
 
               |
83 | 82 | eqeq2d 2460 |
. . . . . 6
 
                         |
84 | 9 | adantr 467 |
. . . . . . . 8
 
               |
85 | 84 | eqeq1d 2452 |
. . . . . . 7
 
                                 |
86 | | xp11 5271 |
. . . . . . . . . 10
                         
                 |
87 | 11, 29, 86 | sylancr 668 |
. . . . . . . . 9
                    
              |
88 | 10 | sneqr 4138 |
. . . . . . . . . 10
       |
89 | 88 | adantr 467 |
. . . . . . . . 9
              
  |
90 | 87, 89 | syl6bi 232 |
. . . . . . . 8
                 
   |
91 | 90 | adantr 467 |
. . . . . . 7
 
                 
   |
92 | 85, 91 | sylbid 219 |
. . . . . 6
 
             
   |
93 | 83, 92 | sylbid 219 |
. . . . 5
 
             |
94 | 93 | rgen2a 2814 |
. . . 4
          
  |
95 | | dff13 6157 |
. . . 4
    
    
          
    |
96 | 77, 94, 95 | mpbir2an 930 |
. . 3
     |
97 | | f1f1orn 5823 |
. . . 4
           |
98 | 64 | f1oen 7587 |
. . . 4
       |
99 | | ensym 7615 |
. . . 4

  |
100 | 97, 98, 99 | 3syl 18 |
. . 3
    
  |
101 | 7 | rneqi 5060 |
. . . . 5
           |
102 | | dmmptg 5331 |
. . . . . . . 8
 
                    |
103 | 6 | a1i 11 |
. . . . . . . 8
           |
104 | 102, 103 | mprg 2750 |
. . . . . . 7
           |
105 | 104, 64 | eqeltri 2524 |
. . . . . 6
           |
106 | | funmpt 5617 |
. . . . . 6
           |
107 | | funrnex 6757 |
. . . . . 6
                      
            |
108 | 105, 106,
107 | mp2 9 |
. . . . 5
           |
109 | 101, 108 | eqeltri 2524 |
. . . 4
 |
110 | | breq1 4404 |
. . . . 5
 
   |
111 | | raleq 2986 |
. . . . . 6
                    |
112 | 111 | exbidv 1767 |
. . . . 5
    
     
  
          |
113 | 110, 112 | imbi12d 322 |
. . . 4
     

     

  
           |
114 | | ax-cc 8862 |
. . . 4

  
        |
115 | 109, 113,
114 | vtocl 3099 |
. . 3

    
       |
116 | 96, 100, 115 | mp2b 10 |
. 2
  
        |
117 | 74, 116 | exlimiiv 1776 |
1
                    |