Metamath Proof Explorer


Theorem cdleme8tN

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. X represents t_1. In their notation, we prove p \/ t_1 = p \/ t. (Contributed by NM, 8-Oct-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme8t.l ˙ = K
cdleme8t.j ˙ = join K
cdleme8t.m ˙ = meet K
cdleme8t.a A = Atoms K
cdleme8t.h H = LHyp K
cdleme8t.x X = P ˙ T ˙ W
Assertion cdleme8tN K HL W H P A ¬ P ˙ W T A P ˙ X = P ˙ T

Proof

Step Hyp Ref Expression
1 cdleme8t.l ˙ = K
2 cdleme8t.j ˙ = join K
3 cdleme8t.m ˙ = meet K
4 cdleme8t.a A = Atoms K
5 cdleme8t.h H = LHyp K
6 cdleme8t.x X = P ˙ T ˙ W
7 1 2 3 4 5 6 cdleme8 K HL W H P A ¬ P ˙ W T A P ˙ X = P ˙ T