This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐺 )