Metamath Proof Explorer

Theorem oteqimp

Description: The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018)

		Ref	Expression
	Assertion	oteqimp	⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) = 𝐴 ∧ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) = 𝐵 ∧ ( 2^nd ‘ 𝑇 ) = 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ot1stg	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐴 )
2		ot2ndg	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐵 )
3		ot3rdg	⊢ ( 𝐶 ∈ 𝑍 → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = 𝐶 )
4	3	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = 𝐶 )
5	1 2 4	3jca	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐴 ∧ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐵 ∧ ( 2^nd ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = 𝐶 ) )
6		2fveq3	⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) )
7	6	eqeq1d	⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) = 𝐴 ↔ ( 1^st ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐴 ) )
8		2fveq3	⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) )
9	8	eqeq1d	⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) = 𝐵 ↔ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐵 ) )
10		fveqeq2	⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( 2^nd ‘ 𝑇 ) = 𝐶 ↔ ( 2^nd ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = 𝐶 ) )
11	7 9 10	3anbi123d	⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) = 𝐴 ∧ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) = 𝐵 ∧ ( 2^nd ‘ 𝑇 ) = 𝐶 ) ↔ ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐴 ∧ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ) = 𝐵 ∧ ( 2^nd ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = 𝐶 ) ) )
12	5 11	imbitrrid	⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑇 ) ) = 𝐴 ∧ ( 2^nd ‘ ( 1^st ‘ 𝑇 ) ) = 𝐵 ∧ ( 2^nd ‘ 𝑇 ) = 𝐶 ) ) )