Theorem elestrchom

Description: A morphism between extensible structures is a function between their base sets. (Contributed by AV, 7-Mar-2020)

	Ref	Expression
Hypotheses	estrcbas.c	|- C = ( ExtStrCat ` U )
	estrcbas.u	|- ( ph -> U e. V )
	estrchomfval.h	|- H = ( Hom ` C )
	estrchom.x	|- ( ph -> X e. U )
	estrchom.y	|- ( ph -> Y e. U )
	estrchom.a	|- A = ( Base ` X )
	estrchom.b	|- B = ( Base ` Y )
Assertion	elestrchom	|- ( ph -> ( F e. ( X H Y ) <-> F : A --> B ) )

Proof

Step	Hyp	Ref	Expression
1		estrcbas.c	|- C = ( ExtStrCat ` U )
2		estrcbas.u	|- ( ph -> U e. V )
3		estrchomfval.h	|- H = ( Hom ` C )
4		estrchom.x	|- ( ph -> X e. U )
5		estrchom.y	|- ( ph -> Y e. U )
6		estrchom.a	|- A = ( Base ` X )
7		estrchom.b	|- B = ( Base ` Y )
8	1 2 3 4 5 6 7	estrchom	|- ( ph -> ( X H Y ) = ( B ^m A ) )
9	8	eleq2d	|- ( ph -> ( F e. ( X H Y ) <-> F e. ( B ^m A ) ) )
10	7	fvexi	|- B e. _V
11	10	a1i	|- ( ph -> B e. _V )
12	6	fvexi	|- A e. _V
13	12	a1i	|- ( ph -> A e. _V )
14	11 13	elmapd	|- ( ph -> ( F e. ( B ^m A ) <-> F : A --> B ) )
15	9 14	bitrd	|- ( ph -> ( F e. ( X H Y ) <-> F : A --> B ) )