Metamath Proof Explorer


Theorem pltfval

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

Ref Expression
Hypotheses pltval.l ˙=K
pltval.s <˙=<K
Assertion pltfval KA<˙=˙I

Proof

Step Hyp Ref Expression
1 pltval.l ˙=K
2 pltval.s <˙=<K
3 elex KAKV
4 fveq2 p=Kp=K
5 4 1 eqtr4di p=Kp=˙
6 5 difeq1d p=KpI=˙I
7 df-plt lt=pVpI
8 1 fvexi ˙V
9 8 difexi ˙IV
10 6 7 9 fvmpt KV<K=˙I
11 3 10 syl KA<K=˙I
12 2 11 eqtrid KA<˙=˙I