Metamath Proof Explorer

Theorem el2xpss

Description: Version of elrel for triple Cartesian products. (Contributed by Scott Fenton, 1-Feb-2025)

Ref Expression
Assertion el2xpss ⊢ A ∈ R ∧ R ⊆ B × C × D → ∃ x ∃ y ∃ z A = x y z

Proof

Step Hyp Ref Expression
1 ssel2 ⊢ R ⊆ B × C × D ∧ A ∈ R → A ∈ B × C × D
2 1 ancoms ⊢ A ∈ R ∧ R ⊆ B × C × D → A ∈ B × C × D
3 el2xptp ⊢ A ∈ B × C × D ↔ ∃ x ∈ B ∃ y ∈ C ∃ z ∈ D A = x y z
4 rexex ⊢ ∃ z ∈ D A = x y z → ∃ z A = x y z
5 4 reximi ⊢ ∃ y ∈ C ∃ z ∈ D A = x y z → ∃ y ∈ C ∃ z A = x y z
6 rexex ⊢ ∃ y ∈ C ∃ z A = x y z → ∃ y ∃ z A = x y z
7 5 6 syl ⊢ ∃ y ∈ C ∃ z ∈ D A = x y z → ∃ y ∃ z A = x y z
8 7 reximi ⊢ ∃ x ∈ B ∃ y ∈ C ∃ z ∈ D A = x y z → ∃ x ∈ B ∃ y ∃ z A = x y z
9 rexex ⊢ ∃ x ∈ B ∃ y ∃ z A = x y z → ∃ x ∃ y ∃ z A = x y z
10 8 9 syl ⊢ ∃ x ∈ B ∃ y ∈ C ∃ z ∈ D A = x y z → ∃ x ∃ y ∃ z A = x y z
11 3 10 sylbi ⊢ A ∈ B × C × D → ∃ x ∃ y ∃ z A = x y z
12 2 11 syl ⊢ A ∈ R ∧ R ⊆ B × C × D → ∃ x ∃ y ∃ z A = x y z