Theorem idfucl 17831

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 2733	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		id 22	. . . 4 ⊢ (𝐶 ∈ Cat → 𝐶 ∈ Cat)
4		eqid 2733	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
5	1, 2, 3, 4	idfuval 17826	. . 3 ⊢ (𝐶 ∈ Cat → 𝐼 = ⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩)
6	5	fveq2d 6896	. . . . 5 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) = (2nd ‘⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩))
7		fvex 6905	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
8		resiexg 7905	. . . . . . 7 ⊢ ((Base‘𝐶) ∈ V → ( I ↾ (Base‘𝐶)) ∈ V)
9	7, 8	ax-mp 5	. . . . . 6 ⊢ ( I ↾ (Base‘𝐶)) ∈ V
10	7, 7	xpex 7740	. . . . . . 7 ⊢ ((Base‘𝐶) × (Base‘𝐶)) ∈ V
11	10	mptex 7225	. . . . . 6 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))) ∈ V
12	9, 11	op2nd 7984	. . . . 5 ⊢ (2nd ‘⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩) = (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))
13	6, 12	eqtrdi 2789	. . . 4 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) = (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))))
14	13	opeq2d 4881	. . 3 ⊢ (𝐶 ∈ Cat → ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ = ⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩)
15	5, 14	eqtr4d 2776	. 2 ⊢ (𝐶 ∈ Cat → 𝐼 = ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩)
16		f1oi 6872	. . . . 5 ⊢ ( I ↾ (Base‘𝐶)):(Base‘𝐶)–1-1-onto→(Base‘𝐶)
17		f1of 6834	. . . . 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 6872	. . . . . . . . . 10 ⊢ ( I ↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)–1-1-onto→((Hom ‘𝐶)‘𝑧)
20		f1of 6834	. . . . . . . . . 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 6905	. . . . . . . . . 10 ⊢ ((Hom ‘𝐶)‘𝑧) ∈ V
23	22, 22	elmap 8865	. . . . . . . . 9 ⊢ (( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ ( I ↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)⟶((Hom ‘𝐶)‘𝑧))
24	21, 23	mpbir 230	. . . . . . . 8 ⊢ ( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧))
25		xp1st 8007	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st ‘𝑧) ∈ (Base‘𝐶))
26	25	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1st ‘𝑧) ∈ (Base‘𝐶))
27		fvresi 7171	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(1st ‘𝑧)) = (1st ‘𝑧))
28	26, 27	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾ (Base‘𝐶))‘(1st ‘𝑧)) = (1st ‘𝑧))
29		xp2nd 8008	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd ‘𝑧) ∈ (Base‘𝐶))
30	29	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2nd ‘𝑧) ∈ (Base‘𝐶))
31		fvresi 7171	. . . . . . . . . . . . 13 ⊢ ((2nd ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(2nd ‘𝑧)) = (2nd ‘𝑧))
32	30, 31	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾ (Base‘𝐶))‘(2nd ‘𝑧)) = (2nd ‘𝑧))
33	28, 32	oveq12d 7427	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))
34		df-ov 7412	. . . . . . . . . . 11 ⊢ ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
35	33, 34	eqtrdi 2789	. . . . . . . . . 10 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
36		1st2nd2 8014	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
37	36	adantl 483	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
38	37	fveq2d 6896	. . . . . . . . . 10 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
39	35, 38	eqtr4d 2776	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘𝑧))
40	39	oveq1d 7424	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) = (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)))
41	24, 40	eleqtrrid 2841	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
42	41	ralrimiva 3147	. . . . . 6 ⊢ (𝐶 ∈ Cat → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
43		mptelixpg 8929	. . . . . . 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 2834	. . . 4 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
47		eqid 2733	. . . . . . . . 9 ⊢ (Id‘𝐶) = (Id‘𝐶)
48		simpl 484	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
49		simpr 486	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
50	2, 4, 47, 48, 49	catidcl 17626	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
51		fvresi 7171	. . . . . . . 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 17827	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(2nd ‘𝐼)𝑥) = ( I ↾ (𝑥(Hom ‘𝐶)𝑥)))
54	53	fveq1d 6894	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = (( I ↾ (𝑥(Hom ‘𝐶)𝑥))‘((Id‘𝐶)‘𝑥)))
55		fvresi 7171	. . . . . . . . 9 ⊢ (𝑥 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑥) = 𝑥)
56	55	adantl 483	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (( I ↾ (Base‘𝐶))‘𝑥) = 𝑥)
57	56	fveq2d 6896	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘(( I ↾ (Base‘𝐶))‘𝑥)) = ((Id‘𝐶)‘𝑥))
58	52, 54, 57	3eqtr4d 2783	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐶)‘(( I ↾ (Base‘𝐶))‘𝑥)))
59		eqid 2733	. . . . . . . . . . 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 17629	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
67		fvresi 7171	. . . . . . . . . 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 17827	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐼)𝑧) = ( I ↾ (𝑥(Hom ‘𝐶)𝑧)))
70	69	fveq1d 6894	. . . . . . . . 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 7171	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑦) = 𝑦)
73	62, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑦) = 𝑦)
74	71, 73	opeq12d 4882	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩ = ⟨𝑥, 𝑦⟩)
75		fvresi 7171	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑧) = 𝑧)
76	63, 75	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑧) = 𝑧)
77	74, 76	oveq12d 7427	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧)) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧))
78	1, 2, 60, 4, 62, 63, 65	idfu2 17828	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐼)𝑧)‘𝑔) = 𝑔)
79	1, 2, 60, 4, 61, 62, 64	idfu2 17828	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑦)‘𝑓) = 𝑓)
80	77, 78, 79	oveq123d 7430	. . . . . . . . 9 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
81	68, 70, 80	3eqtr4d 2783	. . . . . . . 8 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
82	81	ralrimivva 3201	. . . . . . 7 ⊢ (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
83	82	ralrimivva 3201	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
84	58, 83	jca 513	. . . . 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 3147	. . . 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 17814	. . . 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 1343	. . 3 ⊢ (𝐶 ∈ Cat → ( I ↾ (Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼))
88		df-br 5150	. . 3 ⊢ (( I ↾ (Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼) ↔ ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ ∈ (𝐶 Func 𝐶))
89	87, 88	sylib 217	. 2 ⊢ (𝐶 ∈ Cat → ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ ∈ (𝐶 Func 𝐶))
90	15, 89	eqeltrd 2834	1 ⊢ (𝐶 ∈ Cat → 𝐼 ∈ (𝐶 Func 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  Vcvv 3475  ⟨cop 4635   class class class wbr 5149   ↦ cmpt 5232   I cid 5574   × cxp 5675   ↾ cres 5679  ⟶wf 6540  –1-1-onto→wf1o 6543  ‘cfv 6544  (class class class)co 7409  1^st c1st 7973  2^nd c2nd 7974   ↑_m cmap 8820  Xcixp 8891  Basecbs 17144  Hom chom 17208  compcco 17209  Catccat 17608  Idccid 17609   Func cfunc 17804  id_funccidfu 17805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-map 8822  df-ixp 8892  df-cat 17612  df-cid 17613  df-func 17808  df-idfu 17809

This theorem is referenced by:  cofulid  17840  cofurid  17841  idffth  17884  ressffth  17889  catccatid  18056  curf2ndf  18200