| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cicpropd.1 |
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) ) |
| 2 |
|
cicpropd.2 |
|- ( ph -> ( comf ` C ) = ( comf ` D ) ) |
| 3 |
|
cic1st2nd |
|- ( P e. ( ~=c ` C ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) |
| 4 |
3
|
adantl |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) |
| 5 |
|
cic1st2ndbr |
|- ( P e. ( ~=c ` C ) -> ( 1st ` P ) ( ~=c ` C ) ( 2nd ` P ) ) |
| 6 |
5
|
adantl |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( 1st ` P ) ( ~=c ` C ) ( 2nd ` P ) ) |
| 7 |
1
|
adantr |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) ) |
| 8 |
2
|
adantr |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( comf ` C ) = ( comf ` D ) ) |
| 9 |
7 8
|
isopropd |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( Iso ` C ) = ( Iso ` D ) ) |
| 10 |
9
|
oveqd |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( ( 1st ` P ) ( Iso ` C ) ( 2nd ` P ) ) = ( ( 1st ` P ) ( Iso ` D ) ( 2nd ` P ) ) ) |
| 11 |
10
|
neeq1d |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( ( ( 1st ` P ) ( Iso ` C ) ( 2nd ` P ) ) =/= (/) <-> ( ( 1st ` P ) ( Iso ` D ) ( 2nd ` P ) ) =/= (/) ) ) |
| 12 |
|
eqid |
|- ( Iso ` C ) = ( Iso ` C ) |
| 13 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
| 14 |
|
cicrcl2 |
|- ( ( 1st ` P ) ( ~=c ` C ) ( 2nd ` P ) -> C e. Cat ) |
| 15 |
5 14
|
syl |
|- ( P e. ( ~=c ` C ) -> C e. Cat ) |
| 16 |
15
|
adantl |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> C e. Cat ) |
| 17 |
|
ciclcl |
|- ( ( C e. Cat /\ ( 1st ` P ) ( ~=c ` C ) ( 2nd ` P ) ) -> ( 1st ` P ) e. ( Base ` C ) ) |
| 18 |
14 17
|
mpancom |
|- ( ( 1st ` P ) ( ~=c ` C ) ( 2nd ` P ) -> ( 1st ` P ) e. ( Base ` C ) ) |
| 19 |
5 18
|
syl |
|- ( P e. ( ~=c ` C ) -> ( 1st ` P ) e. ( Base ` C ) ) |
| 20 |
19
|
adantl |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( 1st ` P ) e. ( Base ` C ) ) |
| 21 |
|
cicrcl |
|- ( ( C e. Cat /\ ( 1st ` P ) ( ~=c ` C ) ( 2nd ` P ) ) -> ( 2nd ` P ) e. ( Base ` C ) ) |
| 22 |
14 21
|
mpancom |
|- ( ( 1st ` P ) ( ~=c ` C ) ( 2nd ` P ) -> ( 2nd ` P ) e. ( Base ` C ) ) |
| 23 |
5 22
|
syl |
|- ( P e. ( ~=c ` C ) -> ( 2nd ` P ) e. ( Base ` C ) ) |
| 24 |
23
|
adantl |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( 2nd ` P ) e. ( Base ` C ) ) |
| 25 |
12 13 16 20 24
|
brcic |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( ( 1st ` P ) ( ~=c ` C ) ( 2nd ` P ) <-> ( ( 1st ` P ) ( Iso ` C ) ( 2nd ` P ) ) =/= (/) ) ) |
| 26 |
|
eqid |
|- ( Iso ` D ) = ( Iso ` D ) |
| 27 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
| 28 |
1
|
homfeqbas |
|- ( ph -> ( Base ` C ) = ( Base ` D ) ) |
| 29 |
28
|
adantr |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( Base ` C ) = ( Base ` D ) ) |
| 30 |
20 29
|
eleqtrd |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( 1st ` P ) e. ( Base ` D ) ) |
| 31 |
30
|
elfvexd |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> D e. _V ) |
| 32 |
7 8 16 31
|
catpropd |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( C e. Cat <-> D e. Cat ) ) |
| 33 |
16 32
|
mpbid |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> D e. Cat ) |
| 34 |
24 29
|
eleqtrd |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( 2nd ` P ) e. ( Base ` D ) ) |
| 35 |
26 27 33 30 34
|
brcic |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( ( 1st ` P ) ( ~=c ` D ) ( 2nd ` P ) <-> ( ( 1st ` P ) ( Iso ` D ) ( 2nd ` P ) ) =/= (/) ) ) |
| 36 |
11 25 35
|
3bitr4d |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( ( 1st ` P ) ( ~=c ` C ) ( 2nd ` P ) <-> ( 1st ` P ) ( ~=c ` D ) ( 2nd ` P ) ) ) |
| 37 |
6 36
|
mpbid |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> ( 1st ` P ) ( ~=c ` D ) ( 2nd ` P ) ) |
| 38 |
|
df-br |
|- ( ( 1st ` P ) ( ~=c ` D ) ( 2nd ` P ) <-> <. ( 1st ` P ) , ( 2nd ` P ) >. e. ( ~=c ` D ) ) |
| 39 |
37 38
|
sylib |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> <. ( 1st ` P ) , ( 2nd ` P ) >. e. ( ~=c ` D ) ) |
| 40 |
4 39
|
eqeltrd |
|- ( ( ph /\ P e. ( ~=c ` C ) ) -> P e. ( ~=c ` D ) ) |