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

Metamath Proof Explorer

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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-ot	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩
2	1	fveq2i	⊢ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = ( 1^st ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ )
3		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
4		op1stg	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V ∧ 𝐶 ∈ 𝑋 ) → ( 1^st ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) = ⟨ 𝐴 , 𝐵 ⟩ )
5	3 4	mpan	⊢ ( 𝐶 ∈ 𝑋 → ( 1^st ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ) = ⟨ 𝐴 , 𝐵 ⟩ )
6	2 5	eqtrid	⊢ ( 𝐶 ∈ 𝑋 → ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = ⟨ 𝐴 , 𝐵 ⟩ )
7	6	fveq2d	⊢ ( 𝐶 ∈ 𝑋 → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
8		op2ndg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
9	7 8	sylan9eqr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐶 ∈ 𝑋 ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐵 )
10	9	3impa	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐵 )