Metamath Proof Explorer


Theorem cictr

Description: Isomorphism is transitive. (Contributed by AV, 5-Apr-2020)

Ref Expression
Assertion cictr
|- ( ( C e. Cat /\ R ( ~=c ` C ) S /\ S ( ~=c ` C ) T ) -> R ( ~=c ` C ) T )

Proof

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 )