Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | wlkp1.v | |
|
wlkp1.i | |
||
wlkp1.f | |
||
wlkp1.a | |
||
wlkp1.b | |
||
wlkp1.c | |
||
wlkp1.d | |
||
wlkp1.w | |
||
wlkp1.n | |
||
wlkp1.e | |
||
wlkp1.x | |
||
wlkp1.u | |
||
wlkp1.h | |
||
Assertion | wlkp1lem3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wlkp1.v | |
|
2 | wlkp1.i | |
|
3 | wlkp1.f | |
|
4 | wlkp1.a | |
|
5 | wlkp1.b | |
|
6 | wlkp1.c | |
|
7 | wlkp1.d | |
|
8 | wlkp1.w | |
|
9 | wlkp1.n | |
|
10 | wlkp1.e | |
|
11 | wlkp1.x | |
|
12 | wlkp1.u | |
|
13 | wlkp1.h | |
|
14 | 13 | a1i | |
15 | 14 | fveq1d | |
16 | 9 | fvexi | |
17 | 2 | wlkf | |
18 | lencl | |
|
19 | wrddm | |
|
20 | fzonel | |
|
21 | 9 | a1i | |
22 | simpr | |
|
23 | 21 22 | eleq12d | |
24 | 20 23 | mtbiri | |
25 | 18 19 24 | syl2anc | |
26 | 8 17 25 | 3syl | |
27 | fsnunfv | |
|
28 | 16 5 26 27 | mp3an2i | |
29 | 15 28 | eqtrd | |
30 | 12 29 | fveq12d | |