Theorem pltfval

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

	Ref	Expression
Hypotheses	pltval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	pltval.s	$$⊢\underset{\dot{}}{<}={<}_K$$
Assertion	pltfval	$$⊢K\in A\to \underset{\dot{}}{<}=\underset{\dot{}}{\le }\setminus \mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		pltval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		pltval.s	$$⊢\underset{\dot{}}{<}={<}_K$$
3		elex	$$⊢K\in A\to K\in \mathrm{V}$$
4		fveq2	$$⊢p=K\to {\le }_p={\le }_K$$
5	4 1	syl6eqr	$$⊢p=K\to {\le }_p=\underset{\dot{}}{\le }$$
6	5	difeq1d	$$⊢p=K\to {\le }_p\setminus \mathrm{I}=\underset{\dot{}}{\le }\setminus \mathrm{I}$$
7		df-plt	$$⊢\mathrm{lt}=\left(p\in \mathrm{V}⟼{\le }_p\setminus \mathrm{I}\right)$$
8	1	fvexi	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}$$
9	8	difexi	$$⊢\underset{\dot{}}{\le }\setminus \mathrm{I}\in \mathrm{V}$$
10	6 7 9	fvmpt	$$⊢K\in \mathrm{V}\to {<}_K=\underset{\dot{}}{\le }\setminus \mathrm{I}$$
11	3 10	syl	$$⊢K\in A\to {<}_K=\underset{\dot{}}{\le }\setminus \mathrm{I}$$
12	2 11	syl5eq	$$⊢K\in A\to \underset{\dot{}}{<}=\underset{\dot{}}{\le }\setminus \mathrm{I}$$