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

Metamath Proof Explorer

Theorem setcid

Description: The identity arrow in the category of sets is the identity function. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setccat.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
setcid.o ⊢ 1 = ( Id ‘ 𝐶 )
setcid.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
setcid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
Assertion setcid ( 𝜑 → ( 1 ‘ 𝑋 ) = ( I ↾ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 setccat.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2 setcid.o ⊢ 1 = ( Id ‘ 𝐶 )
3 setcid.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 setcid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5 1 setccatid ⊢ ( 𝑈 ∈ 𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥 ) ) ) )
6 3 5 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥 ) ) ) )
7 6 simprd ⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥 ) ) )
8 2 7 eqtrid ⊢ ( 𝜑 → 1 = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥 ) ) )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
10 9 reseq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( I ↾ 𝑥 ) = ( I ↾ 𝑋 ) )
11 4 resiexd ⊢ ( 𝜑 → ( I ↾ 𝑋 ) ∈ V )
12 8 10 4 11 fvmptd ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( I ↾ 𝑋 ) )