Step | Hyp | Ref
| Expression |
1 | | idfucl.i |
. . . 4
⊢ 𝐼 =
(idfunc‘𝐶) |
2 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
3 | | id 22 |
. . . 4
⊢ (𝐶 ∈ Cat → 𝐶 ∈ Cat) |
4 | | eqid 2738 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
5 | 1, 2, 3, 4 | idfuval 17591 |
. . 3
⊢ (𝐶 ∈ Cat → 𝐼 = 〈( I ↾
(Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom
‘𝐶)‘𝑧)))〉) |
6 | 5 | fveq2d 6778 |
. . . . 5
⊢ (𝐶 ∈ Cat →
(2nd ‘𝐼) =
(2nd ‘〈( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))〉)) |
7 | | fvex 6787 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
8 | | resiexg 7761 |
. . . . . . 7
⊢
((Base‘𝐶)
∈ V → ( I ↾ (Base‘𝐶)) ∈ V) |
9 | 7, 8 | ax-mp 5 |
. . . . . 6
⊢ ( I
↾ (Base‘𝐶))
∈ V |
10 | 7, 7 | xpex 7603 |
. . . . . . 7
⊢
((Base‘𝐶)
× (Base‘𝐶))
∈ V |
11 | 10 | mptex 7099 |
. . . . . 6
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom
‘𝐶)‘𝑧))) ∈ V |
12 | 9, 11 | op2nd 7840 |
. . . . 5
⊢
(2nd ‘〈( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))〉) = (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))) |
13 | 6, 12 | eqtrdi 2794 |
. . . 4
⊢ (𝐶 ∈ Cat →
(2nd ‘𝐼) =
(𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶)) ↦ ( I
↾ ((Hom ‘𝐶)‘𝑧)))) |
14 | 13 | opeq2d 4811 |
. . 3
⊢ (𝐶 ∈ Cat → 〈( I
↾ (Base‘𝐶)),
(2nd ‘𝐼)〉 = 〈( I ↾
(Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom
‘𝐶)‘𝑧)))〉) |
15 | 5, 14 | eqtr4d 2781 |
. 2
⊢ (𝐶 ∈ Cat → 𝐼 = 〈( I ↾
(Base‘𝐶)),
(2nd ‘𝐼)〉) |
16 | | f1oi 6754 |
. . . . 5
⊢ ( I
↾ (Base‘𝐶)):(Base‘𝐶)–1-1-onto→(Base‘𝐶) |
17 | | f1of 6716 |
. . . . 5
⊢ (( I
↾ (Base‘𝐶)):(Base‘𝐶)–1-1-onto→(Base‘𝐶) → ( I ↾ (Base‘𝐶)):(Base‘𝐶)⟶(Base‘𝐶)) |
18 | 16, 17 | mp1i 13 |
. . . 4
⊢ (𝐶 ∈ Cat → ( I ↾
(Base‘𝐶)):(Base‘𝐶)⟶(Base‘𝐶)) |
19 | | f1oi 6754 |
. . . . . . . . . 10
⊢ ( I
↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)–1-1-onto→((Hom
‘𝐶)‘𝑧) |
20 | | f1of 6716 |
. . . . . . . . . 10
⊢ (( I
↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)–1-1-onto→((Hom
‘𝐶)‘𝑧) → ( I ↾ ((Hom
‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)⟶((Hom ‘𝐶)‘𝑧)) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . 9
⊢ ( I
↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)⟶((Hom ‘𝐶)‘𝑧) |
22 | | fvex 6787 |
. . . . . . . . . 10
⊢ ((Hom
‘𝐶)‘𝑧) ∈ V |
23 | 22, 22 | elmap 8659 |
. . . . . . . . 9
⊢ (( I
↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ ( I ↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)⟶((Hom ‘𝐶)‘𝑧)) |
24 | 21, 23 | mpbir 230 |
. . . . . . . 8
⊢ ( I
↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)) |
25 | | xp1st 7863 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st
‘𝑧) ∈
(Base‘𝐶)) |
26 | 25 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1st
‘𝑧) ∈
(Base‘𝐶)) |
27 | | fvresi 7045 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(1st
‘𝑧)) =
(1st ‘𝑧)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾
(Base‘𝐶))‘(1st ‘𝑧)) = (1st
‘𝑧)) |
29 | | xp2nd 7864 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd
‘𝑧) ∈
(Base‘𝐶)) |
30 | 29 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2nd
‘𝑧) ∈
(Base‘𝐶)) |
31 | | fvresi 7045 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(2nd
‘𝑧)) =
(2nd ‘𝑧)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾
(Base‘𝐶))‘(2nd ‘𝑧)) = (2nd
‘𝑧)) |
33 | 28, 32 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾
(Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((1st
‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧))) |
34 | | df-ov 7278 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)) = ((Hom ‘𝐶)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
35 | 33, 34 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾
(Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉)) |
36 | | 1st2nd2 7870 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
37 | 36 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
38 | 37 | fveq2d 6778 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
39 | 35, 38 | eqtr4d 2781 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾
(Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘𝑧)) |
40 | 39 | oveq1d 7290 |
. . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (((( I ↾
(Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧)) = (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧))) |
41 | 24, 40 | eleqtrrid 2846 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾ ((Hom
‘𝐶)‘𝑧)) ∈ (((( I ↾
(Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧))) |
42 | 41 | ralrimiva 3103 |
. . . . . 6
⊢ (𝐶 ∈ Cat → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((( I ↾ (Base‘𝐶))‘(1st
‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧))) |
43 | | mptelixpg 8723 |
. . . . . . 7
⊢
(((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 5 |
. . . . . 6
⊢ ((𝑧 ∈ ((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 233 |
. . . . 5
⊢ (𝐶 ∈ Cat → (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom
‘𝐶)‘𝑧))) ∈ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))(((( I
↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐶)‘𝑧))) |
46 | 13, 45 | eqeltrd 2839 |
. . . 4
⊢ (𝐶 ∈ Cat →
(2nd ‘𝐼)
∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((( I ↾ (Base‘𝐶))‘(1st
‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧))) |
47 | | eqid 2738 |
. . . . . . . . 9
⊢
(Id‘𝐶) =
(Id‘𝐶) |
48 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat) |
49 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
50 | 2, 4, 47, 48, 49 | catidcl 17391 |
. . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥)) |
51 | | fvresi 7045 |
. . . . . . . 8
⊢
(((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥) → (( I ↾ (𝑥(Hom ‘𝐶)𝑥))‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐶)‘𝑥)) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (( I ↾ (𝑥(Hom ‘𝐶)𝑥))‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐶)‘𝑥)) |
53 | 1, 2, 48, 4, 49, 49 | idfu2nd 17592 |
. . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(2nd ‘𝐼)𝑥) = ( I ↾ (𝑥(Hom ‘𝐶)𝑥))) |
54 | 53 | fveq1d 6776 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = (( I ↾ (𝑥(Hom ‘𝐶)𝑥))‘((Id‘𝐶)‘𝑥))) |
55 | | fvresi 7045 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Base‘𝐶) → (( I ↾
(Base‘𝐶))‘𝑥) = 𝑥) |
56 | 55 | adantl 482 |
. . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (( I ↾
(Base‘𝐶))‘𝑥) = 𝑥) |
57 | 56 | fveq2d 6778 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘(( I ↾
(Base‘𝐶))‘𝑥)) = ((Id‘𝐶)‘𝑥)) |
58 | 52, 54, 57 | 3eqtr4d 2788 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐶)‘(( I ↾ (Base‘𝐶))‘𝑥))) |
59 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(comp‘𝐶) =
(comp‘𝐶) |
60 | 48 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐶 ∈ Cat) |
61 | 49 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ (Base‘𝐶)) |
62 | | simplrl 774 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ (Base‘𝐶)) |
63 | | simplrr 775 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶)) |
64 | | simprl 768 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
65 | | simprr 770 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) |
66 | 2, 4, 59, 60, 61, 62, 63, 64, 65 | catcocl 17394 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
67 | | fvresi 7045 |
. . . . . . . . . 10
⊢ ((𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (( I ↾ (𝑥(Hom ‘𝐶)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) |
68 | 66, 67 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (𝑥(Hom ‘𝐶)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) |
69 | 1, 2, 60, 4, 61, 63 | idfu2nd 17592 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐼)𝑧) = ( I ↾ (𝑥(Hom ‘𝐶)𝑧))) |
70 | 69 | fveq1d 6776 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (( I ↾ (𝑥(Hom ‘𝐶)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) |
71 | 61, 55 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑥) = 𝑥) |
72 | | fvresi 7045 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (Base‘𝐶) → (( I ↾
(Base‘𝐶))‘𝑦) = 𝑦) |
73 | 62, 72 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑦) = 𝑦) |
74 | 71, 73 | opeq12d 4812 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 〈(( I ↾
(Base‘𝐶))‘𝑥), (( I ↾
(Base‘𝐶))‘𝑦)〉 = 〈𝑥, 𝑦〉) |
75 | | fvresi 7045 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (Base‘𝐶) → (( I ↾
(Base‘𝐶))‘𝑧) = 𝑧) |
76 | 63, 75 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑧) = 𝑧) |
77 | 74, 76 | oveq12d 7293 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (〈(( I ↾
(Base‘𝐶))‘𝑥), (( I ↾
(Base‘𝐶))‘𝑦)〉(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧)) = (〈𝑥, 𝑦〉(comp‘𝐶)𝑧)) |
78 | 1, 2, 60, 4, 62, 63, 65 | idfu2 17593 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐼)𝑧)‘𝑔) = 𝑔) |
79 | 1, 2, 60, 4, 61, 62, 64 | idfu2 17593 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑦)‘𝑓) = 𝑓) |
80 | 77, 78, 79 | oveq123d 7296 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(〈(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)〉(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)) = (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) |
81 | 68, 70, 80 | 3eqtr4d 2788 |
. . . . . . . 8
⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(〈(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)〉(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓))) |
82 | 81 | ralrimivva 3123 |
. . . . . . 7
⊢ (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(〈(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)〉(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓))) |
83 | 82 | ralrimivva 3123 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(〈(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)〉(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓))) |
84 | 58, 83 | jca 512 |
. . . . 5
⊢ ((𝐶 ∈ 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 3103 |
. . . 4
⊢ (𝐶 ∈ 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 17579 |
. . . 4
⊢ (𝐶 ∈ 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 1341 |
. . 3
⊢ (𝐶 ∈ Cat → ( I ↾
(Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼)) |
88 | | df-br 5075 |
. . 3
⊢ (( I
↾ (Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼) ↔ 〈( I ↾ (Base‘𝐶)), (2nd ‘𝐼)〉 ∈ (𝐶 Func 𝐶)) |
89 | 87, 88 | sylib 217 |
. 2
⊢ (𝐶 ∈ Cat → 〈( I
↾ (Base‘𝐶)),
(2nd ‘𝐼)〉 ∈ (𝐶 Func 𝐶)) |
90 | 15, 89 | eqeltrd 2839 |
1
⊢ (𝐶 ∈ Cat → 𝐼 ∈ (𝐶 Func 𝐶)) |