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

Metamath Proof Explorer

Theorem ffthf1o

Description: The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses isfth.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isfth.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
isfth.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
ffthf1o.f ⊢ ( 𝜑 → 𝐹 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝐺 )
ffthf1o.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ffthf1o.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion ffthf1o ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 isfth.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isfth.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 isfth.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
4 ffthf1o.f ⊢ ( 𝜑 → 𝐹 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝐺 )
5 ffthf1o.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 ffthf1o.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 brin ⊢ ( 𝐹 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝐺 ↔ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ∧ 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ) )
8 4 7 sylib ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ∧ 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ) )
9 8 simprd ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
10 1 2 3 9 5 6 fthf1 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
11 8 simpld ⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
12 1 3 2 11 5 6 fullfo ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
13 df-f1o ⊢ ( ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∧ ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
14 10 12 13 sylanbrc ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )