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 𝐶 ) )