Theorem ffthoppc

Description: The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	fulloppc.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	fulloppc.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	ffthoppc.f	⊢ ( 𝜑 → 𝐹 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝐺 )
Assertion	ffthoppc	⊢ ( 𝜑 → 𝐹 ( ( 𝑂 Full 𝑃 ) ∩ ( 𝑂 Faith 𝑃 ) ) tpos 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		fulloppc.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		fulloppc.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		ffthoppc.f	⊢ ( 𝜑 → 𝐹 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝐺 )
4		brin	⊢ ( 𝐹 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝐺 ↔ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ∧ 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ) )
5	3 4	sylib	⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ∧ 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ) )
6	5	simpld	⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
7	1 2 6	fulloppc	⊢ ( 𝜑 → 𝐹 ( 𝑂 Full 𝑃 ) tpos 𝐺 )
8	5	simprd	⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
9	1 2 8	fthoppc	⊢ ( 𝜑 → 𝐹 ( 𝑂 Faith 𝑃 ) tpos 𝐺 )
10		brin	⊢ ( 𝐹 ( ( 𝑂 Full 𝑃 ) ∩ ( 𝑂 Faith 𝑃 ) ) tpos 𝐺 ↔ ( 𝐹 ( 𝑂 Full 𝑃 ) tpos 𝐺 ∧ 𝐹 ( 𝑂 Faith 𝑃 ) tpos 𝐺 ) )
11	7 9 10	sylanbrc	⊢ ( 𝜑 → 𝐹 ( ( 𝑂 Full 𝑃 ) ∩ ( 𝑂 Faith 𝑃 ) ) tpos 𝐺 )