Metamath Proof Explorer

Theorem grimidvtxedg

Description: The identity relation restricted to the set of vertices of a graph is a graph isomorphism between the graph and a graph with the same vertices and edges. (Contributed by AV, 4-May-2025)

Ref Expression
Hypotheses grimidvtxsdg.g 
|- ( ph -> G e. UHGraph )
grimidvtxsdg.h 
|- ( ph -> H e. V )
grimidvtxsdg.v 
|- ( ph -> ( Vtx ` G ) = ( Vtx ` H ) )
grimidvtxsdg.e 
|- ( ph -> ( iEdg ` G ) = ( iEdg ` H ) )
Assertion grimidvtxedg 
|- ( ph -> ( _I |` ( Vtx ` G ) ) e. ( G GraphIso H ) )

Proof

Step Hyp Ref Expression
1 grimidvtxsdg.g 
 |-  ( ph -> G e. UHGraph )
2 grimidvtxsdg.h 
 |-  ( ph -> H e. V )
3 grimidvtxsdg.v 
 |-  ( ph -> ( Vtx ` G ) = ( Vtx ` H ) )
4 grimidvtxsdg.e 
 |-  ( ph -> ( iEdg ` G ) = ( iEdg ` H ) )
5 f1oi 
 |-  ( _I |` ( Vtx ` G ) ) : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G )
6 3 f1oeq3d 
 |-  ( ph -> ( ( _I |` ( Vtx ` G ) ) : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G ) <-> ( _I |` ( Vtx ` G ) ) : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) )
7 5 6 mpbii 
 |-  ( ph -> ( _I |` ( Vtx ` G ) ) : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) )
8 funi 
 |-  Fun _I
9 fvex 
 |-  ( iEdg ` G ) e. _V
10 9 dmex 
 |-  dom ( iEdg ` G ) e. _V
11 resfunexg 
 |-  ( ( Fun _I /\ dom ( iEdg ` G ) e. _V ) -> ( _I |` dom ( iEdg ` G ) ) e. _V )
12 8 10 11 mp2an 
 |-  ( _I |` dom ( iEdg ` G ) ) e. _V
13 12 a1i 
 |-  ( ph -> ( _I |` dom ( iEdg ` G ) ) e. _V )
14 f1oi 
 |-  ( _I |` dom ( iEdg ` G ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` G )
15 4 dmeqd 
 |-  ( ph -> dom ( iEdg ` G ) = dom ( iEdg ` H ) )
16 15 f1oeq3d 
 |-  ( ph -> ( ( _I |` dom ( iEdg ` G ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` G ) <-> ( _I |` dom ( iEdg ` G ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) )
17 14 16 mpbii 
 |-  ( ph -> ( _I |` dom ( iEdg ` G ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) )
18 fvresi 
 |-  ( i e. dom ( iEdg ` G ) -> ( ( _I |` dom ( iEdg ` G ) ) ` i ) = i )
19 18 adantl 
 |-  ( ( ph /\ i e. dom ( iEdg ` G ) ) -> ( ( _I |` dom ( iEdg ` G ) ) ` i ) = i )
20 19 fveq2d 
 |-  ( ( ph /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) = ( ( iEdg ` G ) ` i ) )
21 4 eqcomd 
 |-  ( ph -> ( iEdg ` H ) = ( iEdg ` G ) )
22 21 fveq1d 
 |-  ( ph -> ( ( iEdg ` H ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) = ( ( iEdg ` G ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) )
23 22 adantr 
 |-  ( ( ph /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` H ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) = ( ( iEdg ` G ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) )
24 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
25 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
26 24 25 uhgrss 
 |-  ( ( G e. UHGraph /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` i ) C_ ( Vtx ` G ) )
27 1 26 sylan 
 |-  ( ( ph /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` i ) C_ ( Vtx ` G ) )
28 resiima 
 |-  ( ( ( iEdg ` G ) ` i ) C_ ( Vtx ` G ) -> ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` G ) ` i ) )
29 27 28 syl 
 |-  ( ( ph /\ i e. dom ( iEdg ` G ) ) -> ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` G ) ` i ) )
30 20 23 29 3eqtr4d 
 |-  ( ( ph /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` H ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) )
31 30 ralrimiva 
 |-  ( ph -> A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) )
32 17 31 jca 
 |-  ( ph -> ( ( _I |` dom ( iEdg ` G ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) ) )
33 f1oeq1 
 |-  ( j = ( _I |` dom ( iEdg ` G ) ) -> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) <-> ( _I |` dom ( iEdg ` G ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) )
34 fveq1 
 |-  ( j = ( _I |` dom ( iEdg ` G ) ) -> ( j ` i ) = ( ( _I |` dom ( iEdg ` G ) ) ` i ) )
35 34 fveqeq2d 
 |-  ( j = ( _I |` dom ( iEdg ` G ) ) -> ( ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) <-> ( ( iEdg ` H ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) ) )
36 35 ralbidv 
 |-  ( j = ( _I |` dom ( iEdg ` G ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) <-> A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) ) )
37 33 36 anbi12d 
 |-  ( j = ( _I |` dom ( iEdg ` G ) ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) ) <-> ( ( _I |` dom ( iEdg ` G ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( ( _I |` dom ( iEdg ` G ) ) ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) ) ) )
38 13 32 37 spcedv 
 |-  ( ph -> E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) ) )
39 fvex 
 |-  ( Vtx ` G ) e. _V
40 resfunexg 
 |-  ( ( Fun _I /\ ( Vtx ` G ) e. _V ) -> ( _I |` ( Vtx ` G ) ) e. _V )
41 8 39 40 mp2an 
 |-  ( _I |` ( Vtx ` G ) ) e. _V
42 41 a1i 
 |-  ( ph -> ( _I |` ( Vtx ` G ) ) e. _V )
43 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
44 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
45 24 43 25 44 isgrim 
 |-  ( ( G e. UHGraph /\ H e. V /\ ( _I |` ( Vtx ` G ) ) e. _V ) -> ( ( _I |` ( Vtx ` G ) ) e. ( G GraphIso H ) <-> ( ( _I |` ( Vtx ` G ) ) : ( 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 ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) ) ) ) )
46 1 2 42 45 syl3anc 
 |-  ( ph -> ( ( _I |` ( Vtx ` G ) ) e. ( G GraphIso H ) <-> ( ( _I |` ( Vtx ` G ) ) : ( 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 ) ) = ( ( _I |` ( Vtx ` G ) ) " ( ( iEdg ` G ) ` i ) ) ) ) ) )
47 7 38 46 mpbir2and 
 |-  ( ph -> ( _I |` ( Vtx ` G ) ) e. ( G GraphIso H ) )