Theorem 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	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	fulloppf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	fulloppf.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Full 𝐷 ) )
Assertion	fulloppf	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Full 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		fulloppf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		fulloppf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		fulloppf.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Full 𝐷 ) )
4		fullfunc	⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
5	4	sseli	⊢ ( 𝐹 ∈ ( 𝐶 Full 𝐷 ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
6		oppfval2	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1st ‘ 𝐹 ) , tpos ( 2nd ‘ 𝐹 ) ⟩ )
7	3 5 6	3syl	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1st ‘ 𝐹 ) , tpos ( 2nd ‘ 𝐹 ) ⟩ )
8		relfull	⊢ Rel ( 𝐶 Full 𝐷 )
9		1st2ndbr	⊢ ( ( Rel ( 𝐶 Full 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Full 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Full 𝐷 ) ( 2nd ‘ 𝐹 ) )
10	8 3 9	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Full 𝐷 ) ( 2nd ‘ 𝐹 ) )
11	1 2 10	fulloppc	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝑂 Full 𝑃 ) tpos ( 2nd ‘ 𝐹 ) )
12		df-br	⊢ ( ( 1st ‘ 𝐹 ) ( 𝑂 Full 𝑃 ) tpos ( 2nd ‘ 𝐹 ) ↔ ⟨ ( 1st ‘ 𝐹 ) , tpos ( 2nd ‘ 𝐹 ) ⟩ ∈ ( 𝑂 Full 𝑃 ) )
13	11 12	sylib	⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝐹 ) , tpos ( 2nd ‘ 𝐹 ) ⟩ ∈ ( 𝑂 Full 𝑃 ) )
14	7 13	eqeltrd	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Full 𝑃 ) )