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	⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
	estrcbas.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	estrchomfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	estrchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
	estrchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
	estrchom.a	⊢ 𝐴 = ( Base ‘ 𝑋 )
	estrchom.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion	elestrchom	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		estrcbas.c	⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2		estrcbas.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		estrchomfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		estrchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5		estrchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
6		estrchom.a	⊢ 𝐴 = ( Base ‘ 𝑋 )
7		estrchom.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
8	1 2 3 4 5 6 7	estrchom	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝐵 ↑m 𝐴 ) )
9	8	eleq2d	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ↔ 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ) )
10	7	fvexi	⊢ 𝐵 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
12	6	fvexi	⊢ 𝐴 ∈ V
13	12	a1i	⊢ ( 𝜑 → 𝐴 ∈ V )
14	11 13	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )
15	9 14	bitrd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )