Theorem prdsbasfn

Description: Points in the structure product are functions; use this with dffn5 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsbasmpt.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsbasmpt.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsbasmpt.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
	prdsbasmpt.t	⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
Assertion	prdsbasfn	⊢ ( 𝜑 → 𝑇 Fn 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		prdsbasmpt.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdsbasmpt.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		prdsbasmpt.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
6		prdsbasmpt.t	⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
7	1 2 3 4 5	prdsbas2	⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
8	6 7	eleqtrd	⊢ ( 𝜑 → 𝑇 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
9		ixpfn	⊢ ( 𝑇 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) → 𝑇 Fn 𝐼 )
10	8 9	syl	⊢ ( 𝜑 → 𝑇 Fn 𝐼 )