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 ⊢ C = SetCat ⁡ U
setcid.o ⊢ 1 ˙ = Id ⁡ C
setcid.u ⊢ φ → U ∈ V
setcid.x ⊢ φ → X ∈ U
Assertion setcid ⊢ φ → 1 ˙ ⁡ X = I ↾ X

Proof

Step Hyp Ref Expression
1 setccat.c ⊢ C = SetCat ⁡ U
2 setcid.o ⊢ 1 ˙ = Id ⁡ C
3 setcid.u ⊢ φ → U ∈ V
4 setcid.x ⊢ φ → X ∈ U
5 1 setccatid ⊢ U ∈ V → C ∈ Cat ∧ Id ⁡ C = x ∈ U ⟼ I ↾ x
6 3 5 syl ⊢ φ → C ∈ Cat ∧ Id ⁡ C = x ∈ U ⟼ I ↾ x
7 6 simprd ⊢ φ → Id ⁡ C = x ∈ U ⟼ I ↾ x
8 2 7 eqtrid ⊢ φ → 1 ˙ = x ∈ U ⟼ I ↾ x
9 simpr ⊢ φ ∧ x = X → x = X
10 9 reseq2d ⊢ φ ∧ x = X → I ↾ x = I ↾ X
11 4 resiexd ⊢ φ → I ↾ X ∈ V
12 8 10 4 11 fvmptd ⊢ φ → 1 ˙ ⁡ X = I ↾ X