2atneat

Description: The join of two distinct atoms is not an atom. (Contributed by NM, 12-Oct-2012)

	Ref	Expression
Hypotheses	2atneat.j	$⊢ \underset{˙}{\lor} = join (K)$
	2atneat.a	$⊢ A = Atoms (K)$
Assertion	2atneat	$⊢ (K \in HL \land (P \in A \land Q \in A \land P \neq Q)) \to \neg P \underset{˙}{\lor} Q \in A$

Step	Hyp	Ref	Expression
1		2atneat.j	$⊢ \underset{˙}{\lor} = join (K)$
2		2atneat.a	$⊢ A = Atoms (K)$
3		simpl	$⊢ (K \in HL \land (P \in A \land Q \in A \land P \neq Q)) \to K \in HL$
4		simpr1	$⊢ (K \in HL \land (P \in A \land Q \in A \land P \neq Q)) \to P \in A$
5		simpr2	$⊢ (K \in HL \land (P \in A \land Q \in A \land P \neq Q)) \to Q \in A$
6		simpr3	$⊢ (K \in HL \land (P \in A \land Q \in A \land P \neq Q)) \to P \neq Q$
7		eqid	$⊢ LLines (K) = LLines (K)$
8	1 2 7	llni2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to P \underset{˙}{\lor} Q \in LLines (K)$
9	3 4 5 6 8	syl31anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land P \neq Q)) \to P \underset{˙}{\lor} Q \in LLines (K)$
10	2 7	llnneat	$⊢ (K \in HL \land P \underset{˙}{\lor} Q \in LLines (K)) \to \neg P \underset{˙}{\lor} Q \in A$
11	9 10	syldan	$⊢ (K \in HL \land (P \in A \land Q \in A \land P \neq Q)) \to \neg P \underset{˙}{\lor} Q \in A$

Metamath Proof Explorer