Theorem prdsbasprj

Description: Each point in a structure product restricts on each coordinate to the relevant base set. (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	⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
	prdsbasprj.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
Assertion	prdsbasprj	⊢ ( 𝜑 → ( 𝑇 ‘ 𝐽 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝐽 ) ) )

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		prdsbasprj.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
8		fveq2	⊢ ( 𝑥 = 𝐽 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝐽 ) )
9		2fveq3	⊢ ( 𝑥 = 𝐽 → ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Base ‘ ( 𝑅 ‘ 𝐽 ) ) )
10	8 9	eleq12d	⊢ ( 𝑥 = 𝐽 → ( ( 𝑇 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↔ ( 𝑇 ‘ 𝐽 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝐽 ) ) ) )
11	1 2 3 4 5	prdsbas2	⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
12	6 11	eleqtrd	⊢ ( 𝜑 → 𝑇 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
13		elixp2	⊢ ( 𝑇 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↔ ( 𝑇 ∈ V ∧ 𝑇 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑇 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
14	13	simp3bi	⊢ ( 𝑇 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑇 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
15	12 14	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝑇 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
16	10 15 7	rspcdva	⊢ ( 𝜑 → ( 𝑇 ‘ 𝐽 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝐽 ) ) )