fulloppf

Description: The opposite functor of a full functor is also full. Proposition 3.43(d) in Adamek p. 39. (Contributed by Zhi Wang, 26-Nov-2025)

	Ref	Expression
Hypotheses	fulloppf.o	$⊢ O = oppCat (C)$
	fulloppf.p	$⊢ P = oppCat (D)$
	fulloppf.f	$⊢ φ \to F \in (C Full D)$
Assertion	fulloppf	Could not format assertion : No typesetting found for \|- ( ph -> ( oppFunc ` F ) e. ( O Full P ) ) with typecode \|-

Step	Hyp	Ref	Expression
1		fulloppf.o	$⊢ O = oppCat (C)$
2		fulloppf.p	$⊢ P = oppCat (D)$
3		fulloppf.f	$⊢ φ \to F \in (C Full D)$
4		fullfunc	$⊢ C Full D \subseteq C Func D$
5	4	sseli	$⊢ F \in (C Full D) \to F \in (C Func D)$
6		oppfval2	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for \|- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-
7	3 5 6	3syl	Could not format ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for \|- ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-
8		relfull	$⊢ Rel (C Full D)$
9		1st2ndbr	$⊢ (Rel (C Full D) \land F \in (C Full D)) \to 1^{st} (F) (C Full D) 2^{nd} (F)$
10	8 3 9	sylancr	$⊢ φ \to 1^{st} (F) (C Full D) 2^{nd} (F)$
11	1 2 10	fulloppc	$⊢ φ \to 1^{st} (F) (O Full P) tpos 2^{nd} (F)$
12		df-br	$⊢ 1^{st} (F) (O Full P) tpos 2^{nd} (F) \leftrightarrow ⟨1^{st} (F), tpos 2^{nd} (F)⟩ \in (O Full P)$
13	11 12	sylib	$⊢ φ \to ⟨1^{st} (F), tpos 2^{nd} (F)⟩ \in (O Full P)$
14	7 13	eqeltrd	Could not format ( ph -> ( oppFunc ` F ) e. ( O Full P ) ) : No typesetting found for \|- ( ph -> ( oppFunc ` F ) e. ( O Full P ) ) with typecode \|-

Metamath Proof Explorer