| Step |
Hyp |
Ref |
Expression |
| 1 |
|
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 ) ) ) ) } ) |
| 2 |
|
f1of |
|- ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) -> f : ( Vtx ` g ) --> ( Vtx ` h ) ) |
| 3 |
|
fvex |
|- ( Vtx ` h ) e. _V |
| 4 |
|
fvex |
|- ( Vtx ` g ) e. _V |
| 5 |
3 4
|
elmap |
|- ( f e. ( ( Vtx ` h ) ^m ( Vtx ` g ) ) <-> f : ( Vtx ` g ) --> ( Vtx ` h ) ) |
| 6 |
2 5
|
sylibr |
|- ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) -> f e. ( ( Vtx ` h ) ^m ( Vtx ` g ) ) ) |
| 7 |
6
|
adantr |
|- ( ( 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 e. ( ( Vtx ` h ) ^m ( Vtx ` g ) ) ) |
| 8 |
|
ovex |
|- ( ( Vtx ` h ) ^m ( Vtx ` g ) ) e. _V |
| 9 |
7 8
|
abex |
|- { 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 ) ) ) ) } e. _V |
| 10 |
1 9
|
fnmpoi |
|- GraphIso Fn ( _V X. _V ) |