Theorem fthf1

Description: The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		isfth.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		isfth.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		isfth.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
4		fthf1.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
5		fthf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		fthf1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7	1 2 3	isfth2	⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
8	7	simprbi	⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
9	4 8	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑌 ∈ 𝐵 )
11		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
12		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
13	11 12	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝐺 𝑦 ) = ( 𝑋 𝐺 𝑌 ) )
14	11 12	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
15	11	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
16	12	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
17	15 16	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
18	13 14 17	f1eq123d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
19	10 18	rspcdv	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
20	5 19	rspcimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
21	9 20	mpd	⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )