Theorem elxpxpss

Description: Version of elrel for triple cross products. (Contributed by Scott Fenton, 21-Aug-2024)

	Ref	Expression
Assertion	elxpxpss	$$⊢\left(R\subseteq \left(B\times C\right)\times D\wedge A\in R\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		elxpxp	$$⊢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⟩$$
3		rexex	$$⊢\exists z\in DA=⟨⟨x,y⟩,z⟩\to \exists zA=⟨⟨x,y⟩,z⟩$$
4	3	reximi	$$⊢\exists y\in C\exists z\in DA=⟨⟨x,y⟩,z⟩\to \exists y\in C\exists zA=⟨⟨x,y⟩,z⟩$$
5		rexex	$$⊢\exists y\in C\exists zA=⟨⟨x,y⟩,z⟩\to \exists y\exists zA=⟨⟨x,y⟩,z⟩$$
6	4 5	syl	$$⊢\exists y\in C\exists z\in DA=⟨⟨x,y⟩,z⟩\to \exists y\exists zA=⟨⟨x,y⟩,z⟩$$
7	6	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⟩$$
8		rexex	$$⊢\exists x\in B\exists y\exists zA=⟨⟨x,y⟩,z⟩\to \exists x\exists y\exists zA=⟨⟨x,y⟩,z⟩$$
9	7 8	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⟩$$
10	2 9	sylbi	$$⊢A\in \left(\left(B\times C\right)\times D\right)\to \exists x\exists y\exists zA=⟨⟨x,y⟩,z⟩$$
11	1 10	syl	$$⊢\left(R\subseteq \left(B\times C\right)\times D\wedge A\in R\right)\to \exists x\exists y\exists zA=⟨⟨x,y⟩,z⟩$$