Theorem ot1stg

Description: Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg , ot2ndg , ot3rdg .) (Contributed by NM, 3-Apr-2015) (Revised by Mario Carneiro, 2-May-2015)

	Ref	Expression
Assertion	ot1stg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 1st ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐴 )

Proof

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