Theorem estrchom

Description: The morphisms between extensible structures are mappings 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	estrchom	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝐵 ↑m 𝐴 ) )

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	estrchomfval	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
9		fveq2	⊢ ( 𝑦 = 𝑌 → ( Base ‘ 𝑦 ) = ( Base ‘ 𝑌 ) )
10		fveq2	⊢ ( 𝑥 = 𝑋 → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑋 ) )
11	9 10	oveqan12rd	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) = ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
12	7 6	oveq12i	⊢ ( 𝐵 ↑m 𝐴 ) = ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) )
13	11 12	eqtr4di	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) = ( 𝐵 ↑m 𝐴 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) = ( 𝐵 ↑m 𝐴 ) )
15		ovexd	⊢ ( 𝜑 → ( 𝐵 ↑m 𝐴 ) ∈ V )
16	8 14 4 5 15	ovmpod	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝐵 ↑m 𝐴 ) )