Metamath Proof Explorer

Theorem cdleme0aa

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 14-Jun-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
cdleme0.b ⊢B=BaseK
Assertion cdleme0aa ⊢K∈HL∧W∈H∧P∈A∧Q∈A→U∈B

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 cdleme0.b ⊢B=BaseK
8 simp1l ⊢K∈HL∧W∈H∧P∈A∧Q∈A→K∈HL
9 8 hllatd ⊢K∈HL∧W∈H∧P∈A∧Q∈A→K∈Lat
10 7 4 atbase ⊢P∈A→P∈B
11 10 3ad2ant2 ⊢K∈HL∧W∈H∧P∈A∧Q∈A→P∈B
12 7 4 atbase ⊢Q∈A→Q∈B
13 12 3ad2ant3 ⊢K∈HL∧W∈H∧P∈A∧Q∈A→Q∈B
14 7 2 latjcl ⊢K∈Lat∧P∈B∧Q∈B→P∨˙Q∈B
15 9 11 13 14 syl3anc ⊢K∈HL∧W∈H∧P∈A∧Q∈A→P∨˙Q∈B
16 simp1r ⊢K∈HL∧W∈H∧P∈A∧Q∈A→W∈H
17 7 5 lhpbase ⊢W∈H→W∈B
18 16 17 syl ⊢K∈HL∧W∈H∧P∈A∧Q∈A→W∈B
19 7 3 latmcl ⊢K∈Lat∧P∨˙Q∈B∧W∈B→P∨˙Q∧˙W∈B
20 9 15 18 19 syl3anc ⊢K∈HL∧W∈H∧P∈A∧Q∈A→P∨˙Q∧˙W∈B
21 6 20 eqeltrid ⊢K∈HL∧W∈H∧P∈A∧Q∈A→U∈B