Theorem retos

Description: The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018)

	Ref	Expression
Assertion	retos	⊢ ℝfld ∈ Toset

Proof

Step	Hyp	Ref	Expression
1		ltso	⊢ < Or ℝ
2		idref	⊢ ( ( I ↾ ℝ ) ⊆ ≤ ↔ ∀ 𝑥 ∈ ℝ 𝑥 ≤ 𝑥 )
3		leid	⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ 𝑥 )
4	2 3	mprgbir	⊢ ( I ↾ ℝ ) ⊆ ≤
5		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
6	5	ovexi	⊢ ℝfld ∈ V
7		rebase	⊢ ℝ = ( Base ‘ ℝfld )
8		rele2	⊢ ≤ = ( le ‘ ℝfld )
9		relt	⊢ < = ( lt ‘ ℝfld )
10	7 8 9	tosso	⊢ ( ℝfld ∈ V → ( ℝfld ∈ Toset ↔ ( < Or ℝ ∧ ( I ↾ ℝ ) ⊆ ≤ ) ) )
11	6 10	ax-mp	⊢ ( ℝfld ∈ Toset ↔ ( < Or ℝ ∧ ( I ↾ ℝ ) ⊆ ≤ ) )
12	1 4 11	mpbir2an	⊢ ℝfld ∈ Toset