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	$$⊢A\in \left(\left(B\times C\right)\times D\right)\to A=⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right),2^{nd}\left(A\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	$$⊢A\in \left(\left(B\times C\right)\times D\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
2		xp1st	$$⊢A\in \left(\left(B\times C\right)\times D\right)\to 1^{st}\left(A\right)\in \left(B\times C\right)$$
3		1st2nd2	$$⊢1^{st}\left(A\right)\in \left(B\times C\right)\to 1^{st}\left(A\right)=⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩$$
4	2 3	syl	$$⊢A\in \left(\left(B\times C\right)\times D\right)\to 1^{st}\left(A\right)=⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩$$
5	4	opeq1d	$$⊢A\in \left(\left(B\times C\right)\times D\right)\to ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$
6	1 5	eqtrd	$$⊢A\in \left(\left(B\times C\right)\times D\right)\to A=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$
7		df-ot	$$⊢⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right),2^{nd}\left(A\right)⟩=⟨⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right)⟩,2^{nd}\left(A\right)⟩$$
8	6 7	eqtr4di	$$⊢A\in \left(\left(B\times C\right)\times D\right)\to A=⟨1^{st}\left(1^{st}\left(A\right)\right),2^{nd}\left(1^{st}\left(A\right)\right),2^{nd}\left(A\right)⟩$$