Theorem ot2ndg

Description: Extract the second member of an ordered triple. (See ot1stg comment.) (Contributed by NM, 3-Apr-2015) (Revised by Mario Carneiro, 2-May-2015)

	Ref	Expression
Assertion	ot2ndg	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to 2^{nd}\left(1^{st}\left(⟨A,B,C⟩\right)\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		df-ot	$$⊢⟨A,B,C⟩=⟨⟨A,B⟩,C⟩$$
2	1	fveq2i	$$⊢1^{st}\left(⟨A,B,C⟩\right)=1^{st}\left(⟨⟨A,B⟩,C⟩\right)$$
3		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
4		op1stg	$$⊢\left(⟨A,B⟩\in \mathrm{V}\wedge C\in X\right)\to 1^{st}\left(⟨⟨A,B⟩,C⟩\right)=⟨A,B⟩$$
5	3 4	mpan	$$⊢C\in X\to 1^{st}\left(⟨⟨A,B⟩,C⟩\right)=⟨A,B⟩$$
6	2 5	syl5eq	$$⊢C\in X\to 1^{st}\left(⟨A,B,C⟩\right)=⟨A,B⟩$$
7	6	fveq2d	$$⊢C\in X\to 2^{nd}\left(1^{st}\left(⟨A,B,C⟩\right)\right)=2^{nd}\left(⟨A,B⟩\right)$$
8		op2ndg	$$⊢\left(A\in V\wedge B\in W\right)\to 2^{nd}\left(⟨A,B⟩\right)=B$$
9	7 8	sylan9eqr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge C\in X\right)\to 2^{nd}\left(1^{st}\left(⟨A,B,C⟩\right)\right)=B$$
10	9	3impa	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to 2^{nd}\left(1^{st}\left(⟨A,B,C⟩\right)\right)=B$$