Metamath Proof Explorer

Theorem cdlemeulpq

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 5-Dec-2012)

Ref Expression
Hypotheses cdleme0.l ⊢≤˙=≤K
cdleme0.j ⊢∨˙=join⁡K
cdleme0.m ⊢∧˙=meet⁡K
cdleme0.a ⊢A=Atoms⁡K
cdleme0.h ⊢H=LHyp⁡K
cdleme0.u ⊢U=P∨˙Q∧˙W
Assertion cdlemeulpq ⊢K∈HL∧W∈H∧P∈A∧Q∈A→U≤˙P∨˙Q

Proof

Step Hyp Ref Expression
1 cdleme0.l ⊢≤˙=≤K
2 cdleme0.j ⊢∨˙=join⁡K
3 cdleme0.m ⊢∧˙=meet⁡K
4 cdleme0.a ⊢A=Atoms⁡K
5 cdleme0.h ⊢H=LHyp⁡K
6 cdleme0.u ⊢U=P∨˙Q∧˙W
7 simpll ⊢K∈HL∧W∈H∧P∈A∧Q∈A→K∈HL
8 7 hllatd ⊢K∈HL∧W∈H∧P∈A∧Q∈A→K∈Lat
9 simprl ⊢K∈HL∧W∈H∧P∈A∧Q∈A→P∈A
10 simprr ⊢K∈HL∧W∈H∧P∈A∧Q∈A→Q∈A
11 eqid ⊢BaseK=BaseK
12 11 2 4 hlatjcl ⊢K∈HL∧P∈A∧Q∈A→P∨˙Q∈BaseK
13 7 9 10 12 syl3anc ⊢K∈HL∧W∈H∧P∈A∧Q∈A→P∨˙Q∈BaseK
14 11 5 lhpbase ⊢W∈H→W∈BaseK
15 14 ad2antlr ⊢K∈HL∧W∈H∧P∈A∧Q∈A→W∈BaseK
16 11 1 3 latmle1 ⊢K∈Lat∧P∨˙Q∈BaseK∧W∈BaseK→P∨˙Q∧˙W≤˙P∨˙Q
17 8 13 15 16 syl3anc ⊢K∈HL∧W∈H∧P∈A∧Q∈A→P∨˙Q∧˙W≤˙P∨˙Q
18 6 17 eqbrtrid ⊢K∈HL∧W∈H∧P∈A∧Q∈A→U≤˙P∨˙Q