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