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

Metamath Proof Explorer

Theorem pltfval

Description: Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses pltval.l 
|- .<_ = ( le ` K )
pltval.s 
|- .< = ( lt ` K )
Assertion pltfval 
|- ( K e. A -> .< = ( .<_ \ _I ) )

Proof

Step Hyp Ref Expression
1 pltval.l 
 |-  .<_ = ( le ` K )
2 pltval.s 
 |-  .< = ( lt ` K )
3 elex 
 |-  ( K e. A -> K e. _V )
4 fveq2 
 |-  ( p = K -> ( le ` p ) = ( le ` K ) )
5 4 1 eqtr4di 
 |-  ( p = K -> ( le ` p ) = .<_ )
6 5 difeq1d 
 |-  ( p = K -> ( ( le ` p ) \ _I ) = ( .<_ \ _I ) )
7 df-plt 
 |-  lt = ( p e. _V |-> ( ( le ` p ) \ _I ) )
8 1 fvexi 
 |-  .<_ e. _V
9 8 difexi 
 |-  ( .<_ \ _I ) e. _V
10 6 7 9 fvmpt 
 |-  ( K e. _V -> ( lt ` K ) = ( .<_ \ _I ) )
11 3 10 syl 
 |-  ( K e. A -> ( lt ` K ) = ( .<_ \ _I ) )
12 2 11 eqtrid 
 |-  ( K e. A -> .< = ( .<_ \ _I ) )