This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 sselid ⊢ ( 𝜑 → ( 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 ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑌 ) 𝐹 ) = 𝐹 )