Metamath Proof Explorer

Theorem gictr

Description: Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion gictr 
|- ( ( R ~=g S /\ S ~=g T ) -> R ~=g T )

Proof

Step Hyp Ref Expression
1 brgic 
 |-  ( R ~=g S <-> ( R GrpIso S ) =/= (/) )
2 brgic 
 |-  ( S ~=g T <-> ( S GrpIso T ) =/= (/) )
3 n0 
 |-  ( ( R GrpIso S ) =/= (/) <-> E. f f e. ( R GrpIso S ) )
4 n0 
 |-  ( ( S GrpIso T ) =/= (/) <-> E. g g e. ( S GrpIso T ) )
5 exdistrv 
 |-  ( E. f E. g ( f e. ( R GrpIso S ) /\ g e. ( S GrpIso T ) ) <-> ( E. f f e. ( R GrpIso S ) /\ E. g g e. ( S GrpIso T ) ) )
6 gimco 
 |-  ( ( g e. ( S GrpIso T ) /\ f e. ( R GrpIso S ) ) -> ( g o. f ) e. ( R GrpIso T ) )
7 brgici 
 |-  ( ( g o. f ) e. ( R GrpIso T ) -> R ~=g T )
8 6 7 syl 
 |-  ( ( g e. ( S GrpIso T ) /\ f e. ( R GrpIso S ) ) -> R ~=g T )
9 8 ancoms 
 |-  ( ( f e. ( R GrpIso S ) /\ g e. ( S GrpIso T ) ) -> R ~=g T )
10 9 exlimivv 
 |-  ( E. f E. g ( f e. ( R GrpIso S ) /\ g e. ( S GrpIso T ) ) -> R ~=g T )
11 5 10 sylbir 
 |-  ( ( E. f f e. ( R GrpIso S ) /\ E. g g e. ( S GrpIso T ) ) -> R ~=g T )
12 3 4 11 syl2anb 
 |-  ( ( ( R GrpIso S ) =/= (/) /\ ( S GrpIso T ) =/= (/) ) -> R ~=g T )
13 1 2 12 syl2anb 
 |-  ( ( R ~=g S /\ S ~=g T ) -> R ~=g T )