# Metamath Proof Explorer

## Theorem cidval

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

Ref Expression
Hypotheses cidfval.b 𝐵 = ( Base ‘ 𝐶 )
cidfval.h 𝐻 = ( Hom ‘ 𝐶 )
cidfval.o · = ( comp ‘ 𝐶 )
cidfval.c ( 𝜑𝐶 ∈ Cat )
cidfval.i 1 = ( Id ‘ 𝐶 )
cidval.x ( 𝜑𝑋𝐵 )
Assertion cidval ( 𝜑 → ( 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 cidval.x ( 𝜑𝑋𝐵 )
7 1 2 3 4 5 cidfval ( 𝜑1 = ( 𝑥𝐵 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
8 simpr ( ( 𝜑𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
9 8 8 oveq12d ( ( 𝜑𝑥 = 𝑋 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑋 𝐻 𝑋 ) )
10 8 oveq2d ( ( 𝜑𝑥 = 𝑋 ) → ( 𝑦 𝐻 𝑥 ) = ( 𝑦 𝐻 𝑋 ) )
11 8 opeq2d ( ( 𝜑𝑥 = 𝑋 ) → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑦 , 𝑋 ⟩ )
12 11 8 oveq12d ( ( 𝜑𝑥 = 𝑋 ) → ( ⟨ 𝑦 , 𝑥· 𝑥 ) = ( ⟨ 𝑦 , 𝑋· 𝑋 ) )
13 12 oveqd ( ( 𝜑𝑥 = 𝑋 ) → ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) )
14 13 eqeq1d ( ( 𝜑𝑥 = 𝑋 ) → ( ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ↔ ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ) )
15 10 14 raleqbidv ( ( 𝜑𝑥 = 𝑋 ) → ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ) )
16 8 oveq1d ( ( 𝜑𝑥 = 𝑋 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑦 ) )
17 8 8 opeq12d ( ( 𝜑𝑥 = 𝑋 ) → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑋 , 𝑋 ⟩ )
18 17 oveq1d ( ( 𝜑𝑥 = 𝑋 ) → ( ⟨ 𝑥 , 𝑥· 𝑦 ) = ( ⟨ 𝑋 , 𝑋· 𝑦 ) )
19 18 oveqd ( ( 𝜑𝑥 = 𝑋 ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) )
20 19 eqeq1d ( ( 𝜑𝑥 = 𝑋 ) → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) )
21 16 20 raleqbidv ( ( 𝜑𝑥 = 𝑋 ) → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) )
22 15 21 anbi12d ( ( 𝜑𝑥 = 𝑋 ) → ( ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) )
23 22 ralbidv ( ( 𝜑𝑥 = 𝑋 ) → ( ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) )
24 9 23 riotaeqbidv ( ( 𝜑𝑥 = 𝑋 ) → ( 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥· 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥· 𝑦 ) 𝑔 ) = 𝑓 ) ) = ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) )
25 riotaex ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) ∈ V
26 25 a1i ( 𝜑 → ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) ∈ V )
27 7 24 6 26 fvmptd ( 𝜑 → ( 1𝑋 ) = ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) )