Description: Implications of two graphs being isomorphic. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025) (Proof shortened by AV, 12-Jun-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 | gricbri | |- ( 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 ) ) ) ) ) |
| 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 | gricrcl | |- ( A ~=gr B -> ( A e. _V /\ B e. _V ) ) |
|
| 6 | 1 2 3 4 | dfgric2 | |- ( ( A e. _V /\ B e. _V ) -> ( 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 ) ) ) ) ) ) |
| 7 | 5 6 | syl | |- ( A ~=gr B -> ( 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 ) ) ) ) ) ) |
| 8 | 7 | ibi | |- ( 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 ) ) ) ) ) |