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 2819	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		id 22	. . . 4 ⊢ (𝐶 ∈ Cat → 𝐶 ∈ Cat)
4		eqid 2819	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
5	1, 2, 3, 4	idfuval 17138	. . 3 ⊢ (𝐶 ∈ Cat → 𝐼 = ⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩)
6	5	fveq2d 6667	. . . . 5 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) = (2nd ‘⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩))
7		fvex 6676	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
8		resiexg 7611	. . . . . . 7 ⊢ ((Base‘𝐶) ∈ V → ( I ↾ (Base‘𝐶)) ∈ V)
9	7, 8	ax-mp 5	. . . . . 6 ⊢ ( I ↾ (Base‘𝐶)) ∈ V
10	7, 7	xpex 7468	. . . . . . 7 ⊢ ((Base‘𝐶) × (Base‘𝐶)) ∈ V
11	10	mptex 6978	. . . . . 6 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))) ∈ V
12	9, 11	op2nd 7690	. . . . 5 ⊢ (2nd ‘⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩) = (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))
13	6, 12	syl6eq 2870	. . . 4 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) = (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))))
14	13	opeq2d 4802	. . 3 ⊢ (𝐶 ∈ Cat → ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ = ⟨( I ↾ (Base‘𝐶)), (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧)))⟩)
15	5, 14	eqtr4d 2857	. 2 ⊢ (𝐶 ∈ Cat → 𝐼 = ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩)
16		f1oi 6645	. . . . 5 ⊢ ( I ↾ (Base‘𝐶)):(Base‘𝐶)–1-1-onto→(Base‘𝐶)
17		f1of 6608	. . . . 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 6645	. . . . . . . . . 10 ⊢ ( I ↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)–1-1-onto→((Hom ‘𝐶)‘𝑧)
20		f1of 6608	. . . . . . . . . 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 6676	. . . . . . . . . 10 ⊢ ((Hom ‘𝐶)‘𝑧) ∈ V
23	22, 22	elmap 8427	. . . . . . . . 9 ⊢ (( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ ( I ↾ ((Hom ‘𝐶)‘𝑧)):((Hom ‘𝐶)‘𝑧)⟶((Hom ‘𝐶)‘𝑧))
24	21, 23	mpbir 233	. . . . . . . 8 ⊢ ( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧))
25		xp1st 7713	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st ‘𝑧) ∈ (Base‘𝐶))
26	25	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1st ‘𝑧) ∈ (Base‘𝐶))
27		fvresi 6928	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(1st ‘𝑧)) = (1st ‘𝑧))
28	26, 27	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾ (Base‘𝐶))‘(1st ‘𝑧)) = (1st ‘𝑧))
29		xp2nd 7714	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd ‘𝑧) ∈ (Base‘𝐶))
30	29	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2nd ‘𝑧) ∈ (Base‘𝐶))
31		fvresi 6928	. . . . . . . . . . . . 13 ⊢ ((2nd ‘𝑧) ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘(2nd ‘𝑧)) = (2nd ‘𝑧))
32	30, 31	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (( I ↾ (Base‘𝐶))‘(2nd ‘𝑧)) = (2nd ‘𝑧))
33	28, 32	oveq12d 7166	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))
34		df-ov 7151	. . . . . . . . . . 11 ⊢ ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
35	33, 34	syl6eq 2870	. . . . . . . . . 10 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
36		1st2nd2 7720	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
37	36	adantl 484	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
38	37	fveq2d 6667	. . . . . . . . . 10 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
39	35, 38	eqtr4d 2857	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) = ((Hom ‘𝐶)‘𝑧))
40	39	oveq1d 7163	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) = (((Hom ‘𝐶)‘𝑧) ↑m ((Hom ‘𝐶)‘𝑧)))
41	24, 40	eleqtrrid 2918	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
42	41	ralrimiva 3180	. . . . . 6 ⊢ (𝐶 ∈ Cat → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))( I ↾ ((Hom ‘𝐶)‘𝑧)) ∈ (((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
43		mptelixpg 8491	. . . . . . 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 236	. . . . 5 ⊢ (𝐶 ∈ Cat → (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ ( I ↾ ((Hom ‘𝐶)‘𝑧))) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
46	13, 45	eqeltrd 2911	. . . 4 ⊢ (𝐶 ∈ Cat → (2nd ‘𝐼) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((( I ↾ (Base‘𝐶))‘(1st ‘𝑧))(Hom ‘𝐶)(( I ↾ (Base‘𝐶))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
47		eqid 2819	. . . . . . . . 9 ⊢ (Id‘𝐶) = (Id‘𝐶)
48		simpl 485	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
49		simpr 487	. . . . . . . . 9 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
50	2, 4, 47, 48, 49	catidcl 16945	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
51		fvresi 6928	. . . . . . . 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 6665	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = (( I ↾ (𝑥(Hom ‘𝐶)𝑥))‘((Id‘𝐶)‘𝑥)))
55		fvresi 6928	. . . . . . . . 9 ⊢ (𝑥 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑥) = 𝑥)
56	55	adantl 484	. . . . . . . 8 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (( I ↾ (Base‘𝐶))‘𝑥) = 𝑥)
57	56	fveq2d 6667	. . . . . . 7 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘(( I ↾ (Base‘𝐶))‘𝑥)) = ((Id‘𝐶)‘𝑥))
58	52, 54, 57	3eqtr4d 2864	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐼)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐶)‘(( I ↾ (Base‘𝐶))‘𝑥)))
59		eqid 2819	. . . . . . . . . . 11 ⊢ (comp‘𝐶) = (comp‘𝐶)
60	48	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐶 ∈ Cat)
61	49	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ (Base‘𝐶))
62		simplrl 775	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ (Base‘𝐶))
63		simplrr 776	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶))
64		simprl 769	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
65		simprr 771	. . . . . . . . . . 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 6928	. . . . . . . . . 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 6665	. . . . . . . . 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 6928	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑦) = 𝑦)
73	62, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑦) = 𝑦)
74	71, 73	opeq12d 4803	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩ = ⟨𝑥, 𝑦⟩)
75		fvresi 6928	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (Base‘𝐶) → (( I ↾ (Base‘𝐶))‘𝑧) = 𝑧)
76	63, 75	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (( I ↾ (Base‘𝐶))‘𝑧) = 𝑧)
77	74, 76	oveq12d 7166	. . . . . . . . . 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 7169	. . . . . . . . 9 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
81	68, 70, 80	3eqtr4d 2864	. . . . . . . 8 ⊢ ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
82	81	ralrimivva 3189	. . . . . . 7 ⊢ (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
83	82	ralrimivva 3189	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘𝐼)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐼)𝑧)‘𝑔)(⟨(( I ↾ (Base‘𝐶))‘𝑥), (( I ↾ (Base‘𝐶))‘𝑦)⟩(comp‘𝐶)(( I ↾ (Base‘𝐶))‘𝑧))((𝑥(2nd ‘𝐼)𝑦)‘𝑓)))
84	58, 83	jca 514	. . . . 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 3180	. . . 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 1337	. . 3 ⊢ (𝐶 ∈ Cat → ( I ↾ (Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼))
88		df-br 5058	. . 3 ⊢ (( I ↾ (Base‘𝐶))(𝐶 Func 𝐶)(2nd ‘𝐼) ↔ ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ ∈ (𝐶 Func 𝐶))
89	87, 88	sylib 220	. 2 ⊢ (𝐶 ∈ Cat → ⟨( I ↾ (Base‘𝐶)), (2nd ‘𝐼)⟩ ∈ (𝐶 Func 𝐶))
90	15, 89	eqeltrd 2911	1 ⊢ (𝐶 ∈ Cat → 𝐼 ∈ (𝐶 Func 𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1531   ∈ wcel 2108  ∀wral 3136  Vcvv 3493  ⟨cop 4565   class class class wbr 5057   ↦ cmpt 5137   I cid 5452   × cxp 5546   ↾ cres 5550  ⟶wf 6344  –1-1-onto→wf1o 6347  ‘cfv 6348  (class class class)co 7148  1^st c1st 7679  2^nd c2nd 7680   ↑_m cmap 8398  Xcixp 8453  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 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-1st 7681  df-2nd 7682  df-map 8400  df-ixp 8454  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