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

Metamath Proof Explorer

Theorem fucid

Description: The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fucid.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
fucid.i ⊢ 𝐼 = ( Id ‘ 𝑄 )
fucid.1 ⊢ 1 = ( Id ‘ 𝐷 )
fucid.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion fucid ( 𝜑 → ( 𝐼 ‘ 𝐹 ) = ( 1 ∘ ( 1st ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 fucid.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2 fucid.i ⊢ 𝐼 = ( Id ‘ 𝑄 )
3 fucid.1 ⊢ 1 = ( Id ‘ 𝐷 )
4 fucid.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5 funcrcl ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
6 4 5 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
7 6 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
8 6 simprd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
9 1 7 8 3 fuccatid ⊢ ( 𝜑 → ( 𝑄 ∈ Cat ∧ ( Id ‘ 𝑄 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1 ∘ ( 1st ‘ 𝑓 ) ) ) ) )
10 9 simprd ⊢ ( 𝜑 → ( Id ‘ 𝑄 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1 ∘ ( 1st ‘ 𝑓 ) ) ) )
11 2 10 eqtrid ⊢ ( 𝜑 → 𝐼 = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1 ∘ ( 1st ‘ 𝑓 ) ) ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
13 12 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 1st ‘ 𝑓 ) = ( 1st ‘ 𝐹 ) )
14 13 coeq2d ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 1 ∘ ( 1st ‘ 𝑓 ) ) = ( 1 ∘ ( 1st ‘ 𝐹 ) ) )
15 3 fvexi ⊢ 1 ∈ V
16 fvex ⊢ ( 1st ‘ 𝐹 ) ∈ V
17 15 16 coex ⊢ ( 1 ∘ ( 1st ‘ 𝐹 ) ) ∈ V
18 17 a1i ⊢ ( 𝜑 → ( 1 ∘ ( 1st ‘ 𝐹 ) ) ∈ V )
19 11 14 4 18 fvmptd ⊢ ( 𝜑 → ( 𝐼 ‘ 𝐹 ) = ( 1 ∘ ( 1st ‘ 𝐹 ) ) )