Theorem catlid 17740

Description: Left identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
catidcl.b	⊢ 𝐵 = (Base‘𝐶)
catidcl.h	⊢ 𝐻 = (Hom ‘𝐶)
catidcl.i	⊢ 1 = (Id‘𝐶)
catidcl.c	⊢ (𝜑 → 𝐶 ∈ Cat)
catidcl.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
catlid.o	⊢ · = (comp‘𝐶)
catlid.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
catlid.f	⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))

Assertion

Ref	Expression
catlid	⊢ (𝜑 → (( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝐹) = 𝐹)

Proof of Theorem catlid

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

Step	Hyp	Ref	Expression
1		oveq2 7420	. . 3 ⊢ (𝑓 = 𝐹 → (( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝑓) = (( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝐹))
2		id 23	. . 3 ⊢ (𝑓 = 𝐹 → 𝑓 = 𝐹)
3	1, 2	eqeq12d 2779	. 2 ⊢ (𝑓 = 𝐹 → ((( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ↔ (( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝐹) = 𝐹))
4		oveq1 7419	. . . 4 ⊢ (𝑥 = 𝑋 → (𝑥𝐻𝑌) = (𝑋𝐻𝑌))
5		opeq1 4839	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ⟨𝑥, 𝑌⟩ = ⟨𝑋, 𝑌⟩)
6	5	oveq1d 7427	. . . . . 6 ⊢ (𝑥 = 𝑋 → (⟨𝑥, 𝑌⟩ · 𝑌) = (⟨𝑋, 𝑌⟩ · 𝑌))
7	6	oveqd 7429	. . . . 5 ⊢ (𝑥 = 𝑋 → (( 1 ‘𝑌)(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = (( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝑓))
8	7	eqeq1d 2765	. . . 4 ⊢ (𝑥 = 𝑋 → ((( 1 ‘𝑌)(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ↔ (( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝑓) = 𝑓))
9	4, 8	raleqbidv 3338	. . 3 ⊢ (𝑥 = 𝑋 → (∀𝑓 ∈ (𝑥𝐻𝑌)(( 1 ‘𝑌)(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑋𝐻𝑌)(( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝑓) = 𝑓))
10		simpl 487	. . . . . . . 8 ⊢ ((∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓) → ∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓)
11	10	ralimi 3102	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓) → ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓)
12	11	a1i 11	. . . . . 6 ⊢ (𝑔 ∈ (𝑌𝐻𝑌) → (∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓) → ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓))
13	12	ss2rabi 4031	. . . . 5 ⊢ {𝑔 ∈ (𝑌𝐻𝑌) ∣ ∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓)} ⊆ {𝑔 ∈ (𝑌𝐻𝑌) ∣ ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓}
14		catidcl.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐶)
15		catidcl.h	. . . . . . 7 ⊢ 𝐻 = (Hom ‘𝐶)
16		catlid.o	. . . . . . 7 ⊢ · = (comp‘𝐶)
17		catidcl.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ Cat)
18		catidcl.i	. . . . . . 7 ⊢ 1 = (Id‘𝐶)
19		catlid.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
20	14, 15, 16, 17, 18, 19	cidval 17734	. . . . . 6 ⊢ (𝜑 → ( 1 ‘𝑌) = (℩𝑔 ∈ (𝑌𝐻𝑌)∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓)))
21	14, 15, 16, 17, 19	catideu 17732	. . . . . . 7 ⊢ (𝜑 → ∃!𝑔 ∈ (𝑌𝐻𝑌)∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓))
22		riotacl2 7385	. . . . . . 7 ⊢ (∃!𝑔 ∈ (𝑌𝐻𝑌)∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓) → (℩𝑔 ∈ (𝑌𝐻𝑌)∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓)) ∈ {𝑔 ∈ (𝑌𝐻𝑌) ∣ ∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓)})
23	21, 22	syl 18	. . . . . 6 ⊢ (𝜑 → (℩𝑔 ∈ (𝑌𝐻𝑌)∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓)) ∈ {𝑔 ∈ (𝑌𝐻𝑌) ∣ ∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓)})
24	20, 23	eqeltrd 2863	. . . . 5 ⊢ (𝜑 → ( 1 ‘𝑌) ∈ {𝑔 ∈ (𝑌𝐻𝑌) ∣ ∀𝑥 ∈ 𝐵 (∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑌𝐻𝑥)(𝑓(⟨𝑌, 𝑌⟩ · 𝑥)𝑔) = 𝑓)})
25	13, 24	sselid 3936	. . . 4 ⊢ (𝜑 → ( 1 ‘𝑌) ∈ {𝑔 ∈ (𝑌𝐻𝑌) ∣ ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓})
26		oveq1 7419	. . . . . . . 8 ⊢ (𝑔 = ( 1 ‘𝑌) → (𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = (( 1 ‘𝑌)(⟨𝑥, 𝑌⟩ · 𝑌)𝑓))
27	26	eqeq1d 2765	. . . . . . 7 ⊢ (𝑔 = ( 1 ‘𝑌) → ((𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ↔ (( 1 ‘𝑌)(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓))
28	27	2ralbidv 3229	. . . . . 6 ⊢ (𝑔 = ( 1 ‘𝑌) → (∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓 ↔ ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(( 1 ‘𝑌)(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓))
29	28	elrab 3651	. . . . 5 ⊢ (( 1 ‘𝑌) ∈ {𝑔 ∈ (𝑌𝐻𝑌) ∣ ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓} ↔ (( 1 ‘𝑌) ∈ (𝑌𝐻𝑌) ∧ ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(( 1 ‘𝑌)(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓))
30	29	simprbi 502	. . . 4 ⊢ (( 1 ‘𝑌) ∈ {𝑔 ∈ (𝑌𝐻𝑌) ∣ ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(𝑔(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓} → ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(( 1 ‘𝑌)(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓)
31	25, 30	syl 18	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑌)(( 1 ‘𝑌)(⟨𝑥, 𝑌⟩ · 𝑌)𝑓) = 𝑓)
32		catidcl.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
33	9, 31, 32	rspcdva 3583	. 2 ⊢ (𝜑 → ∀𝑓 ∈ (𝑋𝐻𝑌)(( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝑓) = 𝑓)
34		catlid.f	. 2 ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))
35	3, 33, 34	rspcdva 3583	1 ⊢ (𝜑 → (( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∃!wreu 3367  {crab 3416  ⟨cop 4596  ‘cfv 6538  ℩crio 7368  (class class class)co 7412  Basecbs 17270  Hom chom 17322  compcco 17323  Catccat 17721  Idccid 17722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-cat 17725  df-cid 17726

This theorem is referenced by:  oppccatid  17776  sectcan  17813  sectco  17814  sectmon  17840  monsect  17841  sectid  17844  invisoinvl  17848  subccatid  17904  fucidcl  18026  fuclid  18027  invfuc  18035  arwlid  18130  xpccatid  18245  evlfcl  18279  curf1cl  18285  curf2cl  18288  curfcl  18289  curfuncf  18295  uncfcurf  18296  hofcl  18316  yon12  18322  yon2  18323  yonedalem3b  18336  yonedainv  18338  bj-endmnd  37943  endmndlem  49776  idmon  49781  discsubc  49825  upciclem3  49929  fucoid  50109  fucolid  50122  coccom  50425