Metamath Proof Explorer

Theorem fthoppf

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

		Ref	Expression
	Hypotheses	fulloppf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
		fulloppf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
		fthoppf.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Faith 𝐷 ) )
	Assertion	fthoppf	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Faith 𝑃 ) )

Proof

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