oppf1

Description: Value of the object part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025)

		Ref	Expression
	Hypothesis	oppf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	Assertion	oppf1	⊢ ( 𝜑 → ( 1^st ‘ ( oppFunc ‘ 𝐹 ) ) = ( 1^st ‘ 𝐹 ) )

Step	Hyp	Ref	Expression
1		oppf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
2		oppfval2	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
3		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
4		fvex	⊢ ( 2^nd ‘ 𝐹 ) ∈ V
5	4	tposex	⊢ tpos ( 2^nd ‘ 𝐹 ) ∈ V
6	3 5	op1std	⊢ ( ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ → ( 1^st ‘ ( oppFunc ‘ 𝐹 ) ) = ( 1^st ‘ 𝐹 ) )
7	1 2 6	3syl	⊢ ( 𝜑 → ( 1^st ‘ ( oppFunc ‘ 𝐹 ) ) = ( 1^st ‘ 𝐹 ) )

Metamath Proof Explorer