Theorem xrslt

Description: The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Assertion	xrslt	⊢ < = ( lt ‘ ℝ*𝑠 )

Proof

Step	Hyp	Ref	Expression
1		dflt2	⊢ < = ( ≤ ∖ I )
2		xrsex	⊢ ℝ*𝑠 ∈ V
3		xrsle	⊢ ≤ = ( le ‘ ℝ*𝑠 )
4		eqid	⊢ ( lt ‘ ℝ*𝑠 ) = ( lt ‘ ℝ*𝑠 )
5	3 4	pltfval	⊢ ( ℝ*𝑠 ∈ V → ( lt ‘ ℝ*𝑠 ) = ( ≤ ∖ I ) )
6	2 5	ax-mp	⊢ ( lt ‘ ℝ*𝑠 ) = ( ≤ ∖ I )
7	1 6	eqtr4i	⊢ < = ( lt ‘ ℝ*𝑠 )