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