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

Metamath Proof Explorer

Definition df-cid

Description: Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion df-cid Id = ( 𝑐 ∈ Cat ↦ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccid ⊢ Id
1 vc ⊢ 𝑐
2 ccat ⊢ Cat
3 cbs ⊢ Base
4 1 cv ⊢ 𝑐
5 4 3 cfv ⊢ ( Base ‘ 𝑐 )
6 vb ⊢ 𝑏
7 chom ⊢ Hom
8 4 7 cfv ⊢ ( Hom ‘ 𝑐 )
9 vh ⊢ ℎ
10 cco ⊢ comp
11 4 10 cfv ⊢ ( comp ‘ 𝑐 )
12 vo ⊢ 𝑜
13 vx ⊢ 𝑥
14 6 cv ⊢ 𝑏
15 vg ⊢ 𝑔
16 13 cv ⊢ 𝑥
17 9 cv ⊢ ℎ
18 16 16 17 co ⊢ ( 𝑥 ℎ 𝑥 )
19 vy ⊢ 𝑦
20 vf ⊢ 𝑓
21 19 cv ⊢ 𝑦
22 21 16 17 co ⊢ ( 𝑦 ℎ 𝑥 )
23 15 cv ⊢ 𝑔
24 21 16 cop ⊢ ⟨ 𝑦 , 𝑥 ⟩
25 12 cv ⊢ 𝑜
26 24 16 25 co ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 )
27 20 cv ⊢ 𝑓
28 23 27 26 co ⊢ ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 )
29 28 27 wceq ⊢ ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓
30 29 20 22 wral ⊢ ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓
31 16 21 17 co ⊢ ( 𝑥 ℎ 𝑦 )
32 16 16 cop ⊢ ⟨ 𝑥 , 𝑥 ⟩
33 32 21 25 co ⊢ ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 )
34 27 23 33 co ⊢ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 )
35 34 27 wceq ⊢ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓
36 35 20 31 wral ⊢ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓
37 30 36 wa ⊢ ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 )
38 37 19 14 wral ⊢ ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 )
39 38 15 18 crio ⊢ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) )
40 13 14 39 cmpt ⊢ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) )
41 12 11 40 csb ⊢ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) )
42 9 8 41 csb ⊢ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) )
43 6 5 42 csb ⊢ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) )
44 1 2 43 cmpt ⊢ ( 𝑐 ∈ Cat ↦ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
45 0 44 wceq ⊢ Id = ( 𝑐 ∈ Cat ↦ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )