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

Metamath Proof Explorer

Theorem estrchomfn

Description: The Hom-set operation in the category of extensible structures (in a universe) is a function. (Contributed by AV, 8-Mar-2020)

Ref Expression
Hypotheses estrchomfn.c ⊢ C = ExtStrCat ⁡ U
estrchomfn.u ⊢ φ → U ∈ V
estrchomfn.h ⊢ H = Hom ⁡ C
Assertion estrchomfn ⊢ φ → H Fn U × U

Proof

Step Hyp Ref Expression
1 estrchomfn.c ⊢ C = ExtStrCat ⁡ U
2 estrchomfn.u ⊢ φ → U ∈ V
3 estrchomfn.h ⊢ H = Hom ⁡ C
4 eqid ⊢ x ∈ U , y ∈ U ⟼ Base y Base x = x ∈ U , y ∈ U ⟼ Base y Base x
5 ovex ⊢ Base y Base x ∈ V
6 4 5 fnmpoi ⊢ x ∈ U , y ∈ U ⟼ Base y Base x Fn U × U
7 1 2 3 estrchomfval ⊢ φ → H = x ∈ U , y ∈ U ⟼ Base y Base x
8 7 fneq1d ⊢ φ → H Fn U × U ↔ x ∈ U , y ∈ U ⟼ Base y Base x Fn U × U
9 6 8 mpbiri ⊢ φ → H Fn U × U