Metamath Proof Explorer

Theorem fthoppc

Description: The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) in Adamek p. 39. (Contributed by Mario Carneiro, 27-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 fulloppc.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 fulloppc.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 fthoppc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
4 fthfunc ⊢ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
5 4 ssbri ⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
6 3 5 syl ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
7 1 2 6 funcoppc ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 )
8 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
11 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
12 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
14 8 9 10 11 12 13 fthf1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑦 𝐺 𝑥 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1→ ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) )
15 df-f1 ⊢ ( ( 𝑦 𝐺 𝑥 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1→ ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝑦 𝐺 𝑥 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ⟶ ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) ∧ Fun ◡ ( 𝑦 𝐺 𝑥 ) ) )
16 15 simprbi ⊢ ( ( 𝑦 𝐺 𝑥 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1→ ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) → Fun ◡ ( 𝑦 𝐺 𝑥 ) )
17 14 16 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → Fun ◡ ( 𝑦 𝐺 𝑥 ) )
18 ovtpos ⊢ ( 𝑥 tpos 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
19 18 cnveqi ⊢ ◡ ( 𝑥 tpos 𝐺 𝑦 ) = ◡ ( 𝑦 𝐺 𝑥 )
20 19 funeqi ⊢ ( Fun ◡ ( 𝑥 tpos 𝐺 𝑦 ) ↔ Fun ◡ ( 𝑦 𝐺 𝑥 ) )
21 17 20 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → Fun ◡ ( 𝑥 tpos 𝐺 𝑦 ) )
22 21 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑥 tpos 𝐺 𝑦 ) )
23 1 8 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
24 23 isfth ⊢ ( 𝐹 ( 𝑂 Faith 𝑃 ) tpos 𝐺 ↔ ( 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑥 tpos 𝐺 𝑦 ) ) )
25 7 22 24 sylanbrc ⊢ ( 𝜑 → 𝐹 ( 𝑂 Faith 𝑃 ) tpos 𝐺 )