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

Metamath Proof Explorer

Theorem idfu1st

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

Ref Expression
Hypotheses idfuval.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
idfuval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
idfuval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion idfu1st ( 𝜑 → ( 1st ‘ 𝐼 ) = ( I ↾ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 idfuval.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
2 idfuval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 idfuval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
5 1 2 3 4 idfuval ⊢ ( 𝜑 → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ⟩ )
6 5 fveq2d ⊢ ( 𝜑 → ( 1st ‘ 𝐼 ) = ( 1st ‘ ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ⟩ ) )
7 2 fvexi ⊢ 𝐵 ∈ V
8 resiexg ⊢ ( 𝐵 ∈ V → ( I ↾ 𝐵 ) ∈ V )
9 7 8 ax-mp ⊢ ( I ↾ 𝐵 ) ∈ V
10 7 7 xpex ⊢ ( 𝐵 × 𝐵 ) ∈ V
11 10 mptex ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ∈ V
12 9 11 op1st ⊢ ( 1st ‘ ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) ⟩ ) = ( I ↾ 𝐵 )
13 6 12 eqtrdi ⊢ ( 𝜑 → ( 1st ‘ 𝐼 ) = ( I ↾ 𝐵 ) )