Metamath Proof Explorer


Theorem cdleme10tN

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

Ref Expression
Hypotheses cdleme10t.l ˙=K
cdleme10t.j ˙=joinK
cdleme10t.m ˙=meetK
cdleme10t.a A=AtomsK
cdleme10t.h H=LHypK
cdleme10t.y Y=R˙T˙W
Assertion cdleme10tN KHLWHRATA¬T˙WT˙Y=T˙R

Proof

Step Hyp Ref Expression
1 cdleme10t.l ˙=K
2 cdleme10t.j ˙=joinK
3 cdleme10t.m ˙=meetK
4 cdleme10t.a A=AtomsK
5 cdleme10t.h H=LHypK
6 cdleme10t.y Y=R˙T˙W
7 1 2 3 4 5 6 cdleme10 KHLWHRATA¬T˙WT˙Y=T˙R