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