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