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 ) ) ) ) ) )

Metamath Proof Explorer

Theorem uspgrlim

Proof