Metamath Proof Explorer

Theorem cdleme0fN

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 14-Jun-2012) (New usage is discouraged.)

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