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

Metamath Proof Explorer

Theorem pltirr

Description: The "less than" relation is not reflexive. ( pssirr analog.) (Contributed by NM, 7-Feb-2012)

		Ref	Expression
	Hypothesis	pltne.s	$⊢ \underset{˙}{<} = <_{K}$
	Assertion	pltirr	$⊢ (K \in A \land X \in B) \to \neg X \underset{˙}{<} X$

Step	Hyp	Ref	Expression
1		pltne.s	$⊢ \underset{˙}{<} = <_{K}$
2		eqid	$⊢ X = X$
3	1	pltne	$⊢ (K \in A \land X \in B \land X \in B) \to (X \underset{˙}{<} X \to X \neq X)$
4	3	3anidm23	$⊢ (K \in A \land X \in B) \to (X \underset{˙}{<} X \to X \neq X)$
5	4	necon2bd	$⊢ (K \in A \land X \in B) \to (X = X \to \neg X \underset{˙}{<} X)$
6	2 5	mpi	$⊢ (K \in A \land X \in B) \to \neg X \underset{˙}{<} X$