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 = Base K
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 = Base K
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