Theorem pltval3

Description: Alternate expression for the "less than" relation. ( dfpss3 analog.) (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	pleval2.b	|- B = ( Base ` K )
	pleval2.l	|- .<_ = ( le ` K )
	pleval2.s	|- .< = ( lt ` K )
Assertion	pltval3	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( 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	posref	|- ( ( K e. Poset /\ X e. B ) -> X .<_ X )
6	5	3adant3	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> X .<_ X )
7		breq1	|- ( X = Y -> ( X .<_ X <-> Y .<_ X ) )
8	6 7	syl5ibcom	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X = Y -> Y .<_ X ) )
9	8	adantr	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( X = Y -> Y .<_ X ) )
10	1 2	posasymb	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ Y .<_ X ) <-> X = Y ) )
11	10	biimpd	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) )
12	11	expdimp	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( Y .<_ X -> X = Y ) )
13	9 12	impbid	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( X = Y <-> Y .<_ X ) )
14	13	necon3abid	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( X =/= Y <-> -. Y .<_ X ) )
15	14	pm5.32da	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ X =/= Y ) <-> ( X .<_ Y /\ -. Y .<_ X ) ) )
16	4 15	bitrd	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( X .<_ Y /\ -. Y .<_ X ) ) )