Metamath Proof Explorer

Theorem cdleme0b

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 13-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
Assertion cdleme0b ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → U ≠ P

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 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → K ∈ HL
8 7 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → K ∈ Lat
9 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∈ A
10 eqid ⊢ Base K = Base K
11 10 4 atbase ⊢ P ∈ A → P ∈ Base K
12 9 11 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∈ Base K
13 10 4 atbase ⊢ Q ∈ A → Q ∈ Base K
14 13 3ad2ant3 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → Q ∈ Base K
15 10 2 latjcl ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K → P ∨ ˙ Q ∈ Base K
16 8 12 14 15 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
17 simp1r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → W ∈ H
18 10 5 lhpbase ⊢ W ∈ H → W ∈ Base K
19 17 18 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → W ∈ Base K
20 10 1 3 latmle2 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ W ∈ Base K → P ∨ ˙ Q ∧ ˙ W ≤ ˙ W
21 8 16 19 20 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ Q ∧ ˙ W ≤ ˙ W
22 6 21 eqbrtrid ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → U ≤ ˙ W
23 simp2r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → ¬ P ≤ ˙ W
24 nbrne2 ⊢ U ≤ ˙ W ∧ ¬ P ≤ ˙ W → U ≠ P
25 22 23 24 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → U ≠ P