Definition df-setc

Description: Definition of the category Set, relativized to a subset u . Example 3.3(1) of Adamek p. 22. This is the category of all sets in u and functions between these sets. Generally, we will take u 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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csetc	⊢ SetCat
1		vu	⊢ 𝑢
2		cvv	⊢ V
3		cbs	⊢ Base
4		cnx	⊢ ndx
5	4 3	cfv	⊢ ( Base ‘ ndx )
6	1	cv	⊢ 𝑢
7	5 6	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑢 ⟩
8		chom	⊢ Hom
9	4 8	cfv	⊢ ( Hom ‘ ndx )
10		vx	⊢ 𝑥
11		vy	⊢ 𝑦
12	11	cv	⊢ 𝑦
13		cmap	⊢ ↑m
14	10	cv	⊢ 𝑥
15	12 14 13	co	⊢ ( 𝑦 ↑m 𝑥 )
16	10 11 6 6 15	cmpo	⊢ ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) )
17	9 16	cop	⊢ ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) ) ⟩
18		cco	⊢ comp
19	4 18	cfv	⊢ ( comp ‘ ndx )
20		vv	⊢ 𝑣
21	6 6	cxp	⊢ ( 𝑢 × 𝑢 )
22		vz	⊢ 𝑧
23		vg	⊢ 𝑔
24	22	cv	⊢ 𝑧
25		c2nd	⊢ 2nd
26	20	cv	⊢ 𝑣
27	26 25	cfv	⊢ ( 2nd ‘ 𝑣 )
28	24 27 13	co	⊢ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) )
29		vf	⊢ 𝑓
30		c1st	⊢ 1st
31	26 30	cfv	⊢ ( 1st ‘ 𝑣 )
32	27 31 13	co	⊢ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) )
33	23	cv	⊢ 𝑔
34	29	cv	⊢ 𝑓
35	33 34	ccom	⊢ ( 𝑔 ∘ 𝑓 )
36	23 29 28 32 35	cmpo	⊢ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) )
37	20 22 21 6 36	cmpo	⊢ ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
38	19 37	cop	⊢ ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩
39	7 17 38	ctp	⊢ { ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ }
40	1 2 39	cmpt	⊢ ( 𝑢 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )
41	0 40	wceq	⊢ SetCat = ( 𝑢 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( 𝑦 ↑m 𝑥 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )