Metamath Proof Explorer


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