Metamath Proof Explorer

Theorem resssetc

Description: The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the SetCatU categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resssetc.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
resssetc.d ⊢ 𝐷 = ( SetCat ‘ 𝑉 )
resssetc.1 ⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
resssetc.2 ⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
Assertion resssetc ( 𝜑 → ( ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) ∧ ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 resssetc.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2 resssetc.d ⊢ 𝐷 = ( SetCat ‘ 𝑉 )
3 resssetc.1 ⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
4 resssetc.2 ⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
5 3 4 ssexd ⊢ ( 𝜑 → 𝑉 ∈ V )
6 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑉 ∈ V )
7 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
8 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ 𝑉 )
9 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑦 ∈ 𝑉 )
10 2 6 7 8 9 setchom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) = ( 𝑦 ↑m 𝑥 ) )
11 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑈 ∈ 𝑊 )
12 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
13 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑉 ⊆ 𝑈 )
14 13 8 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ 𝑈 )
15 13 9 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑦 ∈ 𝑈 )
16 1 11 12 14 15 setchom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ↑m 𝑥 ) )
17 eqid ⊢ ( 𝐶 ↾s 𝑉 ) = ( 𝐶 ↾s 𝑉 )
18 17 12 resshom ⊢ ( 𝑉 ∈ V → ( Hom ‘ 𝐶 ) = ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) )
19 5 18 syl ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) )
20 19 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑦 ) )
21 10 16 20 3eqtr2rd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
22 21 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
23 eqid ⊢ ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Hom ‘ ( 𝐶 ↾s 𝑉 ) )
24 1 3 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
25 4 24 sseqtrd ⊢ ( 𝜑 → 𝑉 ⊆ ( Base ‘ 𝐶 ) )
26 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
27 17 26 ressbas2 ⊢ ( 𝑉 ⊆ ( Base ‘ 𝐶 ) → 𝑉 = ( Base ‘ ( 𝐶 ↾s 𝑉 ) ) )
28 25 27 syl ⊢ ( 𝜑 → 𝑉 = ( Base ‘ ( 𝐶 ↾s 𝑉 ) ) )
29 2 5 setcbas ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝐷 ) )
30 23 7 28 29 homfeq ⊢ ( 𝜑 → ( ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
31 22 30 mpbird ⊢ ( 𝜑 → ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) )
32 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑉 ∈ V )
33 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
34 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑥 ∈ 𝑉 )
35 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑦 ∈ 𝑉 )
36 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑧 ∈ 𝑉 )
37 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
38 2 32 7 34 35 elsetchom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ↔ 𝑓 : 𝑥 ⟶ 𝑦 ) )
39 37 38 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑓 : 𝑥 ⟶ 𝑦 )
40 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
41 2 32 7 35 36 elsetchom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↔ 𝑔 : 𝑦 ⟶ 𝑧 ) )
42 40 41 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑔 : 𝑦 ⟶ 𝑧 )
43 2 32 33 34 35 36 39 42 setcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
44 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑈 ∈ 𝑊 )
45 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
46 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑉 ⊆ 𝑈 )
47 46 34 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑥 ∈ 𝑈 )
48 46 35 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑦 ∈ 𝑈 )
49 46 36 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑧 ∈ 𝑈 )
50 1 44 45 47 48 49 39 42 setcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
51 17 45 ressco ⊢ ( 𝑉 ∈ V → ( comp ‘ 𝐶 ) = ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) )
52 5 51 syl ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( comp ‘ 𝐶 ) = ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) )
54 53 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) )
55 54 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) )
56 43 50 55 3eqtr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) )
57 56 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) )
58 57 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ∀ 𝑧 ∈ 𝑉 ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) )
59 eqid ⊢ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) = ( comp ‘ ( 𝐶 ↾s 𝑉 ) )
60 31 eqcomd ⊢ ( 𝜑 → ( Homf ‘ 𝐷 ) = ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) )
61 33 59 7 29 28 60 comfeq ⊢ ( 𝜑 → ( ( compf ‘ 𝐷 ) = ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ∀ 𝑧 ∈ 𝑉 ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) ) )
62 58 61 mpbird ⊢ ( 𝜑 → ( compf ‘ 𝐷 ) = ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) )
63 62 eqcomd ⊢ ( 𝜑 → ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ 𝐷 ) )
64 31 63 jca ⊢ ( 𝜑 → ( ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) ∧ ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ 𝐷 ) ) )