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

Metamath Proof Explorer

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 ⊢ φ → 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 elestrchom ⊢ φ → F ∈ X H Y ↔ F : A ⟶ B

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 4 5 6 7 estrchom ⊢ φ → X H Y = B A
9 8 eleq2d ⊢ φ → F ∈ X H Y ↔ F ∈ B A
10 7 fvexi ⊢ B ∈ V
11 10 a1i ⊢ φ → B ∈ V
12 6 fvexi ⊢ A ∈ V
13 12 a1i ⊢ φ → A ∈ V
14 11 13 elmapd ⊢ φ → F ∈ B A ↔ F : A ⟶ B
15 9 14 bitrd ⊢ φ → F ∈ X H Y ↔ F : A ⟶ B