| Step |
Hyp |
Ref |
Expression |
| 1 |
|
thinccisod.c |
|- C = ( CatCat ` U ) |
| 2 |
|
thinccisod.r |
|- R = ( Base ` X ) |
| 3 |
|
thinccisod.s |
|- S = ( Base ` Y ) |
| 4 |
|
thinccisod.h |
|- H = ( Hom ` X ) |
| 5 |
|
thinccisod.j |
|- J = ( Hom ` Y ) |
| 6 |
|
thinccisod.u |
|- ( ph -> U e. V ) |
| 7 |
|
thinccisod.x |
|- ( ph -> X e. U ) |
| 8 |
|
thinccisod.y |
|- ( ph -> Y e. U ) |
| 9 |
|
thinccisod.xt |
|- ( ph -> X e. ThinCat ) |
| 10 |
|
thinccisod.yt |
|- ( ph -> Y e. ThinCat ) |
| 11 |
|
thinccisod.f |
|- ( ph -> F : R -1-1-onto-> S ) |
| 12 |
|
thinccisod.1 |
|- ( ( ph /\ ( x e. R /\ y e. R ) ) -> ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) |
| 13 |
|
f1of |
|- ( F : R -1-1-onto-> S -> F : R --> S ) |
| 14 |
11 13
|
syl |
|- ( ph -> F : R --> S ) |
| 15 |
|
fvexd |
|- ( ph -> ( Base ` X ) e. _V ) |
| 16 |
2 15
|
eqeltrid |
|- ( ph -> R e. _V ) |
| 17 |
14 16
|
fexd |
|- ( ph -> F e. _V ) |
| 18 |
12
|
ralrimivva |
|- ( ph -> A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) |
| 19 |
18 11
|
jca |
|- ( ph -> ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) /\ F : R -1-1-onto-> S ) ) |
| 20 |
|
fveq1 |
|- ( f = F -> ( f ` x ) = ( F ` x ) ) |
| 21 |
|
fveq1 |
|- ( f = F -> ( f ` y ) = ( F ` y ) ) |
| 22 |
20 21
|
oveq12d |
|- ( f = F -> ( ( f ` x ) J ( f ` y ) ) = ( ( F ` x ) J ( F ` y ) ) ) |
| 23 |
22
|
eqeq1d |
|- ( f = F -> ( ( ( f ` x ) J ( f ` y ) ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) |
| 24 |
23
|
bibi2d |
|- ( f = F -> ( ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) <-> ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) ) |
| 25 |
24
|
2ralbidv |
|- ( f = F -> ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) <-> A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) ) |
| 26 |
|
f1oeq1 |
|- ( f = F -> ( f : R -1-1-onto-> S <-> F : R -1-1-onto-> S ) ) |
| 27 |
25 26
|
anbi12d |
|- ( f = F -> ( ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) <-> ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) /\ F : R -1-1-onto-> S ) ) ) |
| 28 |
17 19 27
|
spcedv |
|- ( ph -> E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) |
| 29 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
| 30 |
9
|
thinccd |
|- ( ph -> X e. Cat ) |
| 31 |
7 30
|
elind |
|- ( ph -> X e. ( U i^i Cat ) ) |
| 32 |
1 29 6
|
catcbas |
|- ( ph -> ( Base ` C ) = ( U i^i Cat ) ) |
| 33 |
31 32
|
eleqtrrd |
|- ( ph -> X e. ( Base ` C ) ) |
| 34 |
10
|
thinccd |
|- ( ph -> Y e. Cat ) |
| 35 |
8 34
|
elind |
|- ( ph -> Y e. ( U i^i Cat ) ) |
| 36 |
35 32
|
eleqtrrd |
|- ( ph -> Y e. ( Base ` C ) ) |
| 37 |
1 29 2 3 4 5 6 33 36 9 10
|
thincciso |
|- ( ph -> ( X ( ~=c ` C ) Y <-> E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) ) |
| 38 |
28 37
|
mpbird |
|- ( ph -> X ( ~=c ` C ) Y ) |