Metamath Proof Explorer


Theorem cdleme9a

Description: Part of proof of Lemma E in Crawley p. 113. C represents s_1, which we prove is an atom. (Contributed by NM, 10-Jun-2012)

Ref Expression
Hypotheses cdleme8.l
|- .<_ = ( le ` K )
cdleme8.j
|- .\/ = ( join ` K )
cdleme8.m
|- ./\ = ( meet ` K )
cdleme8.a
|- A = ( Atoms ` K )
cdleme8.h
|- H = ( LHyp ` K )
cdleme8.4
|- C = ( ( P .\/ S ) ./\ W )
Assertion cdleme9a
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( S e. A /\ P =/= S ) ) -> C e. A )

Proof

Step Hyp Ref Expression
1 cdleme8.l
 |-  .<_ = ( le ` K )
2 cdleme8.j
 |-  .\/ = ( join ` K )
3 cdleme8.m
 |-  ./\ = ( meet ` K )
4 cdleme8.a
 |-  A = ( Atoms ` K )
5 cdleme8.h
 |-  H = ( LHyp ` K )
6 cdleme8.4
 |-  C = ( ( P .\/ S ) ./\ W )
7 1 2 3 4 5 6 lhpat2
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( S e. A /\ P =/= S ) ) -> C e. A )