Metamath Proof Explorer


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 ‘ ( 𝑅𝑥 ) ) ) )