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

Metamath Proof Explorer

Theorem estrcid

Description: The identity arrow in the category of extensible structures is the identity function of base sets. (Contributed by AV, 8-Mar-2020)

Ref Expression
Hypotheses estrccat.c ⊢ C = ExtStrCat ⁡ U
estrcid.o ⊢ 1 ˙ = Id ⁡ C
estrcid.u ⊢ φ → U ∈ V
estrcid.x ⊢ φ → X ∈ U
Assertion estrcid ⊢ φ → 1 ˙ ⁡ X = I ↾ Base X

Proof

Step Hyp Ref Expression
1 estrccat.c ⊢ C = ExtStrCat ⁡ U
2 estrcid.o ⊢ 1 ˙ = Id ⁡ C
3 estrcid.u ⊢ φ → U ∈ V
4 estrcid.x ⊢ φ → X ∈ U
5 1 estrccatid ⊢ U ∈ V → C ∈ Cat ∧ Id ⁡ C = x ∈ U ⟼ I ↾ Base x
6 3 5 syl ⊢ φ → C ∈ Cat ∧ Id ⁡ C = x ∈ U ⟼ I ↾ Base x
7 6 simprd ⊢ φ → Id ⁡ C = x ∈ U ⟼ I ↾ Base x
8 2 7 eqtrid ⊢ φ → 1 ˙ = x ∈ U ⟼ I ↾ Base x
9 fveq2 ⊢ x = X → Base x = Base X
10 9 reseq2d ⊢ x = X → I ↾ Base x = I ↾ Base X
11 10 adantl ⊢ φ ∧ x = X → I ↾ Base x = I ↾ Base X
12 fvexd ⊢ φ → Base X ∈ V
13 12 resiexd ⊢ φ → I ↾ Base X ∈ V
14 8 11 4 13 fvmptd ⊢ φ → 1 ˙ ⁡ X = I ↾ Base X