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

Metamath Proof Explorer

Theorem isfth2

Description: Equivalent condition for a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses isfth.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isfth.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
isfth.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
Assertion isfth2 ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 isfth.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isfth.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 isfth.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
4 1 isfth ⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
5 simpll ⊢ ( ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
6 simplr ⊢ ( ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
7 simpr ⊢ ( ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
8 1 2 3 5 6 7 funcf2 ⊢ ( ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
9 df-f1 ⊢ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
10 9 baib ⊢ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
11 8 10 syl ⊢ ( ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
12 11 ralbidva ⊢ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
13 12 ralbidva ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
14 13 pm5.32i ⊢ ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
15 4 14 bitr4i ⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )