Metamath Proof Explorer

Theorem funcres2

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

Ref Expression
Assertion funcres2 ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) ⊆ ( 𝐶 Func 𝐷 ) )

Proof

Step Hyp Ref Expression
1 relfunc ⊢ Rel ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) )
2 1 a1i ⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → Rel ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) )
3 simpr ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6 simpl ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → 𝑅 ∈ ( Subcat ‘ 𝐷 ) )
7 eqidd ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → dom dom 𝑅 = dom dom 𝑅 )
8 6 7 subcfn ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → 𝑅 Fn ( dom dom 𝑅 × dom dom 𝑅 ) )
9 eqid ⊢ ( Base ‘ ( 𝐷 ↾cat 𝑅 ) ) = ( Base ‘ ( 𝐷 ↾cat 𝑅 ) )
10 4 9 3 funcf1 ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → 𝑓 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ ( 𝐷 ↾cat 𝑅 ) ) )
11 eqid ⊢ ( 𝐷 ↾cat 𝑅 ) = ( 𝐷 ↾cat 𝑅 )
12 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
13 subcrcl ⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → 𝐷 ∈ Cat )
14 13 adantr ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → 𝐷 ∈ Cat )
15 6 8 12 subcss1 ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → dom dom 𝑅 ⊆ ( Base ‘ 𝐷 ) )
16 11 12 14 8 15 rescbas ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → dom dom 𝑅 = ( Base ‘ ( 𝐷 ↾cat 𝑅 ) ) )
17 16 feq3d ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → ( 𝑓 : ( Base ‘ 𝐶 ) ⟶ dom dom 𝑅 ↔ 𝑓 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ ( 𝐷 ↾cat 𝑅 ) ) ) )
18 10 17 mpbird ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → 𝑓 : ( Base ‘ 𝐶 ) ⟶ dom dom 𝑅 )
19 eqid ⊢ ( Hom ‘ ( 𝐷 ↾cat 𝑅 ) ) = ( Hom ‘ ( 𝐷 ↾cat 𝑅 ) )
20 simplr ⊢ ( ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 )
21 simprl ⊢ ( ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
22 simprr ⊢ ( ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
23 4 5 19 20 21 22 funcf2 ⊢ ( ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ↾cat 𝑅 ) ) ( 𝑓 ‘ 𝑦 ) ) )
24 11 12 14 8 15 reschom ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → 𝑅 = ( Hom ‘ ( 𝐷 ↾cat 𝑅 ) ) )
25 24 adantr ⊢ ( ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑅 = ( Hom ‘ ( 𝐷 ↾cat 𝑅 ) ) )
26 25 oveqd ⊢ ( ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ↾cat 𝑅 ) ) ( 𝑓 ‘ 𝑦 ) ) )
27 26 feq3d ⊢ ( ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ↾cat 𝑅 ) ) ( 𝑓 ‘ 𝑦 ) ) ) )
28 23 27 mpbird ⊢ ( ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑓 ‘ 𝑦 ) ) )
29 4 5 6 8 18 28 funcres2b ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ↔ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) )
30 3 29 mpbird ⊢ ( ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) ∧ 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ) → 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 )
31 30 ex ⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 → 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) )
32 df-br ⊢ ( 𝑓 ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) 𝑔 ↔ ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) )
33 df-br ⊢ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ↔ ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
34 31 32 33 3imtr3g ⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) → ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Func 𝐷 ) ) )
35 2 34 relssdv ⊢ ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → ( 𝐶 Func ( 𝐷 ↾cat 𝑅 ) ) ⊆ ( 𝐶 Func 𝐷 ) )