# Metamath Proof Explorer

## Theorem cidfval

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses cidfval.b 𝐵 = ( Base ‘ 𝐶 )
cidfval.h 𝐻 = ( Hom ‘ 𝐶 )
cidfval.o · = ( comp ‘ 𝐶 )
cidfval.c ( 𝜑𝐶 ∈ Cat )
cidfval.i 1 = ( Id ‘ 𝐶 )
Assertion cidfval ( 𝜑1 = ( 𝑥𝐵 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )

### Proof

Step Hyp Ref Expression
1 cidfval.b 𝐵 = ( Base ‘ 𝐶 )
2 cidfval.h 𝐻 = ( Hom ‘ 𝐶 )
3 cidfval.o · = ( comp ‘ 𝐶 )
4 cidfval.c ( 𝜑𝐶 ∈ Cat )
5 cidfval.i 1 = ( Id ‘ 𝐶 )
6 fvexd ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) ∈ V )
7 fveq2 ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
8 7 1 eqtr4di ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
9 fvexd ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) ∈ V )
10 simpl ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → 𝑐 = 𝐶 )
11 10 fveq2d ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
12 11 2 eqtr4di ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = 𝐻 )
13 fvexd ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( comp ‘ 𝑐 ) ∈ V )
14 simpll ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → 𝑐 = 𝐶 )
15 14 fveq2d ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
16 15 3 eqtr4di ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( comp ‘ 𝑐 ) = · )
17 simpllr ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → 𝑏 = 𝐵 )
18 simplr ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → = 𝐻 )
19 18 oveqd ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑥 𝑥 ) = ( 𝑥 𝐻 𝑥 ) )
20 18 oveqd ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑦 𝑥 ) = ( 𝑦 𝐻 𝑥 ) )
21 simpr ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → 𝑜 = · )
22 21 oveqd ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) = ( ⟨ 𝑦 , 𝑥· 𝑥 ) )
23 22 oveqd ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) )
24 23 eqeq1d ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ↔ ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ) )
25 20 24 raleqbidv ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ) )
26 18 oveqd ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑥 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
27 21 oveqd ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) = ( ⟨ 𝑥 , 𝑥· 𝑦 ) )
28 27 oveqd ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) )
29 28 eqeq1d ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) )
30 26 29 raleqbidv ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) )
31 25 30 anbi12d ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) )
32 17 31 raleqbidv ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) )
33 19 32 riotaeqbidv ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) = ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) )
34 17 33 mpteq12dv ( ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) = ( 𝑥𝐵 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
35 13 16 34 csbied2 ( ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) ∧ = 𝐻 ) → ( comp ‘ 𝑐 ) / 𝑜 ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) = ( 𝑥𝐵 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
36 9 12 35 csbied2 ( ( 𝑐 = 𝐶𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) / ( comp ‘ 𝑐 ) / 𝑜 ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) = ( 𝑥𝐵 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
37 6 8 36 csbied2 ( 𝑐 = 𝐶 ( Base ‘ 𝑐 ) / 𝑏 ( Hom ‘ 𝑐 ) / ( comp ‘ 𝑐 ) / 𝑜 ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) = ( 𝑥𝐵 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
38 df-cid Id = ( 𝑐 ∈ Cat ↦ ( Base ‘ 𝑐 ) / 𝑏 ( Hom ‘ 𝑐 ) / ( comp ‘ 𝑐 ) / 𝑜 ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
39 37 38 1 mptfvmpt ( 𝐶 ∈ Cat → ( Id ‘ 𝐶 ) = ( 𝑥𝐵 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
40 4 39 syl ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥𝐵 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
41 5 40 syl5eq ( 𝜑1 = ( 𝑥𝐵 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )