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 )