Metamath Proof Explorer

Theorem funcsetcres2

Description: A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses resssetc.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
resssetc.d ⊢ 𝐷 = ( SetCat ‘ 𝑉 )
resssetc.1 ⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
resssetc.2 ⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
Assertion funcsetcres2 ( 𝜑 → ( 𝐸 Func 𝐷 ) ⊆ ( 𝐸 Func 𝐶 ) )

Proof

Step Hyp Ref Expression
1 resssetc.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2 resssetc.d ⊢ 𝐷 = ( SetCat ‘ 𝑉 )
3 resssetc.1 ⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
4 resssetc.2 ⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
5 eqidd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( Homf ‘ 𝐸 ) = ( Homf ‘ 𝐸 ) )
6 eqidd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( compf ‘ 𝐸 ) = ( compf ‘ 𝐸 ) )
7 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
9 1 setccat ⊢ ( 𝑈 ∈ 𝑊 → 𝐶 ∈ Cat )
10 3 9 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → 𝐶 ∈ Cat )
12 1 3 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
13 4 12 sseqtrd ⊢ ( 𝜑 → 𝑉 ⊆ ( Base ‘ 𝐶 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → 𝑉 ⊆ ( Base ‘ 𝐶 ) )
15 eqid ⊢ ( 𝐶 ↾s 𝑉 ) = ( 𝐶 ↾s 𝑉 )
16 eqid ⊢ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) )
17 7 8 11 14 15 16 fullresc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ∧ ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ) )
18 17 simpld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) )
19 1 2 3 4 resssetc ⊢ ( 𝜑 → ( ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) ∧ ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ 𝐷 ) ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) ∧ ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ 𝐷 ) ) )
21 20 simpld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) )
22 18 21 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( Homf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) = ( Homf ‘ 𝐷 ) )
23 17 simprd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) )
24 20 simprd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ 𝐷 ) )
25 23 24 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( compf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) = ( compf ‘ 𝐷 ) )
26 funcrcl ⊢ ( 𝑓 ∈ ( 𝐸 Func 𝐷 ) → ( 𝐸 ∈ Cat ∧ 𝐷 ∈ Cat ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( 𝐸 ∈ Cat ∧ 𝐷 ∈ Cat ) )
28 27 simpld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → 𝐸 ∈ Cat )
29 7 8 11 14 fullsubc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( Subcat ‘ 𝐶 ) )
30 16 29 subccat ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ∈ Cat )
31 27 simprd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → 𝐷 ∈ Cat )
32 5 6 22 25 28 28 30 31 funcpropd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( 𝐸 Func ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) = ( 𝐸 Func 𝐷 ) )
33 funcres2 ⊢ ( ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( Subcat ‘ 𝐶 ) → ( 𝐸 Func ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ⊆ ( 𝐸 Func 𝐶 ) )
34 29 33 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( 𝐸 Func ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ⊆ ( 𝐸 Func 𝐶 ) )
35 32 34 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → ( 𝐸 Func 𝐷 ) ⊆ ( 𝐸 Func 𝐶 ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → 𝑓 ∈ ( 𝐸 Func 𝐷 ) )
37 35 36 sseldd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐸 Func 𝐷 ) ) → 𝑓 ∈ ( 𝐸 Func 𝐶 ) )
38 37 ex ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐸 Func 𝐷 ) → 𝑓 ∈ ( 𝐸 Func 𝐶 ) ) )
39 38 ssrdv ⊢ ( 𝜑 → ( 𝐸 Func 𝐷 ) ⊆ ( 𝐸 Func 𝐶 ) )