This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid 
 |-  ( ( 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 ) ) )