pltfval

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

	Ref	Expression
Hypotheses	pltval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pltval.s	$⊢ \underset{˙}{<} = <_{K}$
Assertion	pltfval	$⊢ K \in A \to \underset{˙}{<} = \underset{˙}{\leq} ∖ I$

Step	Hyp	Ref	Expression
1		pltval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		pltval.s	$⊢ \underset{˙}{<} = <_{K}$
3		elex	$⊢ K \in A \to K \in V$
4		fveq2	$⊢ p = K \to \leq_{p} = \leq_{K}$
5	4 1	eqtr4di	$⊢ p = K \to \leq_{p} = \underset{˙}{\leq}$
6	5	difeq1d	$⊢ p = K \to \leq_{p} ∖ I = \underset{˙}{\leq} ∖ I$
7		df-plt	$⊢ lt = (p \in V ⟼ \leq_{p} ∖ I)$
8	1	fvexi	$⊢ \underset{˙}{\leq} \in V$
9	8	difexi	$⊢ \underset{˙}{\leq} ∖ I \in V$
10	6 7 9	fvmpt	$⊢ K \in V \to <_{K} = \underset{˙}{\leq} ∖ I$
11	3 10	syl	$⊢ K \in A \to <_{K} = \underset{˙}{\leq} ∖ I$
12	2 11	eqtrid	$⊢ K \in A \to \underset{˙}{<} = \underset{˙}{\leq} ∖ I$

Metamath Proof Explorer