Step |
Hyp |
Ref |
Expression |
1 |
|
axcc2lem.1 |
|
2 |
|
axcc2lem.2 |
|
3 |
|
axcc2lem.3 |
|
4 |
|
fvex |
|
5 |
4 3
|
fnmpti |
|
6 |
|
snex |
|
7 |
|
fvex |
|
8 |
6 7
|
xpex |
|
9 |
2
|
fvmpt2 |
|
10 |
8 9
|
mpan2 |
|
11 |
|
vex |
|
12 |
11
|
snnz |
|
13 |
|
0ex |
|
14 |
13
|
snnz |
|
15 |
|
iftrue |
|
16 |
15
|
neeq1d |
|
17 |
14 16
|
mpbiri |
|
18 |
|
iffalse |
|
19 |
|
neqne |
|
20 |
18 19
|
eqnetrd |
|
21 |
17 20
|
pm2.61i |
|
22 |
|
p0ex |
|
23 |
|
fvex |
|
24 |
22 23
|
ifex |
|
25 |
1
|
fvmpt2 |
|
26 |
24 25
|
mpan2 |
|
27 |
26
|
neeq1d |
|
28 |
21 27
|
mpbiri |
|
29 |
|
xpnz |
|
30 |
29
|
biimpi |
|
31 |
12 28 30
|
sylancr |
|
32 |
10 31
|
eqnetrd |
|
33 |
8 2
|
fnmpti |
|
34 |
|
fnfvelrn |
|
35 |
33 34
|
mpan |
|
36 |
|
neeq1 |
|
37 |
|
fveq2 |
|
38 |
|
id |
|
39 |
37 38
|
eleq12d |
|
40 |
36 39
|
imbi12d |
|
41 |
40
|
rspccv |
|
42 |
35 41
|
syl5 |
|
43 |
32 42
|
mpdi |
|
44 |
43
|
impcom |
|
45 |
10
|
eleq2d |
|
46 |
45
|
adantr |
|
47 |
44 46
|
mpbid |
|
48 |
|
xp2nd |
|
49 |
47 48
|
syl |
|
50 |
49
|
3adant3 |
|
51 |
3
|
fvmpt2 |
|
52 |
4 51
|
mpan2 |
|
53 |
52
|
3ad2ant1 |
|
54 |
53
|
eqcomd |
|
55 |
26
|
3ad2ant1 |
|
56 |
|
ifnefalse |
|
57 |
56
|
3ad2ant3 |
|
58 |
55 57
|
eqtrd |
|
59 |
50 54 58
|
3eltr3d |
|
60 |
59
|
3expia |
|
61 |
60
|
expcom |
|
62 |
61
|
ralrimiv |
|
63 |
|
omex |
|
64 |
|
fnex |
|
65 |
5 63 64
|
mp2an |
|
66 |
|
fneq1 |
|
67 |
|
fveq1 |
|
68 |
67
|
eleq1d |
|
69 |
68
|
imbi2d |
|
70 |
69
|
ralbidv |
|
71 |
66 70
|
anbi12d |
|
72 |
65 71
|
spcev |
|
73 |
5 62 72
|
sylancr |
|
74 |
8
|
a1i |
|
75 |
74 2
|
fmptd |
|
76 |
63 75
|
ax-mp |
|
77 |
|
sneq |
|
78 |
|
fveq2 |
|
79 |
77 78
|
xpeq12d |
|
80 |
79 2 8
|
fvmpt3i |
|
81 |
80
|
adantl |
|
82 |
81
|
eqeq2d |
|
83 |
10
|
adantr |
|
84 |
83
|
eqeq1d |
|
85 |
|
xp11 |
|
86 |
12 28 85
|
sylancr |
|
87 |
11
|
sneqr |
|
88 |
87
|
adantr |
|
89 |
86 88
|
syl6bi |
|
90 |
89
|
adantr |
|
91 |
84 90
|
sylbid |
|
92 |
82 91
|
sylbid |
|
93 |
92
|
rgen2 |
|
94 |
|
dff13 |
|
95 |
76 93 94
|
mpbir2an |
|
96 |
|
f1f1orn |
|
97 |
63
|
f1oen |
|
98 |
|
ensym |
|
99 |
96 97 98
|
3syl |
|
100 |
2
|
rneqi |
|
101 |
|
dmmptg |
|
102 |
8
|
a1i |
|
103 |
101 102
|
mprg |
|
104 |
103 63
|
eqeltri |
|
105 |
|
funmpt |
|
106 |
|
funrnex |
|
107 |
104 105 106
|
mp2 |
|
108 |
100 107
|
eqeltri |
|
109 |
|
breq1 |
|
110 |
|
raleq |
|
111 |
110
|
exbidv |
|
112 |
109 111
|
imbi12d |
|
113 |
|
ax-cc |
|
114 |
108 112 113
|
vtocl |
|
115 |
95 99 114
|
mp2b |
|
116 |
73 115
|
exlimiiv |
|