Metamath Proof Explorer

Theorem grictr

Description: Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022) (Revised by AV, 3-May-2025)

Ref Expression
Assertion grictr 
|- ( ( R ~=gr S /\ S ~=gr T ) -> R ~=gr T )

Proof

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