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 ⊢ Base K = Base K
12 11 2 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
13 7 9 10 12 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
14 11 5 lhpbase ⊢ W ∈ H → W ∈ Base K
15 14 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A → W ∈ Base K
16 11 1 3 latmle1 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ W ∈ Base K → 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