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

Metamath Proof Explorer

Theorem el2xptp

Description: A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018)

Ref Expression
Assertion el2xptp ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )

Proof

Step Hyp Ref Expression
1 elxp2 ⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑝 ∈ ( 𝐵 × 𝐶 ) ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ )
2 opeq1 ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 𝑝 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
3 2 eqeq2d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
4 3 rexbidv ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
5 4 rexxp ⊢ ( ∃ 𝑝 ∈ ( 𝐵 × 𝐶 ) ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
6 df-ot ⊢ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩
7 6 eqcomi ⊢ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩
8 7 eqeq2i ⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
9 8 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
10 9 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
11 10 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
12 1 5 11 3bitri ⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )