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

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 ⊢ Y = S ⨉ 𝑠 R
prdsbasmpt.b ⊢ B = Base Y
prdsbasmpt.s ⊢ φ → S ∈ V
prdsbasmpt.i ⊢ φ → I ∈ W
prdsbasmpt.r ⊢ φ → R Fn I
Assertion prdsbasmpt ⊢ φ → x ∈ I ⟼ U ∈ B ↔ ∀ x ∈ I U ∈ Base R ⁡ x

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 1 2 3 4 5 prdsbas2 ⊢ φ → B = ⨉ x ∈ I Base R ⁡ x
7 6 eleq2d ⊢ φ → x ∈ I ⟼ U ∈ B ↔ x ∈ I ⟼ U ∈ ⨉ x ∈ I Base R ⁡ x
8 mptelixpg ⊢ I ∈ W → x ∈ I ⟼ U ∈ ⨉ x ∈ I Base R ⁡ x ↔ ∀ x ∈ I U ∈ Base R ⁡ x
9 4 8 syl ⊢ φ → x ∈ I ⟼ U ∈ ⨉ x ∈ I Base R ⁡ x ↔ ∀ x ∈ I U ∈ Base R ⁡ x
10 7 9 bitrd ⊢ φ → x ∈ I ⟼ U ∈ B ↔ ∀ x ∈ I U ∈ Base R ⁡ x