Theorem pltfval

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

	Ref	Expression
Hypotheses	pltval.l	⊢ ≤ = ( le ‘ 𝐾 )
	pltval.s	⊢ < = ( lt ‘ 𝐾 )
Assertion	pltfval	⊢ ( 𝐾 ∈ 𝐴 → < = ( ≤ ∖ I ) )

Proof

Step	Hyp	Ref	Expression
1		pltval.l	⊢ ≤ = ( le ‘ 𝐾 )
2		pltval.s	⊢ < = ( lt ‘ 𝐾 )
3		elex	⊢ ( 𝐾 ∈ 𝐴 → 𝐾 ∈ V )
4		fveq2	⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ( le ‘ 𝐾 ) )
5	4 1	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ≤ )
6	5	difeq1d	⊢ ( 𝑝 = 𝐾 → ( ( le ‘ 𝑝 ) ∖ I ) = ( ≤ ∖ I ) )
7		df-plt	⊢ lt = ( 𝑝 ∈ V ↦ ( ( le ‘ 𝑝 ) ∖ I ) )
8	1	fvexi	⊢ ≤ ∈ V
9	8	difexi	⊢ ( ≤ ∖ I ) ∈ V
10	6 7 9	fvmpt	⊢ ( 𝐾 ∈ V → ( lt ‘ 𝐾 ) = ( ≤ ∖ I ) )
11	3 10	syl	⊢ ( 𝐾 ∈ 𝐴 → ( lt ‘ 𝐾 ) = ( ≤ ∖ I ) )
12	2 11	eqtrid	⊢ ( 𝐾 ∈ 𝐴 → < = ( ≤ ∖ I ) )