Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 26-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemk.b | |
|
cdlemk.l | |
||
cdlemk.j | |
||
cdlemk.a | |
||
cdlemk.h | |
||
cdlemk.t | |
||
cdlemk.r | |
||
cdlemk.m | |
||
Assertion | cdlemk8 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemk.b | |
|
2 | cdlemk.l | |
|
3 | cdlemk.j | |
|
4 | cdlemk.a | |
|
5 | cdlemk.h | |
|
6 | cdlemk.t | |
|
7 | cdlemk.r | |
|
8 | cdlemk.m | |
|
9 | coass | |
|
10 | simp1 | |
|
11 | simp2l | |
|
12 | 1 5 6 | ltrn1o | |
13 | 10 11 12 | syl2anc | |
14 | f1ococnv1 | |
|
15 | 13 14 | syl | |
16 | 15 | coeq2d | |
17 | simp2r | |
|
18 | 1 5 6 | ltrn1o | |
19 | 10 17 18 | syl2anc | |
20 | f1of | |
|
21 | fcoi1 | |
|
22 | 19 20 21 | 3syl | |
23 | 16 22 | eqtrd | |
24 | 9 23 | eqtrid | |
25 | 24 | fveq1d | |
26 | 5 6 | ltrncnv | |
27 | 10 11 26 | syl2anc | |
28 | 5 6 | ltrnco | |
29 | 10 17 27 28 | syl3anc | |
30 | simp3l | |
|
31 | 2 4 5 6 | ltrncoval | |
32 | 10 29 11 30 31 | syl121anc | |
33 | 25 32 | eqtr3d | |
34 | 33 | oveq2d | |
35 | 2 4 5 6 | ltrnel | |
36 | 35 | 3adant2r | |
37 | 2 3 4 5 6 7 | trljat1 | |
38 | 10 29 36 37 | syl3anc | |
39 | 34 38 | eqtr4d | |