Metamath Proof Explorer

Theorem grimprop

Description: Properties of an isomorphism of graphs. (Contributed by AV, 29-Apr-2025)

Ref Expression
Hypotheses grimprop.v 
|- V = ( Vtx ` G )
grimprop.w 
|- W = ( Vtx ` H )
grimprop.e 
|- E = ( iEdg ` G )
grimprop.d 
|- D = ( iEdg ` H )
Assertion grimprop 
|- ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> W /\ E. j ( j : dom E -1-1-onto-> dom D /\ A. i e. dom E ( D ` ( j ` i ) ) = ( F " ( E ` i ) ) ) ) )

Proof

Step Hyp Ref Expression
1 grimprop.v 
 |-  V = ( Vtx ` G )
2 grimprop.w 
 |-  W = ( Vtx ` H )
3 grimprop.e 
 |-  E = ( iEdg ` G )
4 grimprop.d 
 |-  D = ( iEdg ` H )
5 grimdmrel 
 |-  Rel dom GraphIso
6 5 ovrcl 
 |-  ( F e. ( G GraphIso H ) -> ( G e. _V /\ H e. _V ) )
7 6 simpld 
 |-  ( F e. ( G GraphIso H ) -> G e. _V )
8 6 simprd 
 |-  ( F e. ( G GraphIso H ) -> H e. _V )
9 id 
 |-  ( F e. ( G GraphIso H ) -> F e. ( G GraphIso H ) )
10 7 8 9 3jca 
 |-  ( F e. ( G GraphIso H ) -> ( G e. _V /\ H e. _V /\ F e. ( G GraphIso H ) ) )
11 1 2 3 4 isgrim 
 |-  ( ( G e. _V /\ H e. _V /\ F e. ( G GraphIso H ) ) -> ( F e. ( G GraphIso H ) <-> ( F : V -1-1-onto-> W /\ E. j ( j : dom E -1-1-onto-> dom D /\ A. i e. dom E ( D ` ( j ` i ) ) = ( F " ( E ` i ) ) ) ) ) )
12 11 biimpd 
 |-  ( ( G e. _V /\ H e. _V /\ F e. ( G GraphIso H ) ) -> ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> W /\ E. j ( j : dom E -1-1-onto-> dom D /\ A. i e. dom E ( D ` ( j ` i ) ) = ( F " ( E ` i ) ) ) ) ) )
13 10 12 mpcom 
 |-  ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> W /\ E. j ( j : dom E -1-1-onto-> dom D /\ A. i e. dom E ( D ` ( j ` i ) ) = ( F " ( E ` i ) ) ) ) )