Metamath Proof Explorer


Theorem prdsbasmpt2

Description: A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Mario Carneiro, 3-Jul-2015) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypotheses prdsbasmpt2.y Y = S 𝑠 x I R
prdsbasmpt2.b B = Base Y
prdsbasmpt2.s φ S V
prdsbasmpt2.i φ I W
prdsbasmpt2.r φ x I R X
prdsbasmpt2.k K = Base R
Assertion prdsbasmpt2 φ x I U B x I U K

Proof

Step Hyp Ref Expression
1 prdsbasmpt2.y Y = S 𝑠 x I R
2 prdsbasmpt2.b B = Base Y
3 prdsbasmpt2.s φ S V
4 prdsbasmpt2.i φ I W
5 prdsbasmpt2.r φ x I R X
6 prdsbasmpt2.k K = Base R
7 1 2 3 4 5 6 prdsbas3 φ B = x I K
8 7 eleq2d φ x I U B x I U x I K
9 mptelixpg I W x I U x I K x I U K
10 4 9 syl φ x I U x I K x I U K
11 8 10 bitrd φ x I U B x I U K