This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐷 ) )