Theorem catlid

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

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

Proof

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