This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )