Theorem ply1basf

Description: Univariate polynomial base set elements are functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	ply1rcl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1rcl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1basf.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion	ply1basf	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		ply1rcl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1rcl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		ply1basf.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
5		eqid	⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
6		psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { 𝑎 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
7		id	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵 )
8		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
9	1 8 2	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
10	7 9	eleqtrdi	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
11	4 3 5 6 10	mplelf	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )