This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme8t.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme8t.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme8t.a	$⊢ A = Atoms (K)$
	cdleme8t.h	$⊢ H = LHyp (K)$
	cdleme8t.x	$⊢ X = (P \underset{˙}{\lor} T) \underset{˙}{\land} W$
Assertion	cdleme8tN	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land T \in A) \to P \underset{˙}{\lor} X = P \underset{˙}{\lor} T$

Proof

Step	Hyp	Ref	Expression
1		cdleme8t.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme8t.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme8t.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme8t.a	$⊢ A = Atoms (K)$
5		cdleme8t.h	$⊢ H = LHyp (K)$
6		cdleme8t.x	$⊢ X = (P \underset{˙}{\lor} T) \underset{˙}{\land} W$
7	1 2 3 4 5 6	cdleme8	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land T \in A) \to P \underset{˙}{\lor} X = P \underset{˙}{\lor} T$