| Step |
Hyp |
Ref |
Expression |
| 1 |
|
modelaxreplem.1 |
|
| 2 |
|
modelaxreplem.2 |
|
| 3 |
|
modelaxreplem.3 |
|
| 4 |
|
modelaxreplem.4 |
|
| 5 |
|
modelaxreplem1.5 |
|
| 6 |
|
eleq1 |
|
| 7 |
3 6
|
syl5ibrcom |
|
| 8 |
|
vex |
|
| 9 |
8 5
|
ssexi |
|
| 10 |
9
|
0sdom |
|
| 11 |
|
ssdomg |
|
| 12 |
8 5 11
|
mp2 |
|
| 13 |
|
fodomr |
|
| 14 |
12 13
|
mpan2 |
|
| 15 |
10 14
|
sylbir |
|
| 16 |
|
df-fo |
|
| 17 |
|
df-fn |
|
| 18 |
|
eleq1 |
|
| 19 |
4 18
|
syl5ibrcom |
|
| 20 |
19
|
anim2d |
|
| 21 |
17 20
|
biimtrid |
|
| 22 |
5 1
|
sstrid |
|
| 23 |
|
sseq1 |
|
| 24 |
22 23
|
syl5ibrcom |
|
| 25 |
|
df-3an |
|
| 26 |
|
funeq |
|
| 27 |
|
dmeq |
|
| 28 |
27
|
eleq1d |
|
| 29 |
|
rneq |
|
| 30 |
29
|
sseq1d |
|
| 31 |
26 28 30
|
3anbi123d |
|
| 32 |
29
|
eleq1d |
|
| 33 |
31 32
|
imbi12d |
|
| 34 |
33
|
spvv |
|
| 35 |
2 34
|
syl |
|
| 36 |
25 35
|
biimtrrid |
|
| 37 |
21 24 36
|
syl2and |
|
| 38 |
|
eleq1 |
|
| 39 |
38
|
adantl |
|
| 40 |
37 39
|
mpbidi |
|
| 41 |
16 40
|
biimtrid |
|
| 42 |
41
|
exlimdv |
|
| 43 |
15 42
|
syl5 |
|
| 44 |
7 43
|
pm2.61dne |
|