Theorem pltne

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

	Ref	Expression
Hypothesis	pltne.s	|- .< = ( lt ` K )
Assertion	pltne	|- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y -> X =/= Y ) )

Proof

Step	Hyp	Ref	Expression
1		pltne.s	|- .< = ( lt ` K )
2		eqid	|- ( le ` K ) = ( le ` K )
3	2 1	pltval	|- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y <-> ( X ( le ` K ) Y /\ X =/= Y ) ) )
4	3	simplbda	|- ( ( ( K e. A /\ X e. B /\ Y e. C ) /\ X .< Y ) -> X =/= Y )
5	4	ex	|- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y -> X =/= Y ) )