Theorem pltval

Description: Less-than relation. ( df-pss analog.) (Contributed by NM, 12-Oct-2011)

	Ref	Expression
Hypotheses	pltval.l	|- .<_ = ( le ` K )
	pltval.s	|- .< = ( lt ` K )
Assertion	pltval	|- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		pltval.l	|- .<_ = ( le ` K )
2		pltval.s	|- .< = ( lt ` K )
3	1 2	pltfval	|- ( K e. A -> .< = ( .<_ \ _I ) )
4	3	breqd	|- ( K e. A -> ( X .< Y <-> X ( .<_ \ _I ) Y ) )
5		brdif	|- ( X ( .<_ \ _I ) Y <-> ( X .<_ Y /\ -. X _I Y ) )
6		ideqg	|- ( Y e. C -> ( X _I Y <-> X = Y ) )
7	6	necon3bbid	|- ( Y e. C -> ( -. X _I Y <-> X =/= Y ) )
8	7	adantl	|- ( ( X e. B /\ Y e. C ) -> ( -. X _I Y <-> X =/= Y ) )
9	8	anbi2d	|- ( ( X e. B /\ Y e. C ) -> ( ( X .<_ Y /\ -. X _I Y ) <-> ( X .<_ Y /\ X =/= Y ) ) )
10	5 9	syl5bb	|- ( ( X e. B /\ Y e. C ) -> ( X ( .<_ \ _I ) Y <-> ( X .<_ Y /\ X =/= Y ) ) )
11	4 10	sylan9bb	|- ( ( K e. A /\ ( X e. B /\ Y e. C ) ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) )
12	11	3impb	|- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) )