Step |
Hyp |
Ref |
Expression |
1 |
|
homahom.h |
|- H = ( HomA ` C ) |
2 |
|
xpss |
|- ( ( ( Base ` C ) X. ( Base ` C ) ) X. _V ) C_ ( _V X. _V ) |
3 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
4 |
1
|
homarcl |
|- ( f e. ( X H Y ) -> C e. Cat ) |
5 |
1 3 4
|
homaf |
|- ( f e. ( X H Y ) -> H : ( ( Base ` C ) X. ( Base ` C ) ) --> ~P ( ( ( Base ` C ) X. ( Base ` C ) ) X. _V ) ) |
6 |
1 3
|
homarcl2 |
|- ( f e. ( X H Y ) -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) |
7 |
6
|
simpld |
|- ( f e. ( X H Y ) -> X e. ( Base ` C ) ) |
8 |
6
|
simprd |
|- ( f e. ( X H Y ) -> Y e. ( Base ` C ) ) |
9 |
5 7 8
|
fovrnd |
|- ( f e. ( X H Y ) -> ( X H Y ) e. ~P ( ( ( Base ` C ) X. ( Base ` C ) ) X. _V ) ) |
10 |
|
elelpwi |
|- ( ( f e. ( X H Y ) /\ ( X H Y ) e. ~P ( ( ( Base ` C ) X. ( Base ` C ) ) X. _V ) ) -> f e. ( ( ( Base ` C ) X. ( Base ` C ) ) X. _V ) ) |
11 |
9 10
|
mpdan |
|- ( f e. ( X H Y ) -> f e. ( ( ( Base ` C ) X. ( Base ` C ) ) X. _V ) ) |
12 |
2 11
|
sselid |
|- ( f e. ( X H Y ) -> f e. ( _V X. _V ) ) |
13 |
12
|
ssriv |
|- ( X H Y ) C_ ( _V X. _V ) |
14 |
|
df-rel |
|- ( Rel ( X H Y ) <-> ( X H Y ) C_ ( _V X. _V ) ) |
15 |
13 14
|
mpbir |
|- Rel ( X H Y ) |