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 ⊢ Y = S ⨉ 𝑠 R
prdsbasmpt.b ⊢ B = Base Y
prdsbasmpt.s ⊢ φ → S ∈ V
prdsbasmpt.i ⊢ φ → I ∈ W
prdsbasmpt.r ⊢ φ → R Fn I
prdsbasmpt.t ⊢ φ → T ∈ B
prdsbasprj.j ⊢ φ → J ∈ I
Assertion prdsbasprj ⊢ φ → T ⁡ J ∈ Base R ⁡ J

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y ⊢ Y = S ⨉ 𝑠 R
2 prdsbasmpt.b ⊢ B = Base Y
3 prdsbasmpt.s ⊢ φ → S ∈ V
4 prdsbasmpt.i ⊢ φ → I ∈ W
5 prdsbasmpt.r ⊢ φ → R Fn I
6 prdsbasmpt.t ⊢ φ → T ∈ B
7 prdsbasprj.j ⊢ φ → J ∈ I
8 fveq2 ⊢ x = J → T ⁡ x = T ⁡ J
9 2fveq3 ⊢ x = J → Base R ⁡ x = Base R ⁡ J
10 8 9 eleq12d ⊢ x = J → T ⁡ x ∈ Base R ⁡ x ↔ T ⁡ J ∈ Base R ⁡ J
11 1 2 3 4 5 prdsbas2 ⊢ φ → B = ⨉ x ∈ I Base R ⁡ x
12 6 11 eleqtrd ⊢ φ → T ∈ ⨉ x ∈ I Base R ⁡ x
13 elixp2 ⊢ T ∈ ⨉ x ∈ I Base R ⁡ x ↔ T ∈ V ∧ T Fn I ∧ ∀ x ∈ I T ⁡ x ∈ Base R ⁡ x
14 13 simp3bi ⊢ T ∈ ⨉ x ∈ I Base R ⁡ x → ∀ x ∈ I T ⁡ x ∈ Base R ⁡ x
15 12 14 syl ⊢ φ → ∀ x ∈ I T ⁡ x ∈ Base R ⁡ x
16 10 15 7 rspcdva ⊢ φ → T ⁡ J ∈ Base R ⁡ J