Metamath Proof Explorer

Theorem idfucl

Description: The identity functor is a functor. Example 3.20(1) of Adamek p. 30. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis idfucl.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
Assertion idfucl ( 𝐶 ∈ Cat → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )

Proof

Step Hyp Ref Expression
1 idfucl.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
2 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3 id ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
4 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
5 1 2 3 4 idfuval ⊢ ( 𝐶 ∈ Cat → 𝐼 = ⟨ ( I ↾ ( Base ‘ 𝐶 ) ) , ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ⟩ )
6 5 fveq2d ⊢ ( 𝐶 ∈ Cat → ( 2nd ‘ 𝐼 ) = ( 2nd ‘ ⟨ ( I ↾ ( Base ‘ 𝐶 ) ) , ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ⟩ ) )
7 fvex ⊢ ( Base ‘ 𝐶 ) ∈ V
8 resiexg ⊢ ( ( Base ‘ 𝐶 ) ∈ V → ( I ↾ ( Base ‘ 𝐶 ) ) ∈ V )
9 7 8 ax-mp ⊢ ( I ↾ ( Base ‘ 𝐶 ) ) ∈ V
10 7 7 xpex ⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ V
11 10 mptex ⊢ ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ∈ V
12 9 11 op2nd ⊢ ( 2nd ‘ ⟨ ( I ↾ ( Base ‘ 𝐶 ) ) , ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ⟩ ) = ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
13 6 12 eqtrdi ⊢ ( 𝐶 ∈ Cat → ( 2nd ‘ 𝐼 ) = ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) )
14 13 opeq2d ⊢ ( 𝐶 ∈ Cat → ⟨ ( I ↾ ( Base ‘ 𝐶 ) ) , ( 2nd ‘ 𝐼 ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐶 ) ) , ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ⟩ )
15 5 14 eqtr4d ⊢ ( 𝐶 ∈ Cat → 𝐼 = ⟨ ( I ↾ ( Base ‘ 𝐶 ) ) , ( 2nd ‘ 𝐼 ) ⟩ )
16 f1oi ⊢ ( I ↾ ( Base ‘ 𝐶 ) ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐶 )
17 f1of ⊢ ( ( I ↾ ( Base ‘ 𝐶 ) ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐶 ) → ( I ↾ ( Base ‘ 𝐶 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐶 ) )
18 16 17 mp1i ⊢ ( 𝐶 ∈ Cat → ( I ↾ ( Base ‘ 𝐶 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐶 ) )
19 f1oi ⊢ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) : ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) –1-1-onto→ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 )
20 f1of ⊢ ( ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) : ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) –1-1-onto→ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) → ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) : ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ⟶ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) )
21 19 20 ax-mp ⊢ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) : ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ⟶ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 )
22 fvex ⊢ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ∈ V
23 22 22 elmap ⊢ ( ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ∈ ( ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) : ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ⟶ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) )
24 21 23 mpbir ⊢ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ∈ ( ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) )
25 xp1st ⊢ ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → ( 1st ‘ 𝑧 ) ∈ ( Base ‘ 𝐶 ) )
26 25 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ 𝑧 ) ∈ ( Base ‘ 𝐶 ) )
27 fvresi ⊢ ( ( 1st ‘ 𝑧 ) ∈ ( Base ‘ 𝐶 ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ 𝑧 ) )
28 26 27 syl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) = ( 1st ‘ 𝑧 ) )
29 xp2nd ⊢ ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → ( 2nd ‘ 𝑧 ) ∈ ( Base ‘ 𝐶 ) )
30 29 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( 2nd ‘ 𝑧 ) ∈ ( Base ‘ 𝐶 ) )
31 fvresi ⊢ ( ( 2nd ‘ 𝑧 ) ∈ ( Base ‘ 𝐶 ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) = ( 2nd ‘ 𝑧 ) )
32 30 31 syl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) = ( 2nd ‘ 𝑧 ) )
33 28 32 oveq12d ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( 1st ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) )
34 df-ov ⊢ ( ( 1st ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 2nd ‘ 𝑧 ) ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
35 33 34 eqtrdi ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) )
36 1st2nd2 ⊢ ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
37 36 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
38 37 fveq2d ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) )
39 35 38 eqtr4d ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) )
40 39 oveq1d ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) = ( ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
41 24 40 eleqtrrid ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ∈ ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
42 41 ralrimiva ⊢ ( 𝐶 ∈ Cat → ∀ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ∈ ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
43 mptelixpg ⊢ ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ V → ( ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ∈ ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) )
44 10 43 ax-mp ⊢ ( ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ∈ ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
45 42 44 sylibr ⊢ ( 𝐶 ∈ Cat → ( 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
46 13 45 eqeltrd ⊢ ( 𝐶 ∈ Cat → ( 2nd ‘ 𝐼 ) ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
47 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
48 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
49 simpr ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
50 2 4 47 48 49 catidcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
51 fvresi ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) → ( ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
52 50 51 syl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
53 1 2 48 4 49 49 idfu2nd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑥 ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) )
54 53 fveq1d ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) )
55 fvresi ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) = 𝑥 )
56 55 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) = 𝑥 )
57 56 fveq2d ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
58 52 54 57 3eqtr4d ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) ) )
59 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
60 48 ad2antrr ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
61 49 ad2antrr ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
62 simplrl ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
63 simplrr ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
64 simprl ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
65 simprr ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
66 2 4 59 60 61 62 63 64 65 catcocl ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
67 fvresi ⊢ ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) → ( ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
68 66 67 syl ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
69 1 2 60 4 61 63 idfu2nd ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑧 ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ) )
70 69 fveq1d ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) )
71 61 55 syl ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) = 𝑥 )
72 fvresi ⊢ ( 𝑦 ∈ ( Base ‘ 𝐶 ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) = 𝑦 )
73 62 72 syl ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) = 𝑦 )
74 71 73 opeq12d ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ⟨ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) , ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
75 fvresi ⊢ ( 𝑧 ∈ ( Base ‘ 𝐶 ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) = 𝑧 )
76 63 75 syl ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) = 𝑧 )
77 74 76 oveq12d ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ⟨ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) , ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) )
78 1 2 60 4 62 63 65 idfu2 ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ 𝑔 ) = 𝑔 )
79 1 2 60 4 61 62 64 idfu2 ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) ‘ 𝑓 ) = 𝑓 )
80 77 78 79 oveq123d ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) , ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) ‘ 𝑓 ) ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
81 68 70 80 3eqtr4d ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) , ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) ‘ 𝑓 ) ) )
82 81 ralrimivva ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) , ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) ‘ 𝑓 ) ) )
83 82 ralrimivva ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) , ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) ‘ 𝑓 ) ) )
84 58 83 jca ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) , ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) ‘ 𝑓 ) ) ) )
85 84 ralrimiva ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) , ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) ‘ 𝑓 ) ) ) )
86 2 2 4 4 47 47 59 59 3 3 isfunc ⊢ ( 𝐶 ∈ Cat → ( ( I ↾ ( Base ‘ 𝐶 ) ) ( 𝐶 Func 𝐶 ) ( 2nd ‘ 𝐼 ) ↔ ( ( I ↾ ( Base ‘ 𝐶 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐶 ) ∧ ( 2nd ‘ 𝐼 ) ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝐼 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) , ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) ‘ 𝑓 ) ) ) ) ) )
87 18 46 85 86 mpbir3and ⊢ ( 𝐶 ∈ Cat → ( I ↾ ( Base ‘ 𝐶 ) ) ( 𝐶 Func 𝐶 ) ( 2nd ‘ 𝐼 ) )
88 df-br ⊢ ( ( I ↾ ( Base ‘ 𝐶 ) ) ( 𝐶 Func 𝐶 ) ( 2nd ‘ 𝐼 ) ↔ ⟨ ( I ↾ ( Base ‘ 𝐶 ) ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( 𝐶 Func 𝐶 ) )
89 87 88 sylib ⊢ ( 𝐶 ∈ Cat → ⟨ ( I ↾ ( Base ‘ 𝐶 ) ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( 𝐶 Func 𝐶 ) )
90 15 89 eqeltrd ⊢ ( 𝐶 ∈ Cat → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )