Theorem elxpxpss

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

	Ref	Expression
Assertion	elxpxpss	⊢ ( ( 𝑅 ⊆ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ∧ 𝐴 ∈ 𝑅 ) → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		ssel2	⊢ ( ( 𝑅 ⊆ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ∧ 𝐴 ∈ 𝑅 ) → 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) )
2		elxpxp	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
3		rexex	⊢ ( ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
4	3	reximi	⊢ ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
5		rexex	⊢ ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
6	4 5	syl	⊢ ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
7	6	reximi	⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
8		rexex	⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
9	7 8	syl	⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
10	2 9	sylbi	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
11	1 10	syl	⊢ ( ( 𝑅 ⊆ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ∧ 𝐴 ∈ 𝑅 ) → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )