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

Metamath Proof Explorer

Theorem elrngchom

Description: A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rngcbas.c ⊢ C = RngCat ⁡ U
rngcbas.b ⊢ B = Base C
rngcbas.u ⊢ φ → U ∈ V
rngchomfval.h ⊢ H = Hom ⁡ C
rngchom.x ⊢ φ → X ∈ B
rngchom.y ⊢ φ → Y ∈ B
Assertion elrngchom ⊢ φ → F ∈ X H Y → F : Base X ⟶ Base Y

Proof

Step Hyp Ref Expression
1 rngcbas.c ⊢ C = RngCat ⁡ U
2 rngcbas.b ⊢ B = Base C
3 rngcbas.u ⊢ φ → U ∈ V
4 rngchomfval.h ⊢ H = Hom ⁡ C
5 rngchom.x ⊢ φ → X ∈ B
6 rngchom.y ⊢ φ → Y ∈ B
7 1 2 3 4 5 6 rngchom ⊢ φ → X H Y = X RngHom Y
8 7 eleq2d ⊢ φ → F ∈ X H Y ↔ F ∈ X RngHom Y
9 eqid ⊢ Base X = Base X
10 eqid ⊢ Base Y = Base Y
11 9 10 rnghmf ⊢ F ∈ X RngHom Y → F : Base X ⟶ Base Y
12 8 11 biimtrdi ⊢ φ → F ∈ X H Y → F : Base X ⟶ Base Y