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	syl5eq	⊢ ( 𝜑 → 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 ‘ 𝑋 ) ) )