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

Metamath Proof Explorer

Theorem elringchom

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

Ref Expression
Hypotheses ringcbas.c ⊢ C = RingCat ⁡ U
ringcbas.b ⊢ B = Base C
ringcbas.u ⊢ φ → U ∈ V
ringchomfval.h ⊢ H = Hom ⁡ C
ringchom.x ⊢ φ → X ∈ B
ringchom.y ⊢ φ → Y ∈ B
Assertion elringchom ⊢ φ → F ∈ X H Y → F : Base X ⟶ Base Y

Proof

Step Hyp Ref Expression
1 ringcbas.c ⊢ C = RingCat ⁡ U
2 ringcbas.b ⊢ B = Base C
3 ringcbas.u ⊢ φ → U ∈ V
4 ringchomfval.h ⊢ H = Hom ⁡ C
5 ringchom.x ⊢ φ → X ∈ B
6 ringchom.y ⊢ φ → Y ∈ B
7 1 2 3 4 5 6 ringchom ⊢ φ → X H Y = X RingHom Y
8 7 eleq2d ⊢ φ → F ∈ X H Y ↔ F ∈ X RingHom Y
9 eqid ⊢ Base X = Base X
10 eqid ⊢ Base Y = Base Y
11 9 10 rhmf ⊢ F ∈ X RingHom Y → F : Base X ⟶ Base Y
12 8 11 biimtrdi ⊢ φ → F ∈ X H Y → F : Base X ⟶ Base Y