Metamath Proof Explorer

Theorem ot1st2nd

Description: Reconstruction of a member of a nested Cartesian product in terms of its ordered triple components. (Contributed by BTernaryTau, 9-Oct-2026)

		Ref	Expression
	Assertion	ot1st2nd	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) → 𝐴 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ 𝐴 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
2		xp1st	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) → ( 1^st ‘ 𝐴 ) ∈ ( 𝐵 × 𝐶 ) )
3		1st2nd2	⊢ ( ( 1^st ‘ 𝐴 ) ∈ ( 𝐵 × 𝐶 ) → ( 1^st ‘ 𝐴 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) ⟩ )
4	2 3	syl	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) → ( 1^st ‘ 𝐴 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) ⟩ )
5	4	opeq1d	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) → ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) ⟩ , ( 2^nd ‘ 𝐴 ) ⟩ )
6	1 5	eqtrd	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) → 𝐴 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) ⟩ , ( 2^nd ‘ 𝐴 ) ⟩ )
7		df-ot	⊢ ⟨ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ 𝐴 ) ⟩ = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) ⟩ , ( 2^nd ‘ 𝐴 ) ⟩
8	6 7	eqtr4di	⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) → 𝐴 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) , ( 2^nd ‘ 𝐴 ) ⟩ )