Theorem fthres2b

Description: Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	fthres2b.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	fthres2b.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	fthres2b.r	⊢ ( 𝜑 → 𝑅 ∈ ( Subcat ‘ 𝐷 ) )
	fthres2b.s	⊢ ( 𝜑 → 𝑅 Fn ( 𝑆 × 𝑆 ) )
	fthres2b.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	fthres2b.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝐺 𝑦 ) : 𝑌 ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ) )
Assertion	fthres2b	⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ 𝐹 ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		fthres2b.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
2		fthres2b.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		fthres2b.r	⊢ ( 𝜑 → 𝑅 ∈ ( Subcat ‘ 𝐷 ) )
4		fthres2b.s	⊢ ( 𝜑 → 𝑅 Fn ( 𝑆 × 𝑆 ) )
5		fthres2b.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
6		fthres2b.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝐺 𝑦 ) : 𝑌 ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ) )
7	1 2 3 4 5 6	funcres2b	⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ 𝐹 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝐺 ) )
8	7	anbi1d	⊢ ( 𝜑 → ( ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) ↔ ( 𝐹 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) ) )
9	1	isfth	⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
10	1	isfth	⊢ ( 𝐹 ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
11	8 9 10	3bitr4g	⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ 𝐹 ( 𝐶 Faith ( 𝐷 ↾cat 𝑅 ) ) 𝐺 ) )