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

Metamath Proof Explorer

Theorem pltne

Description: The "less than" relation is not reflexive. ( df-pss analog.) (Contributed by NM, 2-Dec-2011)

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

Step	Hyp	Ref	Expression
1		pltne.s	$⊢ \underset{˙}{<} = <_{K}$
2		eqid	$⊢ \leq_{K} = \leq_{K}$
3	2 1	pltval	$⊢ (K \in A \land X \in B \land Y \in C) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{K} Y \land X \neq Y))$
4	3	simplbda	$⊢ ((K \in A \land X \in B \land Y \in C) \land X \underset{˙}{<} Y) \to X \neq Y$
5	4	ex	$⊢ (K \in A \land X \in B \land Y \in C) \to (X \underset{˙}{<} Y \to X \neq Y)$