Metamath Proof Explorer

Theorem isgrim

Description: An isomorphism of graphs is a bijection between their vertices that preserves adjacency. (Contributed by AV, 19-Apr-2025)

Ref Expression
Hypotheses isgrim.v 
|- V = ( Vtx ` G )
isgrim.w 
|- W = ( Vtx ` H )
isgrim.e 
|- E = ( iEdg ` G )
isgrim.d 
|- D = ( iEdg ` H )
Assertion isgrim 
|- ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( 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 isgrim.v 
 |-  V = ( Vtx ` G )
2 isgrim.w 
 |-  W = ( Vtx ` H )
3 isgrim.e 
 |-  E = ( iEdg ` G )
4 isgrim.d 
 |-  D = ( iEdg ` H )
5 df-grim 
 |-  GraphIso = ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) ) } )
6 elex 
 |-  ( G e. X -> G e. _V )
7 6 3ad2ant1 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> G e. _V )
8 elex 
 |-  ( H e. Y -> H e. _V )
9 8 3ad2ant2 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> H e. _V )
10 f1of 
 |-  ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> f : ( Vtx ` G ) --> ( Vtx ` H ) )
11 fvex 
 |-  ( Vtx ` H ) e. _V
12 fvex 
 |-  ( Vtx ` G ) e. _V
13 11 12 elmap 
 |-  ( f e. ( ( Vtx ` H ) ^m ( Vtx ` G ) ) <-> f : ( Vtx ` G ) --> ( Vtx ` H ) )
14 10 13 sylibr 
 |-  ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> f e. ( ( Vtx ` H ) ^m ( Vtx ` G ) ) )
15 14 adantr 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) -> f e. ( ( Vtx ` H ) ^m ( Vtx ` G ) ) )
16 ovex 
 |-  ( ( Vtx ` H ) ^m ( Vtx ` G ) ) e. _V
17 15 16 abex 
 |-  { f | ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) } e. _V
18 17 a1i 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> { f | ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) } e. _V )
19 eqidd 
 |-  ( ( g = G /\ h = H ) -> f = f )
20 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
21 20 adantr 
 |-  ( ( g = G /\ h = H ) -> ( Vtx ` g ) = ( Vtx ` G ) )
22 fveq2 
 |-  ( h = H -> ( Vtx ` h ) = ( Vtx ` H ) )
23 22 adantl 
 |-  ( ( g = G /\ h = H ) -> ( Vtx ` h ) = ( Vtx ` H ) )
24 19 21 23 f1oeq123d 
 |-  ( ( g = G /\ h = H ) -> ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) <-> f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) )
25 fvexd 
 |-  ( ( g = G /\ h = H ) -> ( iEdg ` g ) e. _V )
26 fveq2 
 |-  ( g = G -> ( iEdg ` g ) = ( iEdg ` G ) )
27 26 adantr 
 |-  ( ( g = G /\ h = H ) -> ( iEdg ` g ) = ( iEdg ` G ) )
28 fvexd 
 |-  ( ( ( g = G /\ h = H ) /\ e = ( iEdg ` G ) ) -> ( iEdg ` h ) e. _V )
29 fveq2 
 |-  ( h = H -> ( iEdg ` h ) = ( iEdg ` H ) )
30 29 adantl 
 |-  ( ( g = G /\ h = H ) -> ( iEdg ` h ) = ( iEdg ` H ) )
31 30 adantr 
 |-  ( ( ( g = G /\ h = H ) /\ e = ( iEdg ` G ) ) -> ( iEdg ` h ) = ( iEdg ` H ) )
32 eqidd 
 |-  ( ( e = ( iEdg ` G ) /\ d = ( iEdg ` H ) ) -> j = j )
33 dmeq 
 |-  ( e = ( iEdg ` G ) -> dom e = dom ( iEdg ` G ) )
34 33 adantr 
 |-  ( ( e = ( iEdg ` G ) /\ d = ( iEdg ` H ) ) -> dom e = dom ( iEdg ` G ) )
35 dmeq 
 |-  ( d = ( iEdg ` H ) -> dom d = dom ( iEdg ` H ) )
36 35 adantl 
 |-  ( ( e = ( iEdg ` G ) /\ d = ( iEdg ` H ) ) -> dom d = dom ( iEdg ` H ) )
37 32 34 36 f1oeq123d 
 |-  ( ( e = ( iEdg ` G ) /\ d = ( iEdg ` H ) ) -> ( j : dom e -1-1-onto-> dom d <-> j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) )
38 fveq1 
 |-  ( d = ( iEdg ` H ) -> ( d ` ( j ` i ) ) = ( ( iEdg ` H ) ` ( j ` i ) ) )
39 fveq1 
 |-  ( e = ( iEdg ` G ) -> ( e ` i ) = ( ( iEdg ` G ) ` i ) )
40 39 imaeq2d 
 |-  ( e = ( iEdg ` G ) -> ( f " ( e ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) )
41 38 40 eqeqan12rd 
 |-  ( ( e = ( iEdg ` G ) /\ d = ( iEdg ` H ) ) -> ( ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) <-> ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) )
42 34 41 raleqbidv 
 |-  ( ( e = ( iEdg ` G ) /\ d = ( iEdg ` H ) ) -> ( A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) <-> A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) )
43 37 42 anbi12d 
 |-  ( ( e = ( iEdg ` G ) /\ d = ( iEdg ` H ) ) -> ( ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) <-> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) )
44 43 adantll 
 |-  ( ( ( ( g = G /\ h = H ) /\ e = ( iEdg ` G ) ) /\ d = ( iEdg ` H ) ) -> ( ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) <-> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) )
45 28 31 44 sbcied2 
 |-  ( ( ( g = G /\ h = H ) /\ e = ( iEdg ` G ) ) -> ( [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) <-> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) )
46 25 27 45 sbcied2 
 |-  ( ( g = G /\ h = H ) -> ( [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) <-> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) )
47 biidd 
 |-  ( ( g = G /\ h = H ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) <-> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) )
48 46 47 bitrd 
 |-  ( ( g = G /\ h = H ) -> ( [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) <-> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) )
49 48 exbidv 
 |-  ( ( g = G /\ h = H ) -> ( E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) <-> E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) )
50 24 49 anbi12d 
 |-  ( ( g = G /\ h = H ) -> ( ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) ) <-> ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) ) )
51 50 abbidv 
 |-  ( ( g = G /\ h = H ) -> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) ) } = { f | ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) } )
52 5 7 9 18 51 elovmpod 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( F e. ( G GraphIso H ) <-> F e. { f | ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) } ) )
53 id 
 |-  ( f = F -> f = F )
54 1 eqcomi 
 |-  ( Vtx ` G ) = V
55 54 a1i 
 |-  ( f = F -> ( Vtx ` G ) = V )
56 2 eqcomi 
 |-  ( Vtx ` H ) = W
57 56 a1i 
 |-  ( f = F -> ( Vtx ` H ) = W )
58 53 55 57 f1oeq123d 
 |-  ( f = F -> ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) <-> F : V -1-1-onto-> W ) )
59 eqidd 
 |-  ( f = F -> j = j )
60 3 eqcomi 
 |-  ( iEdg ` G ) = E
61 60 dmeqi 
 |-  dom ( iEdg ` G ) = dom E
62 61 a1i 
 |-  ( f = F -> dom ( iEdg ` G ) = dom E )
63 4 eqcomi 
 |-  ( iEdg ` H ) = D
64 63 dmeqi 
 |-  dom ( iEdg ` H ) = dom D
65 64 a1i 
 |-  ( f = F -> dom ( iEdg ` H ) = dom D )
66 59 62 65 f1oeq123d 
 |-  ( f = F -> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) <-> j : dom E -1-1-onto-> dom D ) )
67 63 fveq1i 
 |-  ( ( iEdg ` H ) ` ( j ` i ) ) = ( D ` ( j ` i ) )
68 67 a1i 
 |-  ( f = F -> ( ( iEdg ` H ) ` ( j ` i ) ) = ( D ` ( j ` i ) ) )
69 60 fveq1i 
 |-  ( ( iEdg ` G ) ` i ) = ( E ` i )
70 69 a1i 
 |-  ( f = F -> ( ( iEdg ` G ) ` i ) = ( E ` i ) )
71 53 70 imaeq12d 
 |-  ( f = F -> ( f " ( ( iEdg ` G ) ` i ) ) = ( F " ( E ` i ) ) )
72 68 71 eqeq12d 
 |-  ( f = F -> ( ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) <-> ( D ` ( j ` i ) ) = ( F " ( E ` i ) ) ) )
73 62 72 raleqbidv 
 |-  ( f = F -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) <-> A. i e. dom E ( D ` ( j ` i ) ) = ( F " ( E ` i ) ) ) )
74 66 73 anbi12d 
 |-  ( f = F -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) <-> ( j : dom E -1-1-onto-> dom D /\ A. i e. dom E ( D ` ( j ` i ) ) = ( F " ( E ` i ) ) ) ) )
75 74 exbidv 
 |-  ( f = F -> ( E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) <-> E. j ( j : dom E -1-1-onto-> dom D /\ A. i e. dom E ( D ` ( j ` i ) ) = ( F " ( E ` i ) ) ) ) )
76 58 75 anbi12d 
 |-  ( f = F -> ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) <-> ( 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 ) ) ) ) ) )
77 76 elabg 
 |-  ( F e. Z -> ( F e. { f | ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) } <-> ( 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 ) ) ) ) ) )
78 77 3ad2ant3 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( F e. { f | ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( f " ( ( iEdg ` G ) ` i ) ) ) ) } <-> ( 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 ) ) ) ) ) )
79 52 78 bitrd 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( 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 ) ) ) ) ) )