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→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )