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=\mathrm{oppCat}\left(C\right)$$
	fulloppf.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	ffthoppf.f	$$⊢\phi \to F\in \left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)$$
Assertion	ffthoppf	Could not format assertion : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( ( O Full P ) i^i ( O Faith P ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fulloppf.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		fulloppf.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		ffthoppf.f	$$⊢\phi \to F\in \left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)$$
4	3	elin1d	$$⊢\phi \to F\in \left(C\mathrm{Full}D\right)$$
5	1 2 4	fulloppf	Could not format ( ph -> ( oppFunc ` F ) e. ( O Full P ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( O Full P ) ) with typecode |-
6	3	elin2d	$$⊢\phi \to F\in \left(C\mathrm{Faith}D\right)$$
7	1 2 6	fthoppf	Could not format ( ph -> ( oppFunc ` F ) e. ( O Faith P ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( O Faith P ) ) with typecode |-
8	5 7	elind	Could not format ( ph -> ( oppFunc ` F ) e. ( ( O Full P ) i^i ( O Faith P ) ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( ( O Full P ) i^i ( O Faith P ) ) ) with typecode |-