Theorem idfucl 17945

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

Hypothesis

Ref	Expression
idfucl.i	⊢ 𝐼 = (idfunc‘𝐶)

Assertion

Ref	Expression
idfucl	⊢ (𝐶 ∈ Cat → 𝐼 ∈ (𝐶 Func 𝐶))

Proof of Theorem idfucl

Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		idfucl.i	. . . 4 ⊢ 𝐼 = (idfunc‘𝐶)
2		eqid 2740	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		id 22	. . . 4 ⊢ (𝐶 ∈ Cat → 𝐶 ∈ Cat)
4		eqid 2740	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
5	1, 2, 3, 4	idfuval 17940	. . 3 ⊢ (𝐶 ∈ Cat → 𝐼 = ⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩)
6	5	fveq2d 6924	. . . . 5 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) = (2nd ‘⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩))
7		fvex 6933	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
8		resiexg 7952	. . . . . . 7 ⊢ ((Base‘𝐶) ∈ V → ( I ↾ (Base‘𝐶)) ∈ V)
9	7, 8	ax-mp 5	. . . . . 6 ⊢ ( I ↾ (Base‘𝐶)) ∈ V
10	7, 7	xpex 7788	. . . . . . 7 ⊢ ((Base‘𝐶) × (Base‘𝐶)) ∈ V
11	10	mptex 7260	. . . . . 6 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))) ∈ V
12	9, 11	op2nd 8039	. . . . 5 ⊢ (2nd ‘⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩) = (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))
13	6, 12	eqtrdi 2796	. . . 4 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) = (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))))
14	13	opeq2d 4904	. . 3 ⊢ (𝐶 ∈ Cat → ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ = ⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩)
15	5, 14	eqtr4d 2783	. 2 ⊢ (𝐶 ∈ Cat → 𝐼 = ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩)
16		f1oi 6900	. . . . 5 ⊢ ( I ↾ (Base‘𝐶)):(Base‘𝐶)–1-1-onto→(Base‘𝐶)
17		f1of 6862	. . . . 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 6900	. . . . . . . . . 10 ⊢ ( I ↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)–1-1-onto→((Hom ‘𝐶)‘𝑧)
20		f1of 6862	. . . . . . . . . 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 6933	. . . . . . . . . 10 ⊢ ((Hom ‘𝐶)‘𝑧) ∈ V
23	22, 22	elmap 8929	. . . . . . . . 9 ⊢ (( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ ( I ↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)⟶((Hom ‘𝐶)‘𝑧))
24	21, 23	mpbir 231	. . . . . . . 8 ⊢ ( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧))
25		xp1st 8062	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st ‘𝑧) ∈ (Base‘𝐶))
26	25	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1st ‘𝑧) ∈ (Base‘𝐶))
27		fvresi 7207	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(1st ‘𝑧)) = (1st ‘𝑧))
28	26, 27	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾ (Base‘𝐶))‘(1st ‘𝑧)) = (1st ‘𝑧))
29		xp2nd 8063	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd ‘𝑧) ∈ (Base‘𝐶))
30	29	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2nd ‘𝑧) ∈ (Base‘𝐶))
31		fvresi 7207	. . . . . . . . . . . . 13 ⊢ ((2nd ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(2nd ‘𝑧)) = (2nd ‘𝑧))
32	30, 31	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾ (Base‘𝐶))‘(2nd ‘𝑧)) = (2nd ‘𝑧))
33	28, 32	oveq12d 7466	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))
34		df-ov 7451	. . . . . . . . . . 11 ⊢ ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
35	33, 34	eqtrdi 2796	. . . . . . . . . 10 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
36		1st2nd2 8069	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
37	36	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
38	37	fveq2d 6924	. . . . . . . . . 10 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
39	35, 38	eqtr4d 2783	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘𝑧))
40	39	oveq1d 7463	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) = (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)))
41	24, 40	eleqtrrid 2851	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
42	41	ralrimiva 3152	. . . . . 6 ⊢ (𝐶 ∈ Cat → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
43		mptelixpg 8993	. . . . . . 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 234	. . . . 5 ⊢ (𝐶 ∈ Cat → (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
46	13, 45	eqeltrd 2844	. . . 4 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
47		eqid 2740	. . . . . . . . 9 ⊢ (Id‘𝐶) = (Id‘𝐶)
48		simpl 482	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
49		simpr 484	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
50	2, 4, 47, 48, 49	catidcl 17740	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
51		fvresi 7207	. . . . . . . 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 17941	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(2nd ‘𝐼)𝑥) = ( I ↾ (𝑥(Hom ‘𝐶)𝑥)))
54	53	fveq1d 6922	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = (( I ↾ (𝑥(Hom ‘𝐶)𝑥))‘((Id‘𝐶)‘𝑥)))
55		fvresi 7207	. . . . . . . . 9 ⊢ (𝑥 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑥) = 𝑥)
56	55	adantl 481	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (( I ↾ (Base‘𝐶))‘𝑥) = 𝑥)
57	56	fveq2d 6924	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘(( I ↾ (Base‘𝐶))‘𝑥)) = ((Id‘𝐶)‘𝑥))
58	52, 54, 57	3eqtr4d 2790	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐶)‘(( I ↾ (Base‘𝐶))‘𝑥)))
59		eqid 2740	. . . . . . . . . . 11 ⊢ (comp‘𝐶) = (comp‘𝐶)
60	48	ad2antrr 725	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐶 ∈ Cat)
61	49	ad2antrr 725	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ (Base‘𝐶))
62		simplrl 776	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ (Base‘𝐶))
63		simplrr 777	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶))
64		simprl 770	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
65		simprr 772	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
66	2, 4, 59, 60, 61, 62, 63, 64, 65	catcocl 17743	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
67		fvresi 7207	. . . . . . . . . 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 17941	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐼)𝑧) = ( I ↾ (𝑥(Hom ‘𝐶)𝑧)))
70	69	fveq1d 6922	. . . . . . . . 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 7207	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑦) = 𝑦)
73	62, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑦) = 𝑦)
74	71, 73	opeq12d 4905	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩ = ⟨𝑥, 𝑦⟩)
75		fvresi 7207	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑧) = 𝑧)
76	63, 75	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑧) = 𝑧)
77	74, 76	oveq12d 7466	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧)) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧))
78	1, 2, 60, 4, 62, 63, 65	idfu2 17942	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐼)𝑧)‘𝑔) = 𝑔)
79	1, 2, 60, 4, 61, 62, 64	idfu2 17942	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑦)‘𝑓) = 𝑓)
80	77, 78, 79	oveq123d 7469	. . . . . . . . 9 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
81	68, 70, 80	3eqtr4d 2790	. . . . . . . 8 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
82	81	ralrimivva 3208	. . . . . . 7 ⊢ (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
83	82	ralrimivva 3208	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
84	58, 83	jca 511	. . . . 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 3152	. . . 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 17928	. . . 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 1342	. . 3 ⊢ (𝐶 ∈ Cat → ( I ↾ (Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼))
88		df-br 5167	. . 3 ⊢ (( I ↾ (Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼) ↔ ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ ∈ (𝐶 Func 𝐶))
89	87, 88	sylib 218	. 2 ⊢ (𝐶 ∈ Cat → ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ ∈ (𝐶 Func 𝐶))
90	15, 89	eqeltrd 2844	1 ⊢ (𝐶 ∈ Cat → 𝐼 ∈ (𝐶 Func 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067  Vcvv 3488  ⟨cop 4654   class class class wbr 5166   ↦ cmpt 5249   I cid 5592   × cxp 5698   ↾ cres 5702  ⟶wf 6569  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448  1^st c1st 8028  2^nd c2nd 8029   ↑_m cmap 8884  Xcixp 8955  Basecbs 17258  Hom chom 17322  compcco 17323  Catccat 17722  Idccid 17723   Func cfunc 17918  id_funccidfu 17919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-map 8886  df-ixp 8956  df-cat 17726  df-cid 17727  df-func 17922  df-idfu 17923

This theorem is referenced by:  cofulid  17954  cofurid  17955  idffth  18000  ressffth  18005  catccatid  18173  curf2ndf  18317