atnlt

Description: Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012)

	Ref	Expression
Hypotheses	atnlt.s	$⊢ \underset{˙}{<} = <_{K}$
	atnlt.a	$⊢ A = Atoms (K)$
Assertion	atnlt	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to \neg P \underset{˙}{<} Q$

Step	Hyp	Ref	Expression
1		atnlt.s	$⊢ \underset{˙}{<} = <_{K}$
2		atnlt.a	$⊢ A = Atoms (K)$
3	1	pltirr	$⊢ (K \in AtLat \land P \in A) \to \neg P \underset{˙}{<} P$
4	3	3adant3	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to \neg P \underset{˙}{<} P$
5		breq2	$⊢ P = Q \to (P \underset{˙}{<} P \leftrightarrow P \underset{˙}{<} Q)$
6	5	notbid	$⊢ P = Q \to (\neg P \underset{˙}{<} P \leftrightarrow \neg P \underset{˙}{<} Q)$
7	4 6	syl5ibcom	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P = Q \to \neg P \underset{˙}{<} Q)$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9	8 1	pltle	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \underset{˙}{<} Q \to P \leq_{K} Q)$
10	8 2	atcmp	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \leq_{K} Q \leftrightarrow P = Q)$
11	9 10	sylibd	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \underset{˙}{<} Q \to P = Q)$
12	11	necon3ad	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \neq Q \to \neg P \underset{˙}{<} Q)$
13	7 12	pm2.61dne	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to \neg P \underset{˙}{<} Q$

Metamath Proof Explorer