opf11

Description: The object part of the op functor on functor categories. Lemma for fucoppc . (Contributed by Zhi Wang, 18-Nov-2025)

Step	Hyp	Ref	Expression
1		opf11.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
2		opf11.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐷 ) )
3	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑋 ) )
4	2	fvresd	⊢ ( 𝜑 → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑋 ) = ( oppFunc ‘ 𝑋 ) )
5		oppfval2	⊢ ( 𝑋 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝑋 ) = ⟨ ( 1^st ‘ 𝑋 ) , tpos ( 2^nd ‘ 𝑋 ) ⟩ )
6	2 5	syl	⊢ ( 𝜑 → ( oppFunc ‘ 𝑋 ) = ⟨ ( 1^st ‘ 𝑋 ) , tpos ( 2^nd ‘ 𝑋 ) ⟩ )
7	3 4 6	3eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ⟨ ( 1^st ‘ 𝑋 ) , tpos ( 2^nd ‘ 𝑋 ) ⟩ )
8		fvex	⊢ ( 1^st ‘ 𝑋 ) ∈ V
9		fvex	⊢ ( 2^nd ‘ 𝑋 ) ∈ V
10	9	tposex	⊢ tpos ( 2^nd ‘ 𝑋 ) ∈ V
11	8 10	op1std	⊢ ( ( 𝐹 ‘ 𝑋 ) = ⟨ ( 1^st ‘ 𝑋 ) , tpos ( 2^nd ‘ 𝑋 ) ⟩ → ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 1^st ‘ 𝑋 ) )
12	7 11	syl	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 1^st ‘ 𝑋 ) )

Metamath Proof Explorer