4atlem0be

	Ref	Expression
Hypotheses	4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4at.j	$⊢ \underset{˙}{\lor} = join (K)$
	4at.a	$⊢ A = Atoms (K)$
Assertion	4atlem0be	$⊢ (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 \neq R$

Step	Hyp	Ref	Expression
1		4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4at.a	$⊢ A = Atoms (K)$
4		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$
5		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$
6		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$
7		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$
8		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)$
9	1 2 3	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$
10	9	necomd	$⊢ (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 P \neq R$
11	4 5 6 7 8 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 P \neq R$

Metamath Proof Explorer