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 <˙=<K
Assertion pltne KAXBYCX<˙YXY

Proof

Step Hyp Ref Expression
1 pltne.s <˙=<K
2 eqid K=K
3 2 1 pltval KAXBYCX<˙YXKYXY
4 3 simplbda KAXBYCX<˙YXY
5 4 ex KAXBYCX<˙YXY