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 ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
estrcid.o ⊢ 1 = ( Id ‘ 𝐶 )
estrcid.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
estrcid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
Assertion estrcid ( 𝜑 → ( 1 ‘ 𝑋 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 estrccat.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 estrcid.o ⊢ 1 = ( Id ‘ 𝐶 )
3 estrcid.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 estrcid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5 1 estrccatid ⊢ ( 𝑈 ∈ 𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )
6 3 5 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )
7 6 simprd ⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) )
8 2 7 eqtrid ⊢ ( 𝜑 → 1 = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) )
9 fveq2 ⊢ ( 𝑥 = 𝑋 → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑋 ) )
10 9 reseq2d ⊢ ( 𝑥 = 𝑋 → ( I ↾ ( Base ‘ 𝑥 ) ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( I ↾ ( Base ‘ 𝑥 ) ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
12 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑋 ) ∈ V )
13 12 resiexd ⊢ ( 𝜑 → ( I ↾ ( Base ‘ 𝑋 ) ) ∈ V )
14 8 11 4 13 fvmptd ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )