Metamath Proof Explorer

Theorem oppfdiag1a

Description: A constant functor for opposite categories is the opposite functor of the constant functor for original categories. (Contributed by Zhi Wang, 19-Nov-2025)

		Ref	Expression
	Hypotheses	oppfdiag.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
		oppfdiag.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
		oppfdiag.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
		oppfdiag.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
		oppfdiag.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
		oppfdiag1a.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
		oppfdiag1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	Assertion	oppfdiag1a	⊢ ( 𝜑 → ( oppFunc ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) = ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		oppfdiag.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppfdiag.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		oppfdiag.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
4		oppfdiag.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		oppfdiag.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
6		oppfdiag1a.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
7		oppfdiag1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
9	3 4 5 6 7 8	diag1cl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) )
10	9	fvresd	⊢ ( 𝜑 → ( ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) = ( oppFunc ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
11		eqidd	⊢ ( 𝜑 → ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) = ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) )
12	1 2 3 4 5 11 6 7	oppfdiag1	⊢ ( 𝜑 → ( ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) = ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) )
13	10 12	eqtr3d	⊢ ( 𝜑 → ( oppFunc ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) = ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) )