Theorem ffthoppf

Description: The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Zhi Wang, 26-Nov-2025)

	Ref	Expression
Hypotheses	fulloppf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	fulloppf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	ffthoppf.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) )
Assertion	ffthoppf	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( ( 𝑂 Full 𝑃 ) ∩ ( 𝑂 Faith 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fulloppf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		fulloppf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		ffthoppf.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) )
4	3	elin1d	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Full 𝐷 ) )
5	1 2 4	fulloppf	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Full 𝑃 ) )
6	3	elin2d	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Faith 𝐷 ) )
7	1 2 6	fthoppf	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Faith 𝑃 ) )
8	5 7	elind	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( ( 𝑂 Full 𝑃 ) ∩ ( 𝑂 Faith 𝑃 ) ) )