cdleme00a

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

	Ref	Expression
Hypotheses	cdleme0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme0.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme0.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme0.a	$⊢ A = Atoms (K)$
Assertion	cdleme00a	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \neq P$

Step	Hyp	Ref	Expression
1		cdleme0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme0.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme0.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme0.a	$⊢ A = Atoms (K)$
5		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in HL$
6		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \in A$
7		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \in A$
8		simp22	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \in A$
9		simp3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
10	1 2 4	atnlej1	$⊢ (K \in HL \land (R \in A \land P \in A \land Q \in A) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \neq P$
11	5 6 7 8 9 10	syl131anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \neq P$

Metamath Proof Explorer