Description: Properties of a translation of an element not under W . TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw ? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemg4.l | |
|
cdlemg4.a | |
||
cdlemg4.h | |
||
cdlemg4.t | |
||
cdlemg4.b | |
||
Assertion | cdlemg7fvbwN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemg4.l | |
|
2 | cdlemg4.a | |
|
3 | cdlemg4.h | |
|
4 | cdlemg4.t | |
|
5 | cdlemg4.b | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | 5 1 6 7 2 3 | lhpmcvr2 | |
9 | 8 | 3adant3 | |
10 | simp11 | |
|
11 | simp2 | |
|
12 | simp3l | |
|
13 | 11 12 | jca | |
14 | simp12 | |
|
15 | simp13 | |
|
16 | simp3r | |
|
17 | 3 4 1 6 2 7 5 | cdlemg2fv | |
18 | 10 13 14 15 16 17 | syl122anc | |
19 | simp11l | |
|
20 | 19 | hllatd | |
21 | 1 2 3 4 | ltrnel | |
22 | 21 | simpld | |
23 | 10 15 13 22 | syl3anc | |
24 | 5 2 | atbase | |
25 | 23 24 | syl | |
26 | simp12l | |
|
27 | simp11r | |
|
28 | 5 3 | lhpbase | |
29 | 27 28 | syl | |
30 | 5 7 | latmcl | |
31 | 20 26 29 30 | syl3anc | |
32 | 5 6 | latjcl | |
33 | 20 25 31 32 | syl3anc | |
34 | 18 33 | eqeltrd | |
35 | 21 | simprd | |
36 | 10 15 13 35 | syl3anc | |
37 | 5 1 6 | latlej1 | |
38 | 20 25 31 37 | syl3anc | |
39 | 5 1 | lattr | |
40 | 20 25 33 29 39 | syl13anc | |
41 | 38 40 | mpand | |
42 | 36 41 | mtod | |
43 | 18 | breq1d | |
44 | 42 43 | mtbird | |
45 | 34 44 | jca | |
46 | 45 | rexlimdv3a | |
47 | 9 46 | mpd | |