Theorem fseqsupcl

Description: The values of a finite real sequence have a supremum. (Contributed by NM, 20-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	fseqsupcl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		frn	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ran 𝐹 ⊆ ℝ )
2	1	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ran 𝐹 ⊆ ℝ )
3		fzfi	⊢ ( 𝑀 ... 𝑁 ) ∈ Fin
4		ffn	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → 𝐹 Fn ( 𝑀 ... 𝑁 ) )
5	4	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → 𝐹 Fn ( 𝑀 ... 𝑁 ) )
6		dffn4	⊢ ( 𝐹 Fn ( 𝑀 ... 𝑁 ) ↔ 𝐹 : ( 𝑀 ... 𝑁 ) –onto→ ran 𝐹 )
7	5 6	sylib	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → 𝐹 : ( 𝑀 ... 𝑁 ) –onto→ ran 𝐹 )
8		fofi	⊢ ( ( ( 𝑀 ... 𝑁 ) ∈ Fin ∧ 𝐹 : ( 𝑀 ... 𝑁 ) –onto→ ran 𝐹 ) → ran 𝐹 ∈ Fin )
9	3 7 8	sylancr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ran 𝐹 ∈ Fin )
10		fdm	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → dom 𝐹 = ( 𝑀 ... 𝑁 ) )
11	10	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → dom 𝐹 = ( 𝑀 ... 𝑁 ) )
12		fzn0	⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
13	12	biranri	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ( 𝑀 ... 𝑁 ) ≠ ∅ )
14	11 13	eqnetrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → dom 𝐹 ≠ ∅ )
15		dm0rn0	⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
16	15	necon3bii	⊢ ( dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅ )
17	14 16	sylib	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → ran 𝐹 ≠ ∅ )
18		ltso	⊢ < Or ℝ
19		fisupcl	⊢ ( ( < Or ℝ ∧ ( ran 𝐹 ∈ Fin ∧ ran 𝐹 ≠ ∅ ∧ ran 𝐹 ⊆ ℝ ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
20	18 19	mpan	⊢ ( ( ran 𝐹 ∈ Fin ∧ ran 𝐹 ≠ ∅ ∧ ran 𝐹 ⊆ ℝ ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
21	9 17 2 20	syl3anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
22	2 21	sseldd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )