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

Metamath Proof Explorer

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 ⊢ C = ExtStrCat ⁡ U
estrcbas.u ⊢ φ → U ∈ V
estrchomfval.h ⊢ H = Hom ⁡ C
estrchom.x ⊢ φ → X ∈ U
estrchom.y ⊢ φ → Y ∈ U
estrchom.a ⊢ A = Base X
estrchom.b ⊢ B = Base Y
Assertion estrchom ⊢ φ → X H Y = B A

Proof

Step Hyp Ref Expression
1 estrcbas.c ⊢ C = ExtStrCat ⁡ U
2 estrcbas.u ⊢ φ → U ∈ V
3 estrchomfval.h ⊢ H = Hom ⁡ C
4 estrchom.x ⊢ φ → X ∈ U
5 estrchom.y ⊢ φ → Y ∈ U
6 estrchom.a ⊢ A = Base X
7 estrchom.b ⊢ B = Base Y
8 1 2 3 estrchomfval ⊢ φ → H = x ∈ U , y ∈ U ⟼ Base y Base x
9 fveq2 ⊢ y = Y → Base y = Base Y
10 fveq2 ⊢ x = X → Base x = Base X
11 9 10 oveqan12rd ⊢ x = X ∧ y = Y → Base y Base x = Base Y Base X
12 7 6 oveq12i ⊢ B A = Base Y Base X
13 11 12 eqtr4di ⊢ x = X ∧ y = Y → Base y Base x = B A
14 13 adantl ⊢ φ ∧ x = X ∧ y = Y → Base y Base x = B A
15 ovexd ⊢ φ → B A ∈ V
16 8 14 4 5 15 ovmpod ⊢ φ → X H Y = B A