Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 6th and 7th lines on p. 115. F , G represent f(s), f(t) respectively. If s <_ t \/ v and -. s <_ p \/ q, then f(s) <_ f(t) \/ v. (Contributed by NM, 6-Dec-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdleme22.l | |
|
cdleme22.j | |
||
cdleme22.m | |
||
cdleme22.a | |
||
cdleme22.h | |
||
cdleme22g.u | |
||
cdleme22g.f | |
||
cdleme22g.g | |
||
Assertion | cdleme22g | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme22.l | |
|
2 | cdleme22.j | |
|
3 | cdleme22.m | |
|
4 | cdleme22.a | |
|
5 | cdleme22.h | |
|
6 | cdleme22g.u | |
|
7 | cdleme22g.f | |
|
8 | cdleme22g.g | |
|
9 | simp11l | |
|
10 | 9 | hllatd | |
11 | simp11 | |
|
12 | simp2l | |
|
13 | simp2r | |
|
14 | simp31 | |
|
15 | simp133 | |
|
16 | simp132 | |
|
17 | 1 2 3 4 5 6 7 | cdleme3fa | |
18 | 11 12 13 14 15 16 17 | syl132anc | |
19 | simp12 | |
|
20 | simp131 | |
|
21 | 1 2 3 4 5 6 8 | cdleme3fa | |
22 | 11 12 13 19 15 20 21 | syl132anc | |
23 | eqid | |
|
24 | 23 2 4 | hlatjcl | |
25 | 9 18 22 24 | syl3anc | |
26 | simp11r | |
|
27 | 23 5 | lhpbase | |
28 | 26 27 | syl | |
29 | 23 1 3 | latmle1 | |
30 | 10 25 28 29 | syl3anc | |
31 | simp33 | |
|
32 | simp32 | |
|
33 | 1 2 3 4 5 | cdleme22d | |
34 | 11 14 19 31 32 33 | syl131anc | |
35 | simp32l | |
|
36 | 15 35 | jca | |
37 | 1 2 3 4 5 6 7 8 | cdleme16 | |
38 | 11 12 13 14 19 36 16 20 37 | syl332anc | |
39 | 34 38 | eqtr2d | |
40 | 2 4 | hlatjcom | |
41 | 9 18 22 40 | syl3anc | |
42 | 30 39 41 | 3brtr3d | |
43 | hlcvl | |
|
44 | 9 43 | syl | |
45 | simp33l | |
|
46 | simp33r | |
|
47 | 1 2 3 4 5 6 8 | cdleme3 | |
48 | 11 12 13 19 15 20 47 | syl132anc | |
49 | nbrne2 | |
|
50 | 46 48 49 | syl2anc | |
51 | 1 2 4 | cvlatexch1 | |
52 | 44 45 18 22 50 51 | syl131anc | |
53 | 42 52 | mpd | |