Step |
Hyp |
Ref |
Expression |
1 |
|
cic.i |
|- I = ( Iso ` C ) |
2 |
|
cic.b |
|- B = ( Base ` C ) |
3 |
|
cic.c |
|- ( ph -> C e. Cat ) |
4 |
|
cic.x |
|- ( ph -> X e. B ) |
5 |
|
cic.y |
|- ( ph -> Y e. B ) |
6 |
|
cicfval |
|- ( C e. Cat -> ( ~=c ` C ) = ( ( Iso ` C ) supp (/) ) ) |
7 |
3 6
|
syl |
|- ( ph -> ( ~=c ` C ) = ( ( Iso ` C ) supp (/) ) ) |
8 |
7
|
breqd |
|- ( ph -> ( X ( ~=c ` C ) Y <-> X ( ( Iso ` C ) supp (/) ) Y ) ) |
9 |
|
df-br |
|- ( X ( ( Iso ` C ) supp (/) ) Y <-> <. X , Y >. e. ( ( Iso ` C ) supp (/) ) ) |
10 |
9
|
a1i |
|- ( ph -> ( X ( ( Iso ` C ) supp (/) ) Y <-> <. X , Y >. e. ( ( Iso ` C ) supp (/) ) ) ) |
11 |
1
|
a1i |
|- ( ph -> I = ( Iso ` C ) ) |
12 |
11
|
fveq1d |
|- ( ph -> ( I ` <. X , Y >. ) = ( ( Iso ` C ) ` <. X , Y >. ) ) |
13 |
12
|
neeq1d |
|- ( ph -> ( ( I ` <. X , Y >. ) =/= (/) <-> ( ( Iso ` C ) ` <. X , Y >. ) =/= (/) ) ) |
14 |
|
df-ov |
|- ( X I Y ) = ( I ` <. X , Y >. ) |
15 |
14
|
eqcomi |
|- ( I ` <. X , Y >. ) = ( X I Y ) |
16 |
15
|
a1i |
|- ( ph -> ( I ` <. X , Y >. ) = ( X I Y ) ) |
17 |
16
|
neeq1d |
|- ( ph -> ( ( I ` <. X , Y >. ) =/= (/) <-> ( X I Y ) =/= (/) ) ) |
18 |
|
fvexd |
|- ( ph -> ( Base ` C ) e. _V ) |
19 |
18 18
|
xpexd |
|- ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) e. _V ) |
20 |
4 2
|
eleqtrdi |
|- ( ph -> X e. ( Base ` C ) ) |
21 |
5 2
|
eleqtrdi |
|- ( ph -> Y e. ( Base ` C ) ) |
22 |
20 21
|
opelxpd |
|- ( ph -> <. X , Y >. e. ( ( Base ` C ) X. ( Base ` C ) ) ) |
23 |
|
isofn |
|- ( C e. Cat -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) |
24 |
3 23
|
syl |
|- ( ph -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) |
25 |
|
fvn0elsuppb |
|- ( ( ( ( Base ` C ) X. ( Base ` C ) ) e. _V /\ <. X , Y >. e. ( ( Base ` C ) X. ( Base ` C ) ) /\ ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( ( Iso ` C ) ` <. X , Y >. ) =/= (/) <-> <. X , Y >. e. ( ( Iso ` C ) supp (/) ) ) ) |
26 |
19 22 24 25
|
syl3anc |
|- ( ph -> ( ( ( Iso ` C ) ` <. X , Y >. ) =/= (/) <-> <. X , Y >. e. ( ( Iso ` C ) supp (/) ) ) ) |
27 |
13 17 26
|
3bitr3rd |
|- ( ph -> ( <. X , Y >. e. ( ( Iso ` C ) supp (/) ) <-> ( X I Y ) =/= (/) ) ) |
28 |
8 10 27
|
3bitrd |
|- ( ph -> ( X ( ~=c ` C ) Y <-> ( X I Y ) =/= (/) ) ) |