Theorem thincfth

Description: A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	thincfth.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
	thincfth.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
Assertion	thincfth	⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		thincfth.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2		thincfth.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ ThinCat )
4		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
5		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8	3 4 5 6 7	thincmo	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
9		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
11	6 7 9 10 4 5	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
12		f1mo	⊢ ( ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
13	8 11 12	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
14	13	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
15	6 7 9	isfth2	⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) ) )
16	2 14 15	sylanbrc	⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )