Metamath Proof Explorer

Theorem catidd

Description: Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catidd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
catidd.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
catidd.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
catidd.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
catidd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 1 ∈ ( 𝑥 𝐻 𝑥 ) )
catidd.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ) ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 )
catidd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 )
Assertion catidd ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 1 ) )

Proof

Step Hyp Ref Expression
1 catidd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2 catidd.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3 catidd.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
4 catidd.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 catidd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 1 ∈ ( 𝑥 𝐻 𝑥 ) )
6 catidd.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ) ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 )
7 catidd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 )
8 6 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ) )
9 1 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝐶 ) ) )
10 1 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ 𝐶 ) ) )
11 2 oveqd ⊢ ( 𝜑 → ( 𝑦 𝐻 𝑥 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
12 11 eleq2d ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ↔ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) )
13 9 10 12 3anbi123d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ) )
14 3 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) = ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) )
15 14 oveqd ⊢ ( 𝜑 → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) )
16 15 eqeq1d ⊢ ( 𝜑 → ( ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ↔ ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ) )
17 8 13 16 3imtr3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ) )
18 17 3expd ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) → ( 𝑦 ∈ ( Base ‘ 𝐶 ) → ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ) ) ) )
19 18 imp41 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 )
20 19 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 )
21 7 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) )
22 2 oveqd ⊢ ( 𝜑 → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
23 22 eleq2d ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
24 9 10 23 3anbi123d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) )
25 3 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) = ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) )
26 25 oveqd ⊢ ( 𝜑 → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) )
27 26 eqeq1d ⊢ ( 𝜑 → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) )
28 21 24 27 3imtr3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) )
29 28 3expd ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) → ( 𝑦 ∈ ( Base ‘ 𝐶 ) → ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) ) ) )
30 29 imp41 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 )
31 30 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 )
32 20 31 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) )
33 32 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) )
34 5 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 1 ∈ ( 𝑥 𝐻 𝑥 ) ) )
35 2 oveqd ⊢ ( 𝜑 → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
36 35 eleq2d ⊢ ( 𝜑 → ( 1 ∈ ( 𝑥 𝐻 𝑥 ) ↔ 1 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) )
37 34 9 36 3imtr3d ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) → 1 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) )
38 37 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 1 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
39 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
40 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
41 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
42 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
43 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
44 39 40 41 42 43 catideu ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ∃! 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) )
45 oveq1 ⊢ ( 𝑔 = 1 → ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) )
46 45 eqeq1d ⊢ ( 𝑔 = 1 → ( ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ↔ ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ) )
47 46 ralbidv ⊢ ( 𝑔 = 1 → ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ) )
48 oveq2 ⊢ ( 𝑔 = 1 → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) )
49 48 eqeq1d ⊢ ( 𝑔 = 1 → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) )
50 49 ralbidv ⊢ ( 𝑔 = 1 → ( ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) )
51 47 50 anbi12d ⊢ ( 𝑔 = 1 → ( ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) ) )
52 51 ralbidv ⊢ ( 𝑔 = 1 → ( ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) ) )
53 52 riota2 ⊢ ( ( 1 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ ∃! 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) ↔ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) = 1 ) )
54 38 44 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 1 ) = 𝑓 ) ↔ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) = 1 ) )
55 33 54 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) = 1 )
56 55 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ 1 ) )
57 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
58 39 40 41 4 57 cidfval ⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
59 1 mpteq1d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 1 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ 1 ) )
60 56 58 59 3eqtr4d ⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 1 ) )