Theorem fthres2

Description: A faithful functor into a restricted category is also a faithful functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Assertion	fthres2	⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) ⊆ ( 𝐶 Faith 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		relfth	⊢ Rel ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) )
2	1	a1i	⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → Rel ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) )
3		funcres2	⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) ⊆ ( 𝐶 Func 𝐷 ) )
4	3	ssbrd	⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 → 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) )
5	4	anim1d	⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( ( 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) → ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) ) )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7	6	isfth	⊢ ( 𝑓 ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ↔ ( 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) )
8	6	isfth	⊢ ( 𝑓 ( 𝐶 Faith 𝐷 ) 𝑔 ↔ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) )
9	5 7 8	3imtr4g	⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( 𝑓 ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) 𝑔 → 𝑓 ( 𝐶 Faith 𝐷 ) 𝑔 ) )
10		df-br	⊢ ( 𝑓 ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ↔ ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) )
11		df-br	⊢ ( 𝑓 ( 𝐶 Faith 𝐷 ) 𝑔 ↔ ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Faith 𝐷 ) )
12	9 10 11	3imtr3g	⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) → ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Faith 𝐷 ) ) )
13	2 12	relssdv	⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) ⊆ ( 𝐶 Faith 𝐷 ) )