Theorem relt

Description: The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018)

	Ref	Expression
Assertion	relt	⊢ < = ( lt ‘ ℝfld )

Proof

Step	Hyp	Ref	Expression
1		dflt2	⊢ < = ( ≤ ∖ I )
2		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
3	2	ovexi	⊢ ℝfld ∈ V
4		rele2	⊢ ≤ = ( le ‘ ℝfld )
5		eqid	⊢ ( lt ‘ ℝfld ) = ( lt ‘ ℝfld )
6	4 5	pltfval	⊢ ( ℝfld ∈ V → ( lt ‘ ℝfld ) = ( ≤ ∖ I ) )
7	3 6	ax-mp	⊢ ( lt ‘ ℝfld ) = ( ≤ ∖ I )
8	1 7	eqtr4i	⊢ < = ( lt ‘ ℝfld )