Metamath Proof Explorer

Theorem uspgrlim

Description: A local isomorphism of simple pseudographs is a bijection between their vertices that preserves neighborhoods, expressed by properties of their edges (not edge functions as in isgrlim2 ). (Contributed by AV, 15-Aug-2025)

Ref Expression
Hypotheses uspgrlim.v 
|- V = ( Vtx ` G )
uspgrlim.w 
|- W = ( Vtx ` H )
uspgrlim.n 
|- N = ( G ClNeighbVtx v )
uspgrlim.m 
|- M = ( H ClNeighbVtx ( F ` v ) )
uspgrlim.i 
|- I = ( Edg ` G )
uspgrlim.j 
|- J = ( Edg ` H )
uspgrlim.k 
|- K = { x e. I | x C_ N }
uspgrlim.l 
|- L = { x e. J | x C_ M }
Assertion uspgrlim 
|- ( ( G e. USPGraph /\ H e. USPGraph /\ F e. Z ) -> ( F e. ( G GraphLocIso H ) <-> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 uspgrlim.v 
 |-  V = ( Vtx ` G )
2 uspgrlim.w 
 |-  W = ( Vtx ` H )
3 uspgrlim.n 
 |-  N = ( G ClNeighbVtx v )
4 uspgrlim.m 
 |-  M = ( H ClNeighbVtx ( F ` v ) )
5 uspgrlim.i 
 |-  I = ( Edg ` G )
6 uspgrlim.j 
 |-  J = ( Edg ` H )
7 uspgrlim.k 
 |-  K = { x e. I | x C_ N }
8 uspgrlim.l 
 |-  L = { x e. J | x C_ M }
9 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
10 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
11 eqid 
 |-  { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N }
12 eqid 
 |-  { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } = { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M }
13 1 2 3 4 9 10 11 12 isgrlim2 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. Z ) -> ( F e. ( G GraphLocIso H ) <-> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) ) ) )
14 fvex 
 |-  ( iEdg ` H ) e. _V
15 vex 
 |-  h e. _V
16 14 15 coex 
 |-  ( ( iEdg ` H ) o. h ) e. _V
17 fvex 
 |-  ( iEdg ` G ) e. _V
18 17 cnvex 
 |-  `' ( iEdg ` G ) e. _V
19 16 18 coex 
 |-  ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) e. _V
20 19 a1i 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) e. _V )
21 9 uspgrf1oedg 
 |-  ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) )
22 21 ad2antrr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) )
23 simprl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ 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_ M } )
24 10 uspgrf1oedg 
 |-  ( H e. USPGraph -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) )
25 24 ad2antlr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) )
26 ssrab2 
 |-  { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G )
27 ssrab2 
 |-  { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } C_ dom ( iEdg ` H )
28 26 27 pm3.2i 
 |-  ( { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) /\ { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } C_ dom ( iEdg ` H ) )
29 28 a1i 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) /\ { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } C_ dom ( iEdg ` H ) ) )
30 3f1oss1 
 |-  ( ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) ) /\ ( { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } C_ dom ( iEdg ` G ) /\ { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } C_ dom ( iEdg ` H ) ) ) -> ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) : ( ( iEdg ` G ) " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -1-1-onto-> ( ( iEdg ` H ) " { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) )
31 22 23 25 29 30 syl31anc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) : ( ( iEdg ` G ) " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -1-1-onto-> ( ( iEdg ` H ) " { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) )
32 eqidd 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) = ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) )
33 3 5 7 uspgrlimlem1 
 |-  ( G e. USPGraph -> K = ( ( iEdg ` G ) " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) )
34 33 ad2antrr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> K = ( ( iEdg ` G ) " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) )
35 4 6 8 uspgrlimlem1 
 |-  ( H e. USPGraph -> L = ( ( iEdg ` H ) " { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) )
36 35 ad2antlr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> L = ( ( iEdg ` H ) " { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) )
37 32 34 36 f1oeq123d 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) : K -1-1-onto-> L <-> ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) : ( ( iEdg ` G ) " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ) -1-1-onto-> ( ( iEdg ` H ) " { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) ) )
38 31 37 mpbird 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) : K -1-1-onto-> L )
39 simpll 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> G e. USPGraph )
40 simprr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ 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 " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) )
41 1 2 3 4 5 6 7 8 uspgrlimlem3 
 |-  ( ( G e. USPGraph /\ h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) -> ( e e. K -> ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) ) )
42 39 23 40 41 syl3anc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( e e. K -> ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) ) )
43 42 ralrimiv 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> A. e e. K ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) )
44 38 43 jca 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) ) )
45 f1oeq1 
 |-  ( g = ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) -> ( g : K -1-1-onto-> L <-> ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) : K -1-1-onto-> L ) )
46 fveq1 
 |-  ( g = ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) -> ( g ` e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) )
47 46 eqeq2d 
 |-  ( g = ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) -> ( ( f " e ) = ( g ` e ) <-> ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) ) )
48 47 ralbidv 
 |-  ( g = ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) -> ( A. e e. K ( f " e ) = ( g ` e ) <-> A. e e. K ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) ) )
49 45 48 anbi12d 
 |-  ( g = ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) -> ( ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) <-> ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( ( ( ( iEdg ` H ) o. h ) o. `' ( iEdg ` G ) ) ` e ) ) ) )
50 20 44 49 spcedv 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) -> E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) )
51 50 ex 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) -> E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) )
52 51 exlimdv 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) -> E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) )
53 14 cnvex 
 |-  `' ( iEdg ` H ) e. _V
54 vex 
 |-  g e. _V
55 53 54 coex 
 |-  ( `' ( iEdg ` H ) o. g ) e. _V
56 55 17 coex 
 |-  ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) e. _V
57 56 a1i 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) e. _V )
58 21 ad2antrr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) )
59 simprl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> g : K -1-1-onto-> L )
60 24 ad2antlr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) )
61 5 rabeqi 
 |-  { x e. I | x C_ N } = { x e. ( Edg ` G ) | x C_ N }
62 7 61 eqtri 
 |-  K = { x e. ( Edg ` G ) | x C_ N }
63 62 ssrab3 
 |-  K C_ ( Edg ` G )
64 6 rabeqi 
 |-  { x e. J | x C_ M } = { x e. ( Edg ` H ) | x C_ M }
65 8 64 eqtri 
 |-  L = { x e. ( Edg ` H ) | x C_ M }
66 65 ssrab3 
 |-  L C_ ( Edg ` H )
67 63 66 pm3.2i 
 |-  ( K C_ ( Edg ` G ) /\ L C_ ( Edg ` H ) )
68 67 a1i 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( K C_ ( Edg ` G ) /\ L C_ ( Edg ` H ) ) )
69 3f1oss2 
 |-  ( ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) /\ g : K -1-1-onto-> L /\ ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-onto-> ( Edg ` H ) ) /\ ( K C_ ( Edg ` G ) /\ L C_ ( Edg ` H ) ) ) -> ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) : ( `' ( iEdg ` G ) " K ) -1-1-onto-> ( `' ( iEdg ` H ) " L ) )
70 58 59 60 68 69 syl31anc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) : ( `' ( iEdg ` G ) " K ) -1-1-onto-> ( `' ( iEdg ` H ) " L ) )
71 eqidd 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) = ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) )
72 3 5 7 uspgrlimlem2 
 |-  ( G e. USPGraph -> ( `' ( iEdg ` G ) " K ) = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } )
73 72 ad2antrr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( `' ( iEdg ` G ) " K ) = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } )
74 4 6 8 uspgrlimlem2 
 |-  ( H e. USPGraph -> ( `' ( iEdg ` H ) " L ) = { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } )
75 74 ad2antlr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( `' ( iEdg ` H ) " L ) = { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } )
76 71 73 75 f1oeq123d 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) : ( `' ( iEdg ` G ) " K ) -1-1-onto-> ( `' ( iEdg ` H ) " L ) <-> ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) )
77 70 76 mpbid 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } )
78 fveq2 
 |-  ( x = i -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` G ) ` i ) )
79 78 sseq1d 
 |-  ( x = i -> ( ( ( iEdg ` G ) ` x ) C_ N <-> ( ( iEdg ` G ) ` i ) C_ N ) )
80 79 elrab 
 |-  ( i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } <-> ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) )
81 1 2 3 4 5 6 7 8 uspgrlimlem4 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( ( i e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` i ) C_ N ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) ) )
82 80 81 biimtrid 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -> ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) ) )
83 82 ralrimiv 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) )
84 77 83 jca 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) ) )
85 f1oeq1 
 |-  ( h = ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) -> ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } <-> ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } ) )
86 fveq1 
 |-  ( h = ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) -> ( h ` i ) = ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) )
87 86 fveq2d 
 |-  ( h = ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) -> ( ( iEdg ` H ) ` ( h ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) )
88 87 eqeq2d 
 |-  ( h = ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) -> ( ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) <-> ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) ) )
89 88 ralbidv 
 |-  ( h = ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) -> ( 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 " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) ) )
90 85 89 anbi12d 
 |-  ( h = ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) -> ( ( h : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) <-> ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) : { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } -1-1-onto-> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) C_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( ( `' ( iEdg ` H ) o. g ) o. ( iEdg ` G ) ) ` i ) ) ) ) )
91 57 84 90 spcedv 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) -> 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) )
92 91 ex 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) -> 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) )
93 92 exlimdv 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) -> 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) )
94 52 93 impbid 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) <-> E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) )
95 94 anbi2d 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( f : N -1-1-onto-> M /\ 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) <-> ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) )
96 95 exbidv 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( E. f ( f : N -1-1-onto-> M /\ 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) )
97 96 ralbidv 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( A. v e. V E. f ( f : N -1-1-onto-> M /\ 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) <-> A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) )
98 97 anbi2d 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) ) <-> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) ) )
99 98 3adant3 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. Z ) -> ( ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ 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_ M } /\ A. i e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ N } ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( h ` i ) ) ) ) ) <-> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) ) )
100 13 99 bitrd 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. Z ) -> ( F e. ( G GraphLocIso H ) <-> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) ) )