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 ‘ 𝑋 ) = ( ℩ 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋 ⟩ · 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ) )