Theorem iccpartf

Description: The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 14-Jul-2020)

	Ref	Expression
Hypotheses	iccpartgtprec.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion	iccpartf	⊢ ( 𝜑 → 𝑃 : ( 0 ... 𝑀 ) ⟶ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3		iccpart	⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
4		elmapfn	⊢ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) → 𝑃 Fn ( 0 ... 𝑀 ) )
5	4	adantr	⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → 𝑃 Fn ( 0 ... 𝑀 ) )
6	3 5	biimtrdi	⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) → 𝑃 Fn ( 0 ... 𝑀 ) ) )
7	1 2 6	sylc	⊢ ( 𝜑 → 𝑃 Fn ( 0 ... 𝑀 ) )
8	1 2	iccpartrn	⊢ ( 𝜑 → ran 𝑃 ⊆ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )
9		df-f	⊢ ( 𝑃 : ( 0 ... 𝑀 ) ⟶ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ↔ ( 𝑃 Fn ( 0 ... 𝑀 ) ∧ ran 𝑃 ⊆ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ) )
10	7 8 9	sylanbrc	⊢ ( 𝜑 → 𝑃 : ( 0 ... 𝑀 ) ⟶ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )