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	$⊢ (A \in V \land B \in W \land C \in X) \to 2^{nd} (1^{st} (⟨A, B, C⟩)) = B$

Proof

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