Metamath Proof Explorer

Theorem grlictr

Description: Graph local isomorphism is transitive. (Contributed by AV, 10-Jun-2025)

Ref Expression
Assertion grlictr 
|- ( ( R ~=lgr S /\ S ~=lgr T ) -> R ~=lgr T )

Proof

Step Hyp Ref Expression
1 grlicrcl 
 |-  ( R ~=lgr S -> ( R e. _V /\ S e. _V ) )
2 grlicrcl 
 |-  ( S ~=lgr T -> ( S e. _V /\ T e. _V ) )
3 1 2 anim12i 
 |-  ( ( R ~=lgr S /\ S ~=lgr T ) -> ( ( R e. _V /\ S e. _V ) /\ ( S e. _V /\ T e. _V ) ) )
4 eqid 
 |-  ( Vtx ` R ) = ( Vtx ` R )
5 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
6 4 5 grilcbri 
 |-  ( R ~=lgr S -> E. g ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) )
7 eqid 
 |-  ( Vtx ` T ) = ( Vtx ` T )
8 5 7 grilcbri 
 |-  ( S ~=lgr T -> E. h ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) )
9 vex 
 |-  h e. _V
10 vex 
 |-  g e. _V
11 9 10 coex 
 |-  ( h o. g ) e. _V
12 11 a1i 
 |-  ( ( ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) /\ ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) ) -> ( h o. g ) e. _V )
13 f1oco 
 |-  ( ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) ) -> ( h o. g ) : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) )
14 13 ad2ant2r 
 |-  ( ( ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) /\ ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) ) -> ( h o. g ) : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) )
15 f1of 
 |-  ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) -> g : ( Vtx ` R ) --> ( Vtx ` S ) )
16 15 ffvelcdmda 
 |-  ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ r e. ( Vtx ` R ) ) -> ( g ` r ) e. ( Vtx ` S ) )
17 oveq2 
 |-  ( s = ( g ` r ) -> ( S ClNeighbVtx s ) = ( S ClNeighbVtx ( g ` r ) ) )
18 17 oveq2d 
 |-  ( s = ( g ` r ) -> ( S ISubGr ( S ClNeighbVtx s ) ) = ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) )
19 fveq2 
 |-  ( s = ( g ` r ) -> ( h ` s ) = ( h ` ( g ` r ) ) )
20 19 oveq2d 
 |-  ( s = ( g ` r ) -> ( T ClNeighbVtx ( h ` s ) ) = ( T ClNeighbVtx ( h ` ( g ` r ) ) ) )
21 20 oveq2d 
 |-  ( s = ( g ` r ) -> ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) = ( T ISubGr ( T ClNeighbVtx ( h ` ( g ` r ) ) ) ) )
22 18 21 breq12d 
 |-  ( s = ( g ` r ) -> ( ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) <-> ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` ( g ` r ) ) ) ) ) )
23 22 rspcv 
 |-  ( ( g ` r ) e. ( Vtx ` S ) -> ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) -> ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` ( g ` r ) ) ) ) ) )
24 16 23 syl 
 |-  ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ r e. ( Vtx ` R ) ) -> ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) -> ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` ( g ` r ) ) ) ) ) )
25 fvco3 
 |-  ( ( g : ( Vtx ` R ) --> ( Vtx ` S ) /\ r e. ( Vtx ` R ) ) -> ( ( h o. g ) ` r ) = ( h ` ( g ` r ) ) )
26 15 25 sylan 
 |-  ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ r e. ( Vtx ` R ) ) -> ( ( h o. g ) ` r ) = ( h ` ( g ` r ) ) )
27 26 eqcomd 
 |-  ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ r e. ( Vtx ` R ) ) -> ( h ` ( g ` r ) ) = ( ( h o. g ) ` r ) )
28 27 oveq2d 
 |-  ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ r e. ( Vtx ` R ) ) -> ( T ClNeighbVtx ( h ` ( g ` r ) ) ) = ( T ClNeighbVtx ( ( h o. g ) ` r ) ) )
29 28 oveq2d 
 |-  ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ r e. ( Vtx ` R ) ) -> ( T ISubGr ( T ClNeighbVtx ( h ` ( g ` r ) ) ) ) = ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) )
30 29 breq2d 
 |-  ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ r e. ( Vtx ` R ) ) -> ( ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` ( g ` r ) ) ) ) <-> ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
31 24 30 sylibd 
 |-  ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ r e. ( Vtx ` R ) ) -> ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) -> ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
32 31 ex 
 |-  ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) -> ( r e. ( Vtx ` R ) -> ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) -> ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) ) )
33 32 com3r 
 |-  ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) -> ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) -> ( r e. ( Vtx ` R ) -> ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) ) )
34 33 imp31 
 |-  ( ( ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) /\ g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) ) /\ r e. ( Vtx ` R ) ) -> ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) )
35 34 anim1ci 
 |-  ( ( ( ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) /\ g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) ) /\ r e. ( Vtx ` R ) ) /\ ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) -> ( ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) /\ ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
36 grictr 
 |-  ( ( ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) /\ ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) -> ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) )
37 35 36 syl 
 |-  ( ( ( ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) /\ g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) ) /\ r e. ( Vtx ` R ) ) /\ ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) -> ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) )
38 37 ex 
 |-  ( ( ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) /\ g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) ) /\ r e. ( Vtx ` R ) ) -> ( ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) -> ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
39 38 ralimdva 
 |-  ( ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) /\ g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) ) -> ( A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) -> A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
40 39 expimpd 
 |-  ( A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) -> ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) -> A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
41 40 adantl 
 |-  ( ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) -> ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) -> A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
42 41 imp 
 |-  ( ( ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) /\ ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) ) -> A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) )
43 14 42 jca 
 |-  ( ( ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) /\ ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) ) -> ( ( h o. g ) : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
44 f1oeq1 
 |-  ( f = ( h o. g ) -> ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) <-> ( h o. g ) : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) ) )
45 fveq1 
 |-  ( f = ( h o. g ) -> ( f ` r ) = ( ( h o. g ) ` r ) )
46 45 oveq2d 
 |-  ( f = ( h o. g ) -> ( T ClNeighbVtx ( f ` r ) ) = ( T ClNeighbVtx ( ( h o. g ) ` r ) ) )
47 46 oveq2d 
 |-  ( f = ( h o. g ) -> ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) = ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) )
48 47 breq2d 
 |-  ( f = ( h o. g ) -> ( ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) <-> ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
49 48 ralbidv 
 |-  ( f = ( h o. g ) -> ( A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) <-> A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) )
50 44 49 anbi12d 
 |-  ( f = ( h o. g ) -> ( ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) <-> ( ( h o. g ) : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( ( h o. g ) ` r ) ) ) ) ) )
51 12 43 50 spcedv 
 |-  ( ( ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) /\ ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) ) -> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) )
52 51 ex 
 |-  ( ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) -> ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) -> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) ) )
53 52 exlimiv 
 |-  ( E. h ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) -> ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) -> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) ) )
54 53 com12 
 |-  ( ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) -> ( E. h ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) -> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) ) )
55 54 exlimiv 
 |-  ( E. g ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) -> ( E. h ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) -> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) ) )
56 55 imp 
 |-  ( ( E. g ( g : ( Vtx ` R ) -1-1-onto-> ( Vtx ` S ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( g ` r ) ) ) ) /\ E. h ( h : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ A. s e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx s ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( h ` s ) ) ) ) ) -> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) )
57 6 8 56 syl2an 
 |-  ( ( R ~=lgr S /\ S ~=lgr T ) -> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) )
58 57 adantr 
 |-  ( ( ( R ~=lgr S /\ S ~=lgr T ) /\ ( ( R e. _V /\ S e. _V ) /\ ( S e. _V /\ T e. _V ) ) ) -> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) )
59 4 7 dfgrlic2 
 |-  ( ( R e. _V /\ T e. _V ) -> ( R ~=lgr T <-> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) ) )
60 59 ad2ant2rl 
 |-  ( ( ( R e. _V /\ S e. _V ) /\ ( S e. _V /\ T e. _V ) ) -> ( R ~=lgr T <-> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) ) )
61 60 adantl 
 |-  ( ( ( R ~=lgr S /\ S ~=lgr T ) /\ ( ( R e. _V /\ S e. _V ) /\ ( S e. _V /\ T e. _V ) ) ) -> ( R ~=lgr T <-> E. f ( f : ( Vtx ` R ) -1-1-onto-> ( Vtx ` T ) /\ A. r e. ( Vtx ` R ) ( R ISubGr ( R ClNeighbVtx r ) ) ~=gr ( T ISubGr ( T ClNeighbVtx ( f ` r ) ) ) ) ) )
62 58 61 mpbird 
 |-  ( ( ( R ~=lgr S /\ S ~=lgr T ) /\ ( ( R e. _V /\ S e. _V ) /\ ( S e. _V /\ T e. _V ) ) ) -> R ~=lgr T )
63 3 62 mpdan 
 |-  ( ( R ~=lgr S /\ S ~=lgr T ) -> R ~=lgr T )