This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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