Database
BASIC CATEGORY THEORY
Arrows (disjointified hom-sets)
homarel
Next ⟩
homa1
Metamath Proof Explorer
Ascii
Unicode
Theorem
homarel
Description:
An arrow is an ordered pair.
(Contributed by
Mario Carneiro
, 11-Jan-2017)
Ref
Expression
Hypothesis
homahom.h
⊢
H
=
Hom
a
⁡
C
Assertion
homarel
⊢
Rel
⁡
X
H
Y
Proof
Step
Hyp
Ref
Expression
1
homahom.h
⊢
H
=
Hom
a
⁡
C
2
xpss
⊢
Base
C
×
Base
C
×
V
⊆
V
×
V
3
eqid
⊢
Base
C
=
Base
C
4
1
homarcl
⊢
f
∈
X
H
Y
→
C
∈
Cat
5
1
3
4
homaf
⊢
f
∈
X
H
Y
→
H
:
Base
C
×
Base
C
⟶
𝒫
Base
C
×
Base
C
×
V
6
1
3
homarcl2
⊢
f
∈
X
H
Y
→
X
∈
Base
C
∧
Y
∈
Base
C
7
6
simpld
⊢
f
∈
X
H
Y
→
X
∈
Base
C
8
6
simprd
⊢
f
∈
X
H
Y
→
Y
∈
Base
C
9
5
7
8
fovrnd
⊢
f
∈
X
H
Y
→
X
H
Y
∈
𝒫
Base
C
×
Base
C
×
V
10
elelpwi
⊢
f
∈
X
H
Y
∧
X
H
Y
∈
𝒫
Base
C
×
Base
C
×
V
→
f
∈
Base
C
×
Base
C
×
V
11
9
10
mpdan
⊢
f
∈
X
H
Y
→
f
∈
Base
C
×
Base
C
×
V
12
2
11
sseldi
⊢
f
∈
X
H
Y
→
f
∈
V
×
V
13
12
ssriv
⊢
X
H
Y
⊆
V
×
V
14
df-rel
⊢
Rel
⁡
X
H
Y
↔
X
H
Y
⊆
V
×
V
15
13
14
mpbir
⊢
Rel
⁡
X
H
Y