Metamath Proof Explorer

Theorem funfv1st2nd

Description: The function value for the first component of an ordered pair is the second component of the ordered pair. (Contributed by AV, 17-Oct-2023)

		Ref	Expression
	Assertion	funfv1st2nd	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝐹 ) → ( 𝐹 ‘ ( 1^st ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
2		1st2nd	⊢ ( ( Rel 𝐹 ∧ 𝑋 ∈ 𝐹 ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
3	1 2	sylan	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝐹 ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
4		eleq1	⊢ ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ → ( 𝑋 ∈ 𝐹 ↔ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝐹 ) )
5	4	adantl	⊢ ( ( Fun 𝐹 ∧ 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ) → ( 𝑋 ∈ 𝐹 ↔ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝐹 ) )
6		funopfv	⊢ ( Fun 𝐹 → ( ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝐹 → ( 𝐹 ‘ ( 1^st ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) ) )
7	6	adantr	⊢ ( ( Fun 𝐹 ∧ 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ) → ( ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝐹 → ( 𝐹 ‘ ( 1^st ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) ) )
8	5 7	sylbid	⊢ ( ( Fun 𝐹 ∧ 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ) → ( 𝑋 ∈ 𝐹 → ( 𝐹 ‘ ( 1^st ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) ) )
9	8	impancom	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝐹 ) → ( 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ → ( 𝐹 ‘ ( 1^st ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) ) )
10	3 9	mpd	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝐹 ) → ( 𝐹 ‘ ( 1^st ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) )