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

Metamath Proof Explorer

Theorem idfuval

Description: Value of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses idfuval.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
idfuval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
idfuval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
idfuval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion idfuval ( 𝜑 → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )

Proof

Step Hyp Ref Expression
1 idfuval.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
2 idfuval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 idfuval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 idfuval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
5 fvexd ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) ∈ V )
6 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
7 6 2 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
8 simpr ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
9 8 reseq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( I ↾ 𝑏 ) = ( I ↾ 𝐵 ) )
10 8 sqxpeqd ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) )
11 simpl ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → 𝑐 = 𝐶 )
12 11 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
13 12 4 eqtr4di ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = 𝐻 )
14 13 fveq1d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) = ( 𝐻 ‘ 𝑧 ) )
15 14 reseq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) = ( I ↾ ( 𝐻 ‘ 𝑧 ) ) )
16 10 15 mpteq12dv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) )
17 9 16 opeq12d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
18 5 7 17 csbied2 ⊢ ( 𝑐 = 𝐶 → ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
19 df-idfu ⊢ idfunc = ( 𝑐 ∈ Cat ↦ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑐 ) ‘ 𝑧 ) ) ) ⟩ )
20 opex ⊢ ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ∈ V
21 18 19 20 fvmpt ⊢ ( 𝐶 ∈ Cat → ( idfunc ‘ 𝐶 ) = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
22 3 21 syl ⊢ ( 𝜑 → ( idfunc ‘ 𝐶 ) = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
23 1 22 eqtrid ⊢ ( 𝜑 → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )