Metamath Proof Explorer

Theorem dfgric2

Description: Alternate, explicit definition of the "is isomorphic to" relation for two graphs. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025)

Ref Expression
Hypotheses dfgric2.v 
|- V = ( Vtx ` A )
dfgric2.w 
|- W = ( Vtx ` B )
dfgric2.i 
|- I = ( iEdg ` A )
dfgric2.j 
|- J = ( iEdg ` B )
Assertion dfgric2 
|- ( ( A e. X /\ B e. Y ) -> ( A ~=gr B <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfgric2.v 
 |-  V = ( Vtx ` A )
2 dfgric2.w 
 |-  W = ( Vtx ` B )
3 dfgric2.i 
 |-  I = ( iEdg ` A )
4 dfgric2.j 
 |-  J = ( iEdg ` B )
5 brgric 
 |-  ( A ~=gr B <-> ( A GraphIso B ) =/= (/) )
6 n0 
 |-  ( ( A GraphIso B ) =/= (/) <-> E. f f e. ( A GraphIso B ) )
7 5 6 bitri 
 |-  ( A ~=gr B <-> E. f f e. ( A GraphIso B ) )
8 vex 
 |-  f e. _V
9 1 2 3 4 isgrim 
 |-  ( ( A e. X /\ B e. Y /\ f e. _V ) -> ( f e. ( A GraphIso B ) <-> ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( J ` ( g ` i ) ) = ( f " ( I ` i ) ) ) ) ) )
10 eqcom 
 |-  ( ( J ` ( g ` i ) ) = ( f " ( I ` i ) ) <-> ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) )
11 10 ralbii 
 |-  ( A. i e. dom I ( J ` ( g ` i ) ) = ( f " ( I ` i ) ) <-> A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) )
12 11 anbi2i 
 |-  ( ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( J ` ( g ` i ) ) = ( f " ( I ` i ) ) ) <-> ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) )
13 12 exbii 
 |-  ( E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( J ` ( g ` i ) ) = ( f " ( I ` i ) ) ) <-> E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) )
14 13 anbi2i 
 |-  ( ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( J ` ( g ` i ) ) = ( f " ( I ` i ) ) ) ) <-> ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )
15 9 14 bitrdi 
 |-  ( ( A e. X /\ B e. Y /\ f e. _V ) -> ( f e. ( A GraphIso B ) <-> ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
16 8 15 mp3an3 
 |-  ( ( A e. X /\ B e. Y ) -> ( f e. ( A GraphIso B ) <-> ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
17 16 exbidv 
 |-  ( ( A e. X /\ B e. Y ) -> ( E. f f e. ( A GraphIso B ) <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
18 7 17 bitrid 
 |-  ( ( A e. X /\ B e. Y ) -> ( A ~=gr B <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )