Theorem el2xpss

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

	Ref	Expression
Assertion	el2xpss	$$⊢\left(A\in R\wedge R\subseteq \left(B\times C\right)\times D\right)\to \exists x\exists y\exists zA=⟨x,y,z⟩$$

Proof

Step	Hyp	Ref	Expression
1		ssel2	$$⊢\left(R\subseteq \left(B\times C\right)\times D\wedge A\in R\right)\to A\in \left(\left(B\times C\right)\times D\right)$$
2	1	ancoms	$$⊢\left(A\in R\wedge R\subseteq \left(B\times C\right)\times D\right)\to A\in \left(\left(B\times C\right)\times D\right)$$
3		el2xptp	$$⊢A\in \left(\left(B\times C\right)\times D\right)\leftrightarrow \exists x\in B\exists y\in C\exists z\in DA=⟨x,y,z⟩$$
4		rexex	$$⊢\exists z\in DA=⟨x,y,z⟩\to \exists zA=⟨x,y,z⟩$$
5	4	reximi	$$⊢\exists y\in C\exists z\in DA=⟨x,y,z⟩\to \exists y\in C\exists zA=⟨x,y,z⟩$$
6		rexex	$$⊢\exists y\in C\exists zA=⟨x,y,z⟩\to \exists y\exists zA=⟨x,y,z⟩$$
7	5 6	syl	$$⊢\exists y\in C\exists z\in DA=⟨x,y,z⟩\to \exists y\exists zA=⟨x,y,z⟩$$
8	7	reximi	$$⊢\exists x\in B\exists y\in C\exists z\in DA=⟨x,y,z⟩\to \exists x\in B\exists y\exists zA=⟨x,y,z⟩$$
9		rexex	$$⊢\exists x\in B\exists y\exists zA=⟨x,y,z⟩\to \exists x\exists y\exists zA=⟨x,y,z⟩$$
10	8 9	syl	$$⊢\exists x\in B\exists y\in C\exists z\in DA=⟨x,y,z⟩\to \exists x\exists y\exists zA=⟨x,y,z⟩$$
11	3 10	sylbi	$$⊢A\in \left(\left(B\times C\right)\times D\right)\to \exists x\exists y\exists zA=⟨x,y,z⟩$$
12	2 11	syl	$$⊢\left(A\in R\wedge R\subseteq \left(B\times C\right)\times D\right)\to \exists x\exists y\exists zA=⟨x,y,z⟩$$