This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem el2xpss

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

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

Proof

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