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	$⊢ φ \to F \in ((C Full D) \cap (C Faith D))$
Assertion	ffthoppf	Could not format assertion : No typesetting found for \|- ( ph -> ( oppFunc ` F ) e. ( ( O Full P ) i^i ( O Faith P ) ) ) with typecode \|-

Step	Hyp	Ref	Expression
1		fulloppf.o	$⊢ O = oppCat (C)$
2		fulloppf.p	$⊢ P = oppCat (D)$
3		ffthoppf.f	$⊢ φ \to F \in ((C Full D) \cap (C Faith D))$
4	3	elin1d	$⊢ φ \to F \in (C Full D)$
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	$⊢ φ \to F \in (C Faith D)$
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 \|-

Metamath Proof Explorer