Metamath Proof Explorer

Theorem grimco

Description: The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025)

Ref Expression
Assertion grimco 
|- ( ( F e. ( T GraphIso U ) /\ G e. ( S GraphIso T ) ) -> ( F o. G ) e. ( S GraphIso U ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` T ) = ( Vtx ` T )
2 eqid 
 |-  ( Vtx ` U ) = ( Vtx ` U )
3 eqid 
 |-  ( iEdg ` T ) = ( iEdg ` T )
4 eqid 
 |-  ( iEdg ` U ) = ( iEdg ` U )
5 1 2 3 4 grimprop 
 |-  ( F e. ( T GraphIso U ) -> ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) )
6 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
7 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
8 6 1 7 3 grimprop 
 |-  ( G e. ( S GraphIso T ) -> ( G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. g ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) ) )
9 f1oco 
 |-  ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) -> ( F o. G ) : ( Vtx ` S ) -1-1-onto-> ( Vtx ` U ) )
10 9 ad2ant2r 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) /\ ( G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. g ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) ) ) -> ( F o. G ) : ( Vtx ` S ) -1-1-onto-> ( Vtx ` U ) )
11 vex 
 |-  f e. _V
12 vex 
 |-  g e. _V
13 11 12 coex 
 |-  ( f o. g ) e. _V
14 13 a1i 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) ) -> ( f o. g ) e. _V )
15 f1oco 
 |-  ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) -> ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) )
16 15 a1d 
 |-  ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) -> ( A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) -> ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) ) )
17 16 expcom 
 |-  ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) -> ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) -> ( A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) -> ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) ) ) )
18 17 impd 
 |-  ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) ) )
19 18 adantr 
 |-  ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) ) )
20 19 imp 
 |-  ( ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) -> ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) )
21 20 adantl 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) ) -> ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) )
22 2fveq3 
 |-  ( y = i -> ( ( iEdg ` T ) ` ( g ` y ) ) = ( ( iEdg ` T ) ` ( g ` i ) ) )
23 fveq2 
 |-  ( y = i -> ( ( iEdg ` S ) ` y ) = ( ( iEdg ` S ) ` i ) )
24 23 imaeq2d 
 |-  ( y = i -> ( G " ( ( iEdg ` S ) ` y ) ) = ( G " ( ( iEdg ` S ) ` i ) ) )
25 22 24 eqeq12d 
 |-  ( y = i -> ( ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) <-> ( ( iEdg ` T ) ` ( g ` i ) ) = ( G " ( ( iEdg ` S ) ` i ) ) ) )
26 25 rspcv 
 |-  ( i e. dom ( iEdg ` S ) -> ( A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) -> ( ( iEdg ` T ) ` ( g ` i ) ) = ( G " ( ( iEdg ` S ) ` i ) ) ) )
27 26 adantl 
 |-  ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) -> ( A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) -> ( ( iEdg ` T ) ` ( g ` i ) ) = ( G " ( ( iEdg ` S ) ` i ) ) ) )
28 27 adantr 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) -> ( A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) -> ( ( iEdg ` T ) ` ( g ` i ) ) = ( G " ( ( iEdg ` S ) ` i ) ) ) )
29 f1of 
 |-  ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) -> g : dom ( iEdg ` S ) --> dom ( iEdg ` T ) )
30 29 adantl 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) -> g : dom ( iEdg ` S ) --> dom ( iEdg ` T ) )
31 30 ffvelcdmda 
 |-  ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) -> ( g ` i ) e. dom ( iEdg ` T ) )
32 31 adantr 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) -> ( g ` i ) e. dom ( iEdg ` T ) )
33 2fveq3 
 |-  ( x = ( g ` i ) -> ( ( iEdg ` U ) ` ( f ` x ) ) = ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) )
34 fveq2 
 |-  ( x = ( g ` i ) -> ( ( iEdg ` T ) ` x ) = ( ( iEdg ` T ) ` ( g ` i ) ) )
35 34 imaeq2d 
 |-  ( x = ( g ` i ) -> ( F " ( ( iEdg ` T ) ` x ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) )
36 33 35 eqeq12d 
 |-  ( x = ( g ` i ) -> ( ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) <-> ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) ) )
37 36 rspcv 
 |-  ( ( g ` i ) e. dom ( iEdg ` T ) -> ( A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) -> ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) ) )
38 32 37 syl 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) -> ( A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) -> ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) ) )
39 30 adantr 
 |-  ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) -> g : dom ( iEdg ` S ) --> dom ( iEdg ` T ) )
40 39 adantr 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) -> g : dom ( iEdg ` S ) --> dom ( iEdg ` T ) )
41 simpr 
 |-  ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) -> i e. dom ( iEdg ` S ) )
42 41 adantr 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) -> i e. dom ( iEdg ` S ) )
43 40 42 fvco3d 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) -> ( ( f o. g ) ` i ) = ( f ` ( g ` i ) ) )
44 43 adantr 
 |-  ( ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) /\ ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) ) -> ( ( f o. g ) ` i ) = ( f ` ( g ` i ) ) )
45 44 fveq2d 
 |-  ( ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) /\ ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) )
46 simpr 
 |-  ( ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) /\ ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) ) -> ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) )
47 45 46 eqtrd 
 |-  ( ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) /\ ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) )
48 47 ex 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) -> ( ( ( iEdg ` U ) ` ( f ` ( g ` i ) ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) ) )
49 38 48 syld 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) ) -> ( A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) ) )
50 49 impr 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) )
51 imaeq2 
 |-  ( ( ( iEdg ` T ) ` ( g ` i ) ) = ( G " ( ( iEdg ` S ) ` i ) ) -> ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) = ( F " ( G " ( ( iEdg ` S ) ` i ) ) ) )
52 imaco 
 |-  ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) = ( F " ( G " ( ( iEdg ` S ) ` i ) ) )
53 51 52 eqtr4di 
 |-  ( ( ( iEdg ` T ) ` ( g ` i ) ) = ( G " ( ( iEdg ` S ) ` i ) ) -> ( F " ( ( iEdg ` T ) ` ( g ` i ) ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) )
54 50 53 sylan9eq 
 |-  ( ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) /\ ( ( iEdg ` T ) ` ( g ` i ) ) = ( G " ( ( iEdg ` S ) ` i ) ) ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) )
55 54 ex 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) -> ( ( ( iEdg ` T ) ` ( g ` i ) ) = ( G " ( ( iEdg ` S ) ` i ) ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) )
56 28 55 syld 
 |-  ( ( ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ i e. dom ( iEdg ` S ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) -> ( A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) )
57 56 exp31 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) -> ( i e. dom ( iEdg ` S ) -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> ( A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
58 57 com24 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) -> ( A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> ( i e. dom ( iEdg ` S ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
59 58 expimpd 
 |-  ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) -> ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> ( i e. dom ( iEdg ` S ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
60 59 imp32 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) ) -> ( i e. dom ( iEdg ` S ) -> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) )
61 60 ralrimiv 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) ) -> A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) )
62 21 61 jca 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) ) -> ( ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) )
63 f1oeq1 
 |-  ( j = ( f o. g ) -> ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) <-> ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) ) )
64 fveq1 
 |-  ( j = ( f o. g ) -> ( j ` i ) = ( ( f o. g ) ` i ) )
65 64 fveqeq2d 
 |-  ( j = ( f o. g ) -> ( ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) <-> ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) )
66 65 ralbidv 
 |-  ( j = ( f o. g ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) <-> A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) )
67 63 66 anbi12d 
 |-  ( j = ( f o. g ) -> ( ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) <-> ( ( f o. g ) : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( ( f o. g ) ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) )
68 14 62 67 spcedv 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) /\ ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) ) -> E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) )
69 68 exp32 
 |-  ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) -> ( ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
70 69 exlimdv 
 |-  ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) -> ( E. g ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
71 70 expimpd 
 |-  ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) -> ( ( G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. g ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) ) -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
72 71 com23 
 |-  ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> ( ( G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. g ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) ) -> E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
73 72 exlimdv 
 |-  ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) -> ( E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) -> ( ( G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. g ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) ) -> E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
74 73 imp31 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) /\ ( G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. g ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) ) ) -> E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) )
75 10 74 jca 
 |-  ( ( ( F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` U ) /\ E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` U ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` U ) ` ( f ` x ) ) = ( F " ( ( iEdg ` T ) ` x ) ) ) ) /\ ( G : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. g ( g : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. y e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( g ` y ) ) = ( G " ( ( iEdg ` S ) ` y ) ) ) ) ) -> ( ( F o. G ) : ( Vtx ` S ) -1-1-onto-> ( Vtx ` U ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) )
76 5 8 75 syl2an 
 |-  ( ( F e. ( T GraphIso U ) /\ G e. ( S GraphIso T ) ) -> ( ( F o. G ) : ( Vtx ` S ) -1-1-onto-> ( Vtx ` U ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) )
77 grimdmrel 
 |-  Rel dom GraphIso
78 77 ovrcl 
 |-  ( G e. ( S GraphIso T ) -> ( S e. _V /\ T e. _V ) )
79 78 simpld 
 |-  ( G e. ( S GraphIso T ) -> S e. _V )
80 79 adantl 
 |-  ( ( F e. ( T GraphIso U ) /\ G e. ( S GraphIso T ) ) -> S e. _V )
81 77 ovrcl 
 |-  ( F e. ( T GraphIso U ) -> ( T e. _V /\ U e. _V ) )
82 81 simprd 
 |-  ( F e. ( T GraphIso U ) -> U e. _V )
83 82 adantr 
 |-  ( ( F e. ( T GraphIso U ) /\ G e. ( S GraphIso T ) ) -> U e. _V )
84 coexg 
 |-  ( ( F e. ( T GraphIso U ) /\ G e. ( S GraphIso T ) ) -> ( F o. G ) e. _V )
85 6 2 7 4 isgrim 
 |-  ( ( S e. _V /\ U e. _V /\ ( F o. G ) e. _V ) -> ( ( F o. G ) e. ( S GraphIso U ) <-> ( ( F o. G ) : ( Vtx ` S ) -1-1-onto-> ( Vtx ` U ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
86 80 83 84 85 syl3anc 
 |-  ( ( F e. ( T GraphIso U ) /\ G e. ( S GraphIso T ) ) -> ( ( F o. G ) e. ( S GraphIso U ) <-> ( ( F o. G ) : ( Vtx ` S ) -1-1-onto-> ( Vtx ` U ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` U ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` U ) ` ( j ` i ) ) = ( ( F o. G ) " ( ( iEdg ` S ) ` i ) ) ) ) ) )
87 76 86 mpbird 
 |-  ( ( F e. ( T GraphIso U ) /\ G e. ( S GraphIso T ) ) -> ( F o. G ) e. ( S GraphIso U ) )