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

Metamath Proof Explorer

Theorem estrchomfeqhom

Description: The functionalized Hom-set operation equals the Hom-set operation in the category of extensible structures (in a universe). (Contributed by AV, 8-Mar-2020)

		Ref	Expression
	Hypotheses	estrchomfn.c	$⊢ C = ExtStrCat (U)$
		estrchomfn.u	$⊢ φ \to U \in V$
		estrchomfn.h	$⊢ H = Hom (C)$
	Assertion	estrchomfeqhom	$⊢ φ \to {Hom}_{𝑓} (C) = H$

Proof

Step	Hyp	Ref	Expression
1		estrchomfn.c	$⊢ C = ExtStrCat (U)$
2		estrchomfn.u	$⊢ φ \to U \in V$
3		estrchomfn.h	$⊢ H = Hom (C)$
4	1 2 3	estrchomfn	$⊢ φ \to H Fn (U \times U)$
5	1 2	estrcbas	$⊢ φ \to U = {Base}_{C}$
6	5	eqcomd	$⊢ φ \to {Base}_{C} = U$
7	6	sqxpeqd	$⊢ φ \to {Base}_{C} \times {Base}_{C} = U \times U$
8	7	fneq2d	$⊢ φ \to (H Fn ({Base}_{C} \times {Base}_{C}) \leftrightarrow H Fn (U \times U))$
9	4 8	mpbird	$⊢ φ \to H Fn ({Base}_{C} \times {Base}_{C})$
10		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
11		eqid	$⊢ {Base}_{C} = {Base}_{C}$
12	10 11 3	fnhomeqhomf	$⊢ H Fn ({Base}_{C} \times {Base}_{C}) \to {Hom}_{𝑓} (C) = H$
13	9 12	syl	$⊢ φ \to {Hom}_{𝑓} (C) = H$