Definition df-setc 17707

Description: Definition of the category Set, relativized to a subset 𝑢. Example 3.3(1) of [Adamek] p. 22. This is the category of all sets in 𝑢 and functions between these sets. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.)

Assertion

Ref	Expression
df-setc	⊢ SetCat = (𝑢 ∈ V ↦ {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})

Distinct variable group:   𝑓,𝑔,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-setc

Step	Hyp	Ref	Expression
1		csetc 17706	. 2 class SetCat
2		vu	. . 3 setvar 𝑢
3		cvv 3422	. . 3 class V
4		cnx 16822	. . . . . 6 class ndx
5		cbs 16840	. . . . . 6 class Base
6	4, 5	cfv 6418	. . . . 5 class (Base‘ndx)
7	2	cv 1538	. . . . 5 class 𝑢
8	6, 7	cop 4564	. . . 4 class ⟨(Base‘ndx), 𝑢⟩
9		chom 16899	. . . . . 6 class Hom
10	4, 9	cfv 6418	. . . . 5 class (Hom ‘ndx)
11		vx	. . . . . 6 setvar 𝑥
12		vy	. . . . . 6 setvar 𝑦
13	12	cv 1538	. . . . . . 7 class 𝑦
14	11	cv 1538	. . . . . . 7 class 𝑥
15		cmap 8573	. . . . . . 7 class ↑m
16	13, 14, 15	co 7255	. . . . . 6 class (𝑦 ↑m 𝑥)
17	11, 12, 7, 7, 16	cmpo 7257	. . . . 5 class (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))
18	10, 17	cop 4564	. . . 4 class ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))⟩
19		cco 16900	. . . . . 6 class comp
20	4, 19	cfv 6418	. . . . 5 class (comp‘ndx)
21		vv	. . . . . 6 setvar 𝑣
22		vz	. . . . . 6 setvar 𝑧
23	7, 7	cxp 5578	. . . . . 6 class (𝑢 × 𝑢)
24		vg	. . . . . . 7 setvar 𝑔
25		vf	. . . . . . 7 setvar 𝑓
26	22	cv 1538	. . . . . . . 8 class 𝑧
27	21	cv 1538	. . . . . . . . 9 class 𝑣
28		c2nd 7803	. . . . . . . . 9 class 2nd
29	27, 28	cfv 6418	. . . . . . . 8 class (2nd ‘𝑣)
30	26, 29, 15	co 7255	. . . . . . 7 class (𝑧 ↑m (2nd ‘𝑣))
31		c1st 7802	. . . . . . . . 9 class 1st
32	27, 31	cfv 6418	. . . . . . . 8 class (1st ‘𝑣)
33	29, 32, 15	co 7255	. . . . . . 7 class ((2nd ‘𝑣) ↑m (1st ‘𝑣))
34	24	cv 1538	. . . . . . . 8 class 𝑔
35	25	cv 1538	. . . . . . . 8 class 𝑓
36	34, 35	ccom 5584	. . . . . . 7 class (𝑔 ∘ 𝑓)
37	24, 25, 30, 33, 36	cmpo 7257	. . . . . 6 class (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓))
38	21, 22, 23, 7, 37	cmpo 7257	. . . . 5 class (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))
39	20, 38	cop 4564	. . . 4 class ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩
40	8, 18, 39	ctp 4562	. . 3 class {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩}
41	2, 3, 40	cmpt 5153	. 2 class (𝑢 ∈ V ↦ {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})
42	1, 41	wceq 1539	1 wff SetCat = (𝑢 ∈ V ↦ {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ (𝑦 ↑m 𝑥))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ (𝑧 ↑m (2nd ‘𝑣)), 𝑓 ∈ ((2nd ‘𝑣) ↑m (1st ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))⟩})

This definition is referenced by:  setcval  17708