Theorem pltnle

Description: "Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011)

	Ref	Expression
Hypotheses	pleval2.b	|- B = ( Base ` K )
	pleval2.l	|- .<_ = ( le ` K )
	pleval2.s	|- .< = ( lt ` K )
Assertion	pltnle	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .< Y ) -> -. Y .<_ X )

Proof

Step	Hyp	Ref	Expression
1		pleval2.b	|- B = ( Base ` K )
2		pleval2.l	|- .<_ = ( le ` K )
3		pleval2.s	|- .< = ( lt ` K )
4	2 3	pltval	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) )
5	1 2	posasymb	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ Y .<_ X ) <-> X = Y ) )
6	5	biimpd	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) )
7	6	expdimp	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( Y .<_ X -> X = Y ) )
8	7	necon3ad	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( X =/= Y -> -. Y .<_ X ) )
9	8	expimpd	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ X =/= Y ) -> -. Y .<_ X ) )
10	4 9	sylbid	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .< Y -> -. Y .<_ X ) )
11	10	imp	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .< Y ) -> -. Y .<_ X )