Theorem prdsbasmpt

Description: A constructed tuple is a point in a structure product iff each coordinate is in the proper 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 𝐼 )
Assertion	prdsbasmpt	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐼 𝑈 ∈ ( 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	1 2 3 4 5	prdsbas2	⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
7	6	eleq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
8		mptelixpg	⊢ ( 𝐼 ∈ 𝑊 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐼 𝑈 ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
9	4 8	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐼 𝑈 ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
10	7 9	bitrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐼 𝑈 ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )