Metamath Proof Explorer

Theorem isomgr

Description: The isomorphy relation for two graphs. (Contributed by AV, 11-Nov-2022)

Ref Expression
Hypotheses isomgr.v 
|- V = ( Vtx ` A )
isomgr.w 
|- W = ( Vtx ` B )
isomgr.i 
|- I = ( iEdg ` A )
isomgr.j 
|- J = ( iEdg ` B )
Assertion isomgr 
|- ( ( A e. X /\ B e. Y ) -> ( A IsomGr 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 isomgr.v 
 |-  V = ( Vtx ` A )
2 isomgr.w 
 |-  W = ( Vtx ` B )
3 isomgr.i 
 |-  I = ( iEdg ` A )
4 isomgr.j 
 |-  J = ( iEdg ` B )
5 eqidd 
 |-  ( ( x = A /\ y = B ) -> f = f )
6 fveq2 
 |-  ( x = A -> ( Vtx ` x ) = ( Vtx ` A ) )
7 6 adantr 
 |-  ( ( x = A /\ y = B ) -> ( Vtx ` x ) = ( Vtx ` A ) )
8 7 1 eqtr4di 
 |-  ( ( x = A /\ y = B ) -> ( Vtx ` x ) = V )
9 fveq2 
 |-  ( y = B -> ( Vtx ` y ) = ( Vtx ` B ) )
10 9 adantl 
 |-  ( ( x = A /\ y = B ) -> ( Vtx ` y ) = ( Vtx ` B ) )
11 10 2 eqtr4di 
 |-  ( ( x = A /\ y = B ) -> ( Vtx ` y ) = W )
12 5 8 11 f1oeq123d 
 |-  ( ( x = A /\ y = B ) -> ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) <-> f : V -1-1-onto-> W ) )
13 eqidd 
 |-  ( ( x = A /\ y = B ) -> g = g )
14 fveq2 
 |-  ( x = A -> ( iEdg ` x ) = ( iEdg ` A ) )
15 14 adantr 
 |-  ( ( x = A /\ y = B ) -> ( iEdg ` x ) = ( iEdg ` A ) )
16 15 3 eqtr4di 
 |-  ( ( x = A /\ y = B ) -> ( iEdg ` x ) = I )
17 16 dmeqd 
 |-  ( ( x = A /\ y = B ) -> dom ( iEdg ` x ) = dom I )
18 fveq2 
 |-  ( y = B -> ( iEdg ` y ) = ( iEdg ` B ) )
19 18 adantl 
 |-  ( ( x = A /\ y = B ) -> ( iEdg ` y ) = ( iEdg ` B ) )
20 19 4 eqtr4di 
 |-  ( ( x = A /\ y = B ) -> ( iEdg ` y ) = J )
21 20 dmeqd 
 |-  ( ( x = A /\ y = B ) -> dom ( iEdg ` y ) = dom J )
22 13 17 21 f1oeq123d 
 |-  ( ( x = A /\ y = B ) -> ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) <-> g : dom I -1-1-onto-> dom J ) )
23 16 fveq1d 
 |-  ( ( x = A /\ y = B ) -> ( ( iEdg ` x ) ` i ) = ( I ` i ) )
24 23 imaeq2d 
 |-  ( ( x = A /\ y = B ) -> ( f " ( ( iEdg ` x ) ` i ) ) = ( f " ( I ` i ) ) )
25 20 fveq1d 
 |-  ( ( x = A /\ y = B ) -> ( ( iEdg ` y ) ` ( g ` i ) ) = ( J ` ( g ` i ) ) )
26 24 25 eqeq12d 
 |-  ( ( x = A /\ y = B ) -> ( ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) <-> ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) )
27 17 26 raleqbidv 
 |-  ( ( x = A /\ y = B ) -> ( A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) <-> A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) )
28 22 27 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) <-> ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )
29 28 exbidv 
 |-  ( ( x = A /\ y = B ) -> ( E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) <-> E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )
30 12 29 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` 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 ) ) ) ) ) )
31 30 exbidv 
 |-  ( ( x = A /\ y = B ) -> ( E. f ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) ) <-> 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 ) ) ) ) ) )
32 df-isomgr 
 |-  IsomGr = { <. x , y >. | E. f ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) ) }
33 31 32 brabga 
 |-  ( ( A e. X /\ B e. Y ) -> ( A IsomGr 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 ) ) ) ) ) )