Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | vdwlem3.v | |
|
vdwlem3.w | |
||
vdwlem4.r | |
||
vdwlem4.h | |
||
vdwlem4.f | |
||
vdwlem7.m | |
||
vdwlem7.g | |
||
vdwlem7.k | |
||
vdwlem7.a | |
||
vdwlem7.d | |
||
vdwlem7.s | |
||
Assertion | vdwlem7 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vdwlem3.v | |
|
2 | vdwlem3.w | |
|
3 | vdwlem4.r | |
|
4 | vdwlem4.h | |
|
5 | vdwlem4.f | |
|
6 | vdwlem7.m | |
|
7 | vdwlem7.g | |
|
8 | vdwlem7.k | |
|
9 | vdwlem7.a | |
|
10 | vdwlem7.d | |
|
11 | vdwlem7.s | |
|
12 | ovex | |
|
13 | 2nn0 | |
|
14 | eluznn0 | |
|
15 | 13 8 14 | sylancr | |
16 | eqid | |
|
17 | 12 15 7 6 16 | vdwpc | |
18 | 1 | ad2antrr | |
19 | 2 | ad2antrr | |
20 | 3 | ad2antrr | |
21 | 4 | ad2antrr | |
22 | 6 | ad2antrr | |
23 | 7 | ad2antrr | |
24 | 8 | ad2antrr | |
25 | 9 | ad2antrr | |
26 | 10 | ad2antrr | |
27 | 11 | ad2antrr | |
28 | simplrl | |
|
29 | simplrr | |
|
30 | nnex | |
|
31 | ovex | |
|
32 | 30 31 | elmap | |
33 | 29 32 | sylib | |
34 | simprl | |
|
35 | fveq2 | |
|
36 | 35 | oveq2d | |
37 | 36 35 | oveq12d | |
38 | 36 | fveq2d | |
39 | 38 | sneqd | |
40 | 39 | imaeq2d | |
41 | 37 40 | sseq12d | |
42 | 41 | cbvralvw | |
43 | 34 42 | sylib | |
44 | 38 | cbvmptv | |
45 | simprr | |
|
46 | eqid | |
|
47 | eqid | |
|
48 | 18 19 20 21 5 22 23 24 25 26 27 28 33 43 44 45 46 47 | vdwlem6 | |
49 | 48 | ex | |
50 | 49 | rexlimdvva | |
51 | 17 50 | sylbid | |