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	|- O = ( oppCat ` C )
	fulloppf.p	|- P = ( oppCat ` D )
	ffthoppf.f	|- ( ph -> F e. ( ( C Full D ) i^i ( C Faith D ) ) )
Assertion	ffthoppf	|- ( ph -> ( oppFunc ` F ) e. ( ( O Full P ) i^i ( O Faith P ) ) )

Proof

Step	Hyp	Ref	Expression
1		fulloppf.o	|- O = ( oppCat ` C )
2		fulloppf.p	|- P = ( oppCat ` D )
3		ffthoppf.f	|- ( ph -> F e. ( ( C Full D ) i^i ( C Faith D ) ) )
4	3	elin1d	|- ( ph -> F e. ( C Full D ) )
5	1 2 4	fulloppf	|- ( ph -> ( oppFunc ` F ) e. ( O Full P ) )
6	3	elin2d	|- ( ph -> F e. ( C Faith D ) )
7	1 2 6	fthoppf	|- ( ph -> ( oppFunc ` F ) e. ( O Faith P ) )
8	5 7	elind	|- ( ph -> ( oppFunc ` F ) e. ( ( O Full P ) i^i ( O Faith P ) ) )