Step |
Hyp |
Ref |
Expression |
1 |
|
ciclcl |
|- ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> R e. ( Base ` C ) ) |
2 |
|
cicrcl |
|- ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> S e. ( Base ` C ) ) |
3 |
1 2
|
jca |
|- ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) ) |
4 |
3
|
ex |
|- ( C e. Cat -> ( R ( ~=c ` C ) S -> ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) ) ) |
5 |
|
cicrcl |
|- ( ( C e. Cat /\ S ( ~=c ` C ) T ) -> T e. ( Base ` C ) ) |
6 |
5
|
ex |
|- ( C e. Cat -> ( S ( ~=c ` C ) T -> T e. ( Base ` C ) ) ) |
7 |
4 6
|
anim12d |
|- ( C e. Cat -> ( ( R ( ~=c ` C ) S /\ S ( ~=c ` C ) T ) -> ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) ) |
8 |
7
|
3impib |
|- ( ( C e. Cat /\ R ( ~=c ` C ) S /\ S ( ~=c ` C ) T ) -> ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) |
9 |
|
eqid |
|- ( Iso ` C ) = ( Iso ` C ) |
10 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
11 |
|
simpl |
|- ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> C e. Cat ) |
12 |
|
simpll |
|- ( ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) -> R e. ( Base ` C ) ) |
13 |
12
|
adantl |
|- ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> R e. ( Base ` C ) ) |
14 |
|
simplr |
|- ( ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) -> S e. ( Base ` C ) ) |
15 |
14
|
adantl |
|- ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> S e. ( Base ` C ) ) |
16 |
9 10 11 13 15
|
cic |
|- ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> ( R ( ~=c ` C ) S <-> E. f f e. ( R ( Iso ` C ) S ) ) ) |
17 |
|
simprr |
|- ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> T e. ( Base ` C ) ) |
18 |
9 10 11 15 17
|
cic |
|- ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> ( S ( ~=c ` C ) T <-> E. g g e. ( S ( Iso ` C ) T ) ) ) |
19 |
16 18
|
anbi12d |
|- ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> ( ( R ( ~=c ` C ) S /\ S ( ~=c ` C ) T ) <-> ( E. f f e. ( R ( Iso ` C ) S ) /\ E. g g e. ( S ( Iso ` C ) T ) ) ) ) |
20 |
11
|
adantl |
|- ( ( ( g e. ( S ( Iso ` C ) T ) /\ f e. ( R ( Iso ` C ) S ) ) /\ ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) ) -> C e. Cat ) |
21 |
13
|
adantl |
|- ( ( ( g e. ( S ( Iso ` C ) T ) /\ f e. ( R ( Iso ` C ) S ) ) /\ ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) ) -> R e. ( Base ` C ) ) |
22 |
17
|
adantl |
|- ( ( ( g e. ( S ( Iso ` C ) T ) /\ f e. ( R ( Iso ` C ) S ) ) /\ ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) ) -> T e. ( Base ` C ) ) |
23 |
|
eqid |
|- ( comp ` C ) = ( comp ` C ) |
24 |
15
|
adantl |
|- ( ( ( g e. ( S ( Iso ` C ) T ) /\ f e. ( R ( Iso ` C ) S ) ) /\ ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) ) -> S e. ( Base ` C ) ) |
25 |
|
simplr |
|- ( ( ( g e. ( S ( Iso ` C ) T ) /\ f e. ( R ( Iso ` C ) S ) ) /\ ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) ) -> f e. ( R ( Iso ` C ) S ) ) |
26 |
|
simpll |
|- ( ( ( g e. ( S ( Iso ` C ) T ) /\ f e. ( R ( Iso ` C ) S ) ) /\ ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) ) -> g e. ( S ( Iso ` C ) T ) ) |
27 |
10 23 9 20 21 24 22 25 26
|
isoco |
|- ( ( ( g e. ( S ( Iso ` C ) T ) /\ f e. ( R ( Iso ` C ) S ) ) /\ ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) ) -> ( g ( <. R , S >. ( comp ` C ) T ) f ) e. ( R ( Iso ` C ) T ) ) |
28 |
9 10 20 21 22 27
|
brcici |
|- ( ( ( g e. ( S ( Iso ` C ) T ) /\ f e. ( R ( Iso ` C ) S ) ) /\ ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) ) -> R ( ~=c ` C ) T ) |
29 |
28
|
ex |
|- ( ( g e. ( S ( Iso ` C ) T ) /\ f e. ( R ( Iso ` C ) S ) ) -> ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> R ( ~=c ` C ) T ) ) |
30 |
29
|
ex |
|- ( g e. ( S ( Iso ` C ) T ) -> ( f e. ( R ( Iso ` C ) S ) -> ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> R ( ~=c ` C ) T ) ) ) |
31 |
30
|
exlimiv |
|- ( E. g g e. ( S ( Iso ` C ) T ) -> ( f e. ( R ( Iso ` C ) S ) -> ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> R ( ~=c ` C ) T ) ) ) |
32 |
31
|
com12 |
|- ( f e. ( R ( Iso ` C ) S ) -> ( E. g g e. ( S ( Iso ` C ) T ) -> ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> R ( ~=c ` C ) T ) ) ) |
33 |
32
|
exlimiv |
|- ( E. f f e. ( R ( Iso ` C ) S ) -> ( E. g g e. ( S ( Iso ` C ) T ) -> ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> R ( ~=c ` C ) T ) ) ) |
34 |
33
|
imp |
|- ( ( E. f f e. ( R ( Iso ` C ) S ) /\ E. g g e. ( S ( Iso ` C ) T ) ) -> ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> R ( ~=c ` C ) T ) ) |
35 |
34
|
com12 |
|- ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> ( ( E. f f e. ( R ( Iso ` C ) S ) /\ E. g g e. ( S ( Iso ` C ) T ) ) -> R ( ~=c ` C ) T ) ) |
36 |
19 35
|
sylbid |
|- ( ( C e. Cat /\ ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) ) -> ( ( R ( ~=c ` C ) S /\ S ( ~=c ` C ) T ) -> R ( ~=c ` C ) T ) ) |
37 |
36
|
ex |
|- ( C e. Cat -> ( ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) -> ( ( R ( ~=c ` C ) S /\ S ( ~=c ` C ) T ) -> R ( ~=c ` C ) T ) ) ) |
38 |
37
|
com23 |
|- ( C e. Cat -> ( ( R ( ~=c ` C ) S /\ S ( ~=c ` C ) T ) -> ( ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) -> R ( ~=c ` C ) T ) ) ) |
39 |
38
|
3impib |
|- ( ( C e. Cat /\ R ( ~=c ` C ) S /\ S ( ~=c ` C ) T ) -> ( ( ( R e. ( Base ` C ) /\ S e. ( Base ` C ) ) /\ T e. ( Base ` C ) ) -> R ( ~=c ` C ) T ) ) |
40 |
8 39
|
mpd |
|- ( ( C e. Cat /\ R ( ~=c ` C ) S /\ S ( ~=c ` C ) T ) -> R ( ~=c ` C ) T ) |