Theorem idfucl 17143

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 2798	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		id 22	. . . 4 ⊢ (𝐶 ∈ Cat → 𝐶 ∈ Cat)
4		eqid 2798	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
5	1, 2, 3, 4	idfuval 17138	. . 3 ⊢ (𝐶 ∈ Cat → 𝐼 = ⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩)
6	5	fveq2d 6649	. . . . 5 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) = (2nd ‘⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩))
7		fvex 6658	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
8		resiexg 7601	. . . . . . 7 ⊢ ((Base‘𝐶) ∈ V → ( I ↾ (Base‘𝐶)) ∈ V)
9	7, 8	ax-mp 5	. . . . . 6 ⊢ ( I ↾ (Base‘𝐶)) ∈ V
10	7, 7	xpex 7456	. . . . . . 7 ⊢ ((Base‘𝐶) × (Base‘𝐶)) ∈ V
11	10	mptex 6963	. . . . . 6 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))) ∈ V
12	9, 11	op2nd 7680	. . . . 5 ⊢ (2nd ‘⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩) = (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))
13	6, 12	eqtrdi 2849	. . . 4 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) = (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))))
14	13	opeq2d 4772	. . 3 ⊢ (𝐶 ∈ Cat → ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ = ⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩)
15	5, 14	eqtr4d 2836	. 2 ⊢ (𝐶 ∈ Cat → 𝐼 = ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩)
16		f1oi 6627	. . . . 5 ⊢ ( I ↾ (Base‘𝐶)):(Base‘𝐶)–1-1-onto→(Base‘𝐶)
17		f1of 6590	. . . . 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 6627	. . . . . . . . . 10 ⊢ ( I ↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)–1-1-onto→((Hom ‘𝐶)‘𝑧)
20		f1of 6590	. . . . . . . . . 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 6658	. . . . . . . . . 10 ⊢ ((Hom ‘𝐶)‘𝑧) ∈ V
23	22, 22	elmap 8418	. . . . . . . . 9 ⊢ (( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ ( I ↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)⟶((Hom ‘𝐶)‘𝑧))
24	21, 23	mpbir 234	. . . . . . . 8 ⊢ ( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧))
25		xp1st 7703	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st ‘𝑧) ∈ (Base‘𝐶))
26	25	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1st ‘𝑧) ∈ (Base‘𝐶))
27		fvresi 6912	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(1st ‘𝑧)) = (1st ‘𝑧))
28	26, 27	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾ (Base‘𝐶))‘(1st ‘𝑧)) = (1st ‘𝑧))
29		xp2nd 7704	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd ‘𝑧) ∈ (Base‘𝐶))
30	29	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2nd ‘𝑧) ∈ (Base‘𝐶))
31		fvresi 6912	. . . . . . . . . . . . 13 ⊢ ((2nd ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(2nd ‘𝑧)) = (2nd ‘𝑧))
32	30, 31	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾ (Base‘𝐶))‘(2nd ‘𝑧)) = (2nd ‘𝑧))
33	28, 32	oveq12d 7153	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))
34		df-ov 7138	. . . . . . . . . . 11 ⊢ ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
35	33, 34	eqtrdi 2849	. . . . . . . . . 10 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
36		1st2nd2 7710	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
37	36	adantl 485	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
38	37	fveq2d 6649	. . . . . . . . . 10 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
39	35, 38	eqtr4d 2836	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘𝑧))
40	39	oveq1d 7150	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) = (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)))
41	24, 40	eleqtrrid 2897	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
42	41	ralrimiva 3149	. . . . . 6 ⊢ (𝐶 ∈ Cat → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
43		mptelixpg 8482	. . . . . . 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 237	. . . . 5 ⊢ (𝐶 ∈ Cat → (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
46	13, 45	eqeltrd 2890	. . . 4 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
47		eqid 2798	. . . . . . . . 9 ⊢ (Id‘𝐶) = (Id‘𝐶)
48		simpl 486	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
49		simpr 488	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
50	2, 4, 47, 48, 49	catidcl 16945	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
51		fvresi 6912	. . . . . . . 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 17139	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(2nd ‘𝐼)𝑥) = ( I ↾ (𝑥(Hom ‘𝐶)𝑥)))
54	53	fveq1d 6647	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = (( I ↾ (𝑥(Hom ‘𝐶)𝑥))‘((Id‘𝐶)‘𝑥)))
55		fvresi 6912	. . . . . . . . 9 ⊢ (𝑥 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑥) = 𝑥)
56	55	adantl 485	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (( I ↾ (Base‘𝐶))‘𝑥) = 𝑥)
57	56	fveq2d 6649	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘(( I ↾ (Base‘𝐶))‘𝑥)) = ((Id‘𝐶)‘𝑥))
58	52, 54, 57	3eqtr4d 2843	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐶)‘(( I ↾ (Base‘𝐶))‘𝑥)))
59		eqid 2798	. . . . . . . . . . 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 16948	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
67		fvresi 6912	. . . . . . . . . 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 17139	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐼)𝑧) = ( I ↾ (𝑥(Hom ‘𝐶)𝑧)))
70	69	fveq1d 6647	. . . . . . . . 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 6912	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑦) = 𝑦)
73	62, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑦) = 𝑦)
74	71, 73	opeq12d 4773	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩ = ⟨𝑥, 𝑦⟩)
75		fvresi 6912	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑧) = 𝑧)
76	63, 75	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑧) = 𝑧)
77	74, 76	oveq12d 7153	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧)) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧))
78	1, 2, 60, 4, 62, 63, 65	idfu2 17140	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐼)𝑧)‘𝑔) = 𝑔)
79	1, 2, 60, 4, 61, 62, 64	idfu2 17140	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑦)‘𝑓) = 𝑓)
80	77, 78, 79	oveq123d 7156	. . . . . . . . 9 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
81	68, 70, 80	3eqtr4d 2843	. . . . . . . 8 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
82	81	ralrimivva 3156	. . . . . . 7 ⊢ (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
83	82	ralrimivva 3156	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
84	58, 83	jca 515	. . . . 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 3149	. . . 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 17126	. . . 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 1339	. . 3 ⊢ (𝐶 ∈ Cat → ( I ↾ (Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼))
88		df-br 5031	. . 3 ⊢ (( I ↾ (Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼) ↔ ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ ∈ (𝐶 Func 𝐶))
89	87, 88	sylib 221	. 2 ⊢ (𝐶 ∈ Cat → ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ ∈ (𝐶 Func 𝐶))
90	15, 89	eqeltrd 2890	1 ⊢ (𝐶 ∈ Cat → 𝐼 ∈ (𝐶 Func 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3441  ⟨cop 4531   class class class wbr 5030   ↦ cmpt 5110   I cid 5424   × cxp 5517   ↾ cres 5521  ⟶wf 6320  –1-1-onto→wf1o 6323  ‘cfv 6324  (class class class)co 7135  1^st c1st 7669  2^nd c2nd 7670   ↑_m cmap 8389  Xcixp 8444  Basecbs 16475  Hom chom 16568  compcco 16569  Catccat 16927  Idccid 16928   Func cfunc 17116  id_funccidfu 17117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-map 8391  df-ixp 8445  df-cat 16931  df-cid 16932  df-func 17120  df-idfu 17121

This theorem is referenced by:  cofulid  17152  cofurid  17153  idffth  17195  ressffth  17200  catccatid  17354  curf2ndf  17489