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 ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )