# Metamath Proof Explorer

## Theorem cdleme22b

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 5th line on p. 115. Show that t \/ v =/= p \/ q and s <_ p \/ q implies -. t <_ p \/ q. (Contributed by NM, 2-Dec-2012)

Ref Expression
Hypotheses cdleme22.l
cdleme22.j
cdleme22.m
cdleme22.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdleme22.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
Assertion cdleme22b

### Proof

Step Hyp Ref Expression
1 cdleme22.l
2 cdleme22.j
3 cdleme22.m
4 cdleme22.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdleme22.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 simp1l
7 simp1r1
8 simp1r2
9 simp1r3
10 eqid ${⊢}\mathrm{LLines}\left({K}\right)=\mathrm{LLines}\left({K}\right)$
11 2 4 10 llni2
12 6 7 8 9 11 syl31anc
13 4 10 llnneat
14 6 12 13 syl2anc
15 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
16 15 10 llnn0
17 6 12 16 syl2anc
18 14 17 jca
19 df-ne
20 19 anbi2i
21 pm4.56
22 20 21 bitri
23 18 22 sylib
24 simp3r2
25 simp3l
26 1 2 4 hlatlej1
27 6 8 25 26 syl3anc
28 6 hllatd
29 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
30 29 4 atbase ${⊢}{S}\in {A}\to {S}\in {\mathrm{Base}}_{{K}}$
31 7 30 syl
32 29 4 atbase ${⊢}{T}\in {A}\to {T}\in {\mathrm{Base}}_{{K}}$
33 8 32 syl
34 29 2 4 hlatjcl
35 6 8 25 34 syl3anc
36 29 1 2 latjle12
37 28 31 33 35 36 syl13anc
38 24 27 37 mpbi2and
40 simp3r3
42 simpr
43 simp21
44 simp22
45 29 2 4 hlatjcl
46 6 43 44 45 syl3anc
47 29 1 2 latjle12
48 28 31 33 46 47 syl13anc
50 41 42 49 mpbi2and
51 29 2 4 hlatjcl
52 6 7 8 51 syl3anc
53 29 1 3 latlem12
54 28 52 35 46 53 syl13anc
56 39 50 55 mpbi2and
57 56 ex
58 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
59 6 58 syl
62 simprl
63 simprr
64 29 1 15 4 leat3
65 60 61 62 63 64 syl31anc
66 65 exp32
67 breq2
68 67 biimpa
69 29 1 15 ople0
70 59 52 69 syl2anc
71 68 70 syl5ib
72 71 imp
73 72 olcd
74 73 exp32
75 simp3r1
76 2 3 15 4 2atmat0
77 6 8 25 43 44 75 76 syl33anc
78 66 74 77 mpjaod
79 57 78 syld
80 23 79 mtod