This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uhgrimisgrgric

Description: For isomorphic hypergraphs, the induced subgraph of a subset of vertices of one graph is isomorphic to the subgraph induced by the image of the subset. (Contributed by AV, 31-May-2025)

Ref Expression
Hypothesis uhgrimisgrgric.v 
|- V = ( Vtx ` G )
Assertion uhgrimisgrgric 
|- ( ( G e. UHGraph /\ F e. ( G GraphIso H ) /\ N C_ V ) -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) )

Proof

Step Hyp Ref Expression
1 uhgrimisgrgric.v 
 |-  V = ( Vtx ` G )
2 grimdmrel 
 |-  Rel dom GraphIso
3 2 ovrcl 
 |-  ( F e. ( G GraphIso H ) -> ( G e. _V /\ H e. _V ) )
4 3 3ad2ant2 
 |-  ( ( G e. UHGraph /\ F e. ( G GraphIso H ) /\ N C_ V ) -> ( G e. _V /\ H e. _V ) )
5 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
6 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
7 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
8 1 5 6 7 grimprop 
 |-  ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> ( Vtx ` H ) /\ E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) )
9 f1ofun 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> Fun F )
10 9 3ad2ant1 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) -> Fun F )
11 1 fvexi 
 |-  V e. _V
12 11 ssex 
 |-  ( N C_ V -> N e. _V )
13 resfunexg 
 |-  ( ( Fun F /\ N e. _V ) -> ( F |` N ) e. _V )
14 10 12 13 syl2an 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( F |` N ) e. _V )
15 f1of1 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> F : V -1-1-> ( Vtx ` H ) )
16 15 3ad2ant1 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) -> F : V -1-1-> ( Vtx ` H ) )
17 f1ores 
 |-  ( ( F : V -1-1-> ( Vtx ` H ) /\ N C_ V ) -> ( F |` N ) : N -1-1-onto-> ( F " N ) )
18 16 17 sylan 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( F |` N ) : N -1-1-onto-> ( F " N ) )
19 simpr 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( F |` N ) : N -1-1-onto-> ( F " N ) )
20 vex 
 |-  g e. _V
21 20 resex 
 |-  ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) e. _V
22 21 a1i 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) e. _V )
23 f1of1 
 |-  ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> g : dom ( iEdg ` G ) -1-1-> dom ( iEdg ` H ) )
24 23 adantr 
 |-  ( ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> g : dom ( iEdg ` G ) -1-1-> dom ( iEdg ` H ) )
25 24 3ad2ant2 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) -> g : dom ( iEdg ` G ) -1-1-> dom ( iEdg ` H ) )
26 25 ad2antrr 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> g : dom ( iEdg ` G ) -1-1-> dom ( iEdg ` H ) )
27 ssrab2 
 |-  { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G )
28 f1ores 
 |-  ( ( g : dom ( iEdg ` G ) -1-1-> dom ( iEdg ` H ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) ) -> ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> ( g " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) )
29 26 27 28 sylancl 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> ( g " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) )
30 1 6 uhgrf 
 |-  ( G e. UHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) )
31 id 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) )
32 difssd 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) -> ( ~P V \ { (/) } ) C_ ~P V )
33 31 32 fssd 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ~P V )
34 30 33 syl 
 |-  ( G e. UHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ~P V )
35 34 adantr 
 |-  ( ( G e. UHGraph /\ H e. _V ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ~P V )
36 35 anim2i 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( G e. UHGraph /\ H e. _V ) ) -> ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ~P V ) )
37 36 3adant2 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) -> ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ~P V ) )
38 37 ad2antrr 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ~P V ) )
39 simp2l 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) -> g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) )
40 39 anim1i 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ N C_ V ) )
41 40 adantr 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ N C_ V ) )
42 41 ancomd 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( N C_ V /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) )
43 simpl2r 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) )
44 43 adantr 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) )
45 uhgrimisgrgriclem 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ~P V ) /\ ( N C_ V /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( j e. dom ( iEdg ` H ) /\ ( ( iEdg ` H ) ` j ) C_ ( F " N ) ) <-> E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` k ) C_ N /\ ( g ` k ) = j ) ) )
46 38 42 44 45 syl3anc 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( ( j e. dom ( iEdg ` H ) /\ ( ( iEdg ` H ) ` j ) C_ ( F " N ) ) <-> E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` k ) C_ N /\ ( g ` k ) = j ) ) )
47 fveq2 
 |-  ( x = k -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` G ) ` k ) )
48 47 sseq1d 
 |-  ( x = k -> ( ( ( iEdg ` G ) ` x ) C_ N <-> ( ( iEdg ` G ) ` k ) C_ N ) )
49 48 rexrab 
 |-  ( E. k e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( g ` k ) = j <-> E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` k ) C_ N /\ ( g ` k ) = j ) )
50 46 49 bitr4di 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( ( j e. dom ( iEdg ` H ) /\ ( ( iEdg ` H ) ` j ) C_ ( F " N ) ) <-> E. k e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( g ` k ) = j ) )
51 fveq2 
 |-  ( x = j -> ( ( iEdg ` H ) ` x ) = ( ( iEdg ` H ) ` j ) )
52 51 sseq1d 
 |-  ( x = j -> ( ( ( iEdg ` H ) ` x ) C_ ( F " N ) <-> ( ( iEdg ` H ) ` j ) C_ ( F " N ) ) )
53 52 elrab 
 |-  ( j e. { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } <-> ( j e. dom ( iEdg ` H ) /\ ( ( iEdg ` H ) ` j ) C_ ( F " N ) ) )
54 53 a1i 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( j e. { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } <-> ( j e. dom ( iEdg ` H ) /\ ( ( iEdg ` H ) ` j ) C_ ( F " N ) ) ) )
55 f1ofn 
 |-  ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> g Fn dom ( iEdg ` G ) )
56 55 27 jctir 
 |-  ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> ( g Fn dom ( iEdg ` G ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) ) )
57 56 adantr 
 |-  ( ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( g Fn dom ( iEdg ` G ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) ) )
58 57 3ad2ant2 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) -> ( g Fn dom ( iEdg ` G ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) ) )
59 58 ad2antrr 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( g Fn dom ( iEdg ` G ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) ) )
60 fvelimab 
 |-  ( ( g Fn dom ( iEdg ` G ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) ) -> ( j e. ( g " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) <-> E. k e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( g ` k ) = j ) )
61 59 60 syl 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( j e. ( g " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) <-> E. k e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( g ` k ) = j ) )
62 50 54 61 3bitr4d 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( j e. { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } <-> j e. ( g " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ) )
63 62 eqrdv 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } = ( g " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) )
64 63 f1oeq3d 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } <-> ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> ( g " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ) )
65 29 64 mpbird 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } )
66 ssralv 
 |-  ( { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) )
67 27 66 ax-mp 
 |-  ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) )
68 elex 
 |-  ( G e. UHGraph -> G e. _V )
69 68 anim1i 
 |-  ( ( G e. UHGraph /\ H e. _V ) -> ( G e. _V /\ H e. _V ) )
70 69 3anim3i 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. UHGraph /\ H e. _V ) ) -> ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. _V /\ H e. _V ) ) )
71 70 anim1i 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. _V /\ H e. _V ) ) /\ N C_ V ) )
72 simpr 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. _V /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) /\ ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) )
73 fvres 
 |-  ( i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -> ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) = ( g ` i ) )
74 73 ad2antlr 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. _V /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) /\ ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) = ( g ` i ) )
75 74 fveq2d 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. _V /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) /\ ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) )
76 fveq2 
 |-  ( x = i -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` G ) ` i ) )
77 76 sseq1d 
 |-  ( x = i -> ( ( ( iEdg ` G ) ` x ) C_ N <-> ( ( iEdg ` G ) ` i ) C_ N ) )
78 77 elrab 
 |-  ( i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } <-> ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) )
79 78 simprbi 
 |-  ( i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -> ( ( iEdg ` G ) ` i ) C_ N )
80 79 ad2antlr 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. _V /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) /\ ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( iEdg ` G ) ` i ) C_ N )
81 resima2 
 |-  ( ( ( iEdg ` G ) ` i ) C_ N -> ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) )
82 80 81 syl 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. _V /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) /\ ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) )
83 72 75 82 3eqtr4rd 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. _V /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) /\ ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) )
84 83 ex 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. _V /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -> ( ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) )
85 71 84 sylanl1 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -> ( ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) )
86 85 ralimdva 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) )
87 67 86 syl5 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) )
88 87 expimpd 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) )
89 88 3exp1 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> ( ( F |` N ) : N -1-1-onto-> ( F " N ) -> ( ( G e. UHGraph /\ H e. _V ) -> ( N C_ V -> ( ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) ) ) ) )
90 89 com25 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> ( ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( G e. UHGraph /\ H e. _V ) -> ( N C_ V -> ( ( F |` N ) : N -1-1-onto-> ( F " N ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) ) ) ) )
91 90 3imp1 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( ( F |` N ) : N -1-1-onto-> ( F " N ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) )
92 91 imp 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) )
93 65 92 jca 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) )
94 f1oeq1 
 |-  ( h = ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -> ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } <-> ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } ) )
95 fveq1 
 |-  ( h = ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -> ( h ` i ) = ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) )
96 95 fveq2d 
 |-  ( h = ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -> ( ( iEdg ` H ) ` ( h ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) )
97 96 eqeq2d 
 |-  ( h = ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -> ( ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) <-> ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) )
98 97 ralbidv 
 |-  ( h = ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -> ( A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) <-> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) )
99 94 98 anbi12d 
 |-  ( h = ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -> ( ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) <-> ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( g |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) ` i ) ) ) ) )
100 22 93 99 spcedv 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) )
101 19 100 jca 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) /\ ( F |` N ) : N -1-1-onto-> ( F " N ) ) -> ( ( F |` N ) : N -1-1-onto-> ( F " N ) /\ E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) )
102 18 101 mpdan 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( ( F |` N ) : N -1-1-onto-> ( F " N ) /\ E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) )
103 f1oeq1 
 |-  ( f = ( F |` N ) -> ( f : N -1-1-onto-> ( F " N ) <-> ( F |` N ) : N -1-1-onto-> ( F " N ) ) )
104 imaeq1 
 |-  ( f = ( F |` N ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) )
105 104 eqeq1d 
 |-  ( f = ( F |` N ) -> ( ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) <-> ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) )
106 105 ralbidv 
 |-  ( f = ( F |` N ) -> ( A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) <-> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) )
107 106 anbi2d 
 |-  ( f = ( F |` N ) -> ( ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) <-> ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) )
108 107 exbidv 
 |-  ( f = ( F |` N ) -> ( E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) <-> E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) )
109 103 108 anbi12d 
 |-  ( f = ( F |` N ) -> ( ( f : N -1-1-onto-> ( F " N ) /\ E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) <-> ( ( F |` N ) : N -1-1-onto-> ( F " N ) /\ E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( ( F |` N ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) ) )
110 14 102 109 spcedv 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> E. f ( f : N -1-1-onto-> ( F " N ) /\ E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) )
111 simpl3 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( G e. UHGraph /\ H e. _V ) )
112 simpr 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> N C_ V )
113 f1of 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> F : V --> ( Vtx ` H ) )
114 113 fimassd 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> ( F " N ) C_ ( Vtx ` H ) )
115 114 a1d 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> ( N C_ V -> ( F " N ) C_ ( Vtx ` H ) ) )
116 115 3ad2ant1 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) -> ( N C_ V -> ( F " N ) C_ ( Vtx ` H ) ) )
117 116 imp 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( F " N ) C_ ( Vtx ` H ) )
118 eqid 
 |-  { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N }
119 eqid 
 |-  { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } = { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) }
120 1 5 6 7 118 119 isubgrgrim 
 |-  ( ( ( G e. UHGraph /\ H e. _V ) /\ ( N C_ V /\ ( F " N ) C_ ( Vtx ` H ) ) ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) <-> E. f ( f : N -1-1-onto-> ( F " N ) /\ E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) ) )
121 111 112 117 120 syl12anc 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) <-> E. f ( f : N -1-1-onto-> ( F " N ) /\ E. h ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ ( F " N ) } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) ) )
122 110 121 mpbird 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. _V ) ) /\ N C_ V ) -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) )
123 122 3exp1 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> ( ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( G e. UHGraph /\ H e. _V ) -> ( N C_ V -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) ) ) ) )
124 123 exlimdv 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> ( E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( G e. UHGraph /\ H e. _V ) -> ( N C_ V -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) ) ) ) )
125 124 imp 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( ( G e. UHGraph /\ H e. _V ) -> ( N C_ V -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) ) ) )
126 8 125 syl 
 |-  ( F e. ( G GraphIso H ) -> ( ( G e. UHGraph /\ H e. _V ) -> ( N C_ V -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) ) ) )
127 126 expd 
 |-  ( F e. ( G GraphIso H ) -> ( G e. UHGraph -> ( H e. _V -> ( N C_ V -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) ) ) ) )
128 127 com12 
 |-  ( G e. UHGraph -> ( F e. ( G GraphIso H ) -> ( H e. _V -> ( N C_ V -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) ) ) ) )
129 128 com34 
 |-  ( G e. UHGraph -> ( F e. ( G GraphIso H ) -> ( N C_ V -> ( H e. _V -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) ) ) ) )
130 129 3imp 
 |-  ( ( G e. UHGraph /\ F e. ( G GraphIso H ) /\ N C_ V ) -> ( H e. _V -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) ) )
131 130 adantld 
 |-  ( ( G e. UHGraph /\ F e. ( G GraphIso H ) /\ N C_ V ) -> ( ( G e. _V /\ H e. _V ) -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) ) )
132 4 131 mpd 
 |-  ( ( G e. UHGraph /\ F e. ( G GraphIso H ) /\ N C_ V ) -> ( G ISubGr N ) ~=gr ( H ISubGr ( F " N ) ) )