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

Metamath Proof Explorer

Theorem clnbgrgrimlem

Description: Lemma for clnbgrgrim : For two isomorphic hypergraphs, if there is an edge connecting the image of a vertex of the first graph with a vertex of the second graph, the vertex of the second graph is the image of a neighbor of the vertex of the first graph. (Contributed by AV, 2-Jun-2025)

Ref Expression
Hypotheses clnbgrgrim.v 
|- V = ( Vtx ` G )
clnbgrgrimlem.w 
|- W = ( Vtx ` H )
clnbgrgrimlem.e 
|- E = ( Edg ` H )
Assertion clnbgrgrimlem 
|- ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ ( X e. V /\ Y e. W ) ) -> ( ( K e. E /\ { ( F ` X ) , Y } C_ K ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = Y ) )

Proof

Step Hyp Ref Expression
1 clnbgrgrim.v 
 |-  V = ( Vtx ` G )
2 clnbgrgrimlem.w 
 |-  W = ( Vtx ` H )
3 clnbgrgrimlem.e 
 |-  E = ( Edg ` H )
4 3 eleq2i 
 |-  ( K e. E <-> K e. ( Edg ` H ) )
5 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
6 5 uhgredgiedgb 
 |-  ( H e. UHGraph -> ( K e. ( Edg ` H ) <-> E. k e. dom ( iEdg ` H ) K = ( ( iEdg ` H ) ` k ) ) )
7 4 6 bitrid 
 |-  ( H e. UHGraph -> ( K e. E <-> E. k e. dom ( iEdg ` H ) K = ( ( iEdg ` H ) ` k ) ) )
8 7 adantl 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> ( K e. E <-> E. k e. dom ( iEdg ` H ) K = ( ( iEdg ` H ) ` k ) ) )
9 8 3ad2ant3 
 |-  ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) -> ( K e. E <-> E. k e. dom ( iEdg ` H ) K = ( ( iEdg ` H ) ` k ) ) )
10 9 adantr 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> ( K e. E <-> E. k e. dom ( iEdg ` H ) K = ( ( iEdg ` H ) ` k ) ) )
11 sseq2 
 |-  ( K = ( ( iEdg ` H ) ` k ) -> ( { ( F ` X ) , Y } C_ K <-> { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) ) )
12 11 adantl 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ K = ( ( iEdg ` H ) ` k ) ) -> ( { ( F ` X ) , Y } C_ K <-> { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) ) )
13 simp1 
 |-  ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) -> F : V -1-1-onto-> W )
14 simpr 
 |-  ( ( X e. V /\ Y e. W ) -> Y e. W )
15 13 14 anim12i 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> ( F : V -1-1-onto-> W /\ Y e. W ) )
16 f1ocnvdm 
 |-  ( ( F : V -1-1-onto-> W /\ Y e. W ) -> ( `' F ` Y ) e. V )
17 15 16 syl 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> ( `' F ` Y ) e. V )
18 simpl 
 |-  ( ( X e. V /\ Y e. W ) -> X e. V )
19 18 adantl 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> X e. V )
20 17 19 jca 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> ( ( `' F ` Y ) e. V /\ X e. V ) )
21 20 ad2antrr 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) ) -> ( ( `' F ` Y ) e. V /\ X e. V ) )
22 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
23 22 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
24 23 adantr 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> Fun ( iEdg ` G ) )
25 24 3ad2ant3 
 |-  ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) -> Fun ( iEdg ` G ) )
26 25 ad2antrr 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) -> Fun ( iEdg ` G ) )
27 simpl2l 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) )
28 f1ocnvdm 
 |-  ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ k e. dom ( iEdg ` H ) ) -> ( `' j ` k ) e. dom ( iEdg ` G ) )
29 27 28 sylan 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) -> ( `' j ` k ) e. dom ( iEdg ` G ) )
30 26 29 jca 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) -> ( Fun ( iEdg ` G ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) )
31 22 iedgedg 
 |-  ( ( Fun ( iEdg ` G ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` ( `' j ` k ) ) e. ( Edg ` G ) )
32 30 31 syl 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) -> ( ( iEdg ` G ) ` ( `' j ` k ) ) e. ( Edg ` G ) )
33 32 adantr 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) ) -> ( ( iEdg ` G ) ` ( `' j ` k ) ) e. ( Edg ` G ) )
34 sseq2 
 |-  ( e = ( ( iEdg ` G ) ` ( `' j ` k ) ) -> ( { X , ( `' F ` Y ) } C_ e <-> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
35 34 adantl 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) ) /\ e = ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> ( { X , ( `' F ` Y ) } C_ e <-> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
36 2fveq3 
 |-  ( i = ( `' j ` k ) -> ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) )
37 fveq2 
 |-  ( i = ( `' j ` k ) -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` ( `' j ` k ) ) )
38 37 imaeq2d 
 |-  ( i = ( `' j ` k ) -> ( F " ( ( iEdg ` G ) ` i ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
39 36 38 eqeq12d 
 |-  ( i = ( `' j ` k ) -> ( ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) <-> ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
40 39 rspcv 
 |-  ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
41 40 adantl 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
42 simpr 
 |-  ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) )
43 simp1 
 |-  ( ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) -> k e. dom ( iEdg ` H ) )
44 42 43 anim12i 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ k e. dom ( iEdg ` H ) ) )
45 44 adantr 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ k e. dom ( iEdg ` H ) ) )
46 f1ocnvfv2 
 |-  ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ k e. dom ( iEdg ` H ) ) -> ( j ` ( `' j ` k ) ) = k )
47 45 46 syl 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( j ` ( `' j ` k ) ) = k )
48 47 fveqeq2d 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) <-> ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
49 sseq2 
 |-  ( ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) <-> { ( F ` X ) , Y } C_ ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
50 49 adantl 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) <-> { ( F ` X ) , Y } C_ ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
51 f1ofn 
 |-  ( F : V -1-1-onto-> W -> F Fn V )
52 51 ad2antrr 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> F Fn V )
53 simpr3l 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> X e. V )
54 simpl 
 |-  ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> F : V -1-1-onto-> W )
55 14 3ad2ant3 
 |-  ( ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) -> Y e. W )
56 54 55 anim12i 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> ( F : V -1-1-onto-> W /\ Y e. W ) )
57 56 16 syl 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> ( `' F ` Y ) e. V )
58 52 53 57 3jca 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> ( F Fn V /\ X e. V /\ ( `' F ` Y ) e. V ) )
59 58 adantr 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( F Fn V /\ X e. V /\ ( `' F ` Y ) e. V ) )
60 fnimapr 
 |-  ( ( F Fn V /\ X e. V /\ ( `' F ` Y ) e. V ) -> ( F " { X , ( `' F ` Y ) } ) = { ( F ` X ) , ( F ` ( `' F ` Y ) ) } )
61 59 60 syl 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( F " { X , ( `' F ` Y ) } ) = { ( F ` X ) , ( F ` ( `' F ` Y ) ) } )
62 56 adantr 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( F : V -1-1-onto-> W /\ Y e. W ) )
63 f1ocnvfv2 
 |-  ( ( F : V -1-1-onto-> W /\ Y e. W ) -> ( F ` ( `' F ` Y ) ) = Y )
64 62 63 syl 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( F ` ( `' F ` Y ) ) = Y )
65 64 preq2d 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> { ( F ` X ) , ( F ` ( `' F ` Y ) ) } = { ( F ` X ) , Y } )
66 61 65 eqtr2d 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> { ( F ` X ) , Y } = ( F " { X , ( `' F ` Y ) } ) )
67 66 sseq1d 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( { ( F ` X ) , Y } C_ ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) <-> ( F " { X , ( `' F ` Y ) } ) C_ ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
68 f1of1 
 |-  ( F : V -1-1-onto-> W -> F : V -1-1-> W )
69 68 adantr 
 |-  ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> F : V -1-1-> W )
70 69 ad2antrr 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> F : V -1-1-> W )
71 53 57 prssd 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> { X , ( `' F ` Y ) } C_ V )
72 71 adantr 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> { X , ( `' F ` Y ) } C_ V )
73 simpr2l 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> G e. UHGraph )
74 1 22 uhgrss 
 |-  ( ( G e. UHGraph /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` ( `' j ` k ) ) C_ V )
75 73 74 sylan 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` ( `' j ` k ) ) C_ V )
76 f1imass 
 |-  ( ( F : V -1-1-> W /\ ( { X , ( `' F ` Y ) } C_ V /\ ( ( iEdg ` G ) ` ( `' j ` k ) ) C_ V ) ) -> ( ( F " { X , ( `' F ` Y ) } ) C_ ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) <-> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
77 70 72 75 76 syl12anc 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( ( F " { X , ( `' F ` Y ) } ) C_ ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) <-> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
78 77 biimpd 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( ( F " { X , ( `' F ` Y ) } ) C_ ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
79 67 78 sylbid 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( { ( F ` X ) , Y } C_ ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
80 79 adantr 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) -> ( { ( F ` X ) , Y } C_ ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
81 50 80 sylbid 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
82 81 ex 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
83 48 82 sylbid 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
84 41 83 syld 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
85 84 ex 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) ) )
86 85 com23 
 |-  ( ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( k e. dom ( iEdg ` H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ ( X e. V /\ Y e. W ) ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) ) )
87 86 3exp2 
 |-  ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( k e. dom ( iEdg ` H ) -> ( ( G e. UHGraph /\ H e. UHGraph ) -> ( ( X e. V /\ Y e. W ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) ) ) ) ) )
88 87 com25 
 |-  ( ( F : V -1-1-onto-> W /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( G e. UHGraph /\ H e. UHGraph ) -> ( ( X e. V /\ Y e. W ) -> ( k e. dom ( iEdg ` H ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) ) ) ) ) )
89 88 expimpd 
 |-  ( F : V -1-1-onto-> W -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( G e. UHGraph /\ H e. UHGraph ) -> ( ( X e. V /\ Y e. W ) -> ( k e. dom ( iEdg ` H ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) ) ) ) ) )
90 89 3imp1 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> ( k e. dom ( iEdg ` H ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) ) )
91 90 imp 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
92 29 91 mpd 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
93 92 imp 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) ) -> { X , ( `' F ` Y ) } C_ ( ( iEdg ` G ) ` ( `' j ` k ) ) )
94 33 35 93 rspcedvd 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) ) -> E. e e. ( Edg ` G ) { X , ( `' F ` Y ) } C_ e )
95 94 olcd 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) ) -> ( ( `' F ` Y ) = X \/ E. e e. ( Edg ` G ) { X , ( `' F ` Y ) } C_ e ) )
96 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
97 1 96 clnbgrel 
 |-  ( ( `' F ` Y ) e. ( G ClNeighbVtx X ) <-> ( ( ( `' F ` Y ) e. V /\ X e. V ) /\ ( ( `' F ` Y ) = X \/ E. e e. ( Edg ` G ) { X , ( `' F ` Y ) } C_ e ) ) )
98 21 95 97 sylanbrc 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) ) -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) )
99 98 ex 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) )
100 99 adantr 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ K = ( ( iEdg ` H ) ` k ) ) -> ( { ( F ` X ) , Y } C_ ( ( iEdg ` H ) ` k ) -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) )
101 12 100 sylbid 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) /\ K = ( ( iEdg ` H ) ` k ) ) -> ( { ( F ` X ) , Y } C_ K -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) )
102 101 ex 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) /\ k e. dom ( iEdg ` H ) ) -> ( K = ( ( iEdg ` H ) ` k ) -> ( { ( F ` X ) , Y } C_ K -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) ) )
103 102 rexlimdva 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> ( E. k e. dom ( iEdg ` H ) K = ( ( iEdg ` H ) ` k ) -> ( { ( F ` X ) , Y } C_ K -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) ) )
104 10 103 sylbid 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> ( K e. E -> ( { ( F ` X ) , Y } C_ K -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) ) )
105 104 impd 
 |-  ( ( ( F : V -1-1-onto-> W /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ ( X e. V /\ Y e. W ) ) -> ( ( K e. E /\ { ( F ` X ) , Y } C_ K ) -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) )
106 105 3exp1 
 |-  ( F : V -1-1-onto-> W -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( G e. UHGraph /\ H e. UHGraph ) -> ( ( X e. V /\ Y e. W ) -> ( ( K e. E /\ { ( F ` X ) , Y } C_ K ) -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) ) ) ) )
107 106 exlimdv 
 |-  ( F : V -1-1-onto-> W -> ( E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( G e. UHGraph /\ H e. UHGraph ) -> ( ( X e. V /\ Y e. W ) -> ( ( K e. E /\ { ( F ` X ) , Y } C_ K ) -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) ) ) ) )
108 107 imp 
 |-  ( ( F : V -1-1-onto-> W /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( ( G e. UHGraph /\ H e. UHGraph ) -> ( ( X e. V /\ Y e. W ) -> ( ( K e. E /\ { ( F ` X ) , Y } C_ K ) -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) ) ) )
109 1 2 22 5 grimprop 
 |-  ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> W /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) )
110 108 109 syl11 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> ( F e. ( G GraphIso H ) -> ( ( X e. V /\ Y e. W ) -> ( ( K e. E /\ { ( F ` X ) , Y } C_ K ) -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) ) ) ) )
111 110 3imp1 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ ( X e. V /\ Y e. W ) ) /\ ( K e. E /\ { ( F ` X ) , Y } C_ K ) ) -> ( `' F ` Y ) e. ( G ClNeighbVtx X ) )
112 fveqeq2 
 |-  ( n = ( `' F ` Y ) -> ( ( F ` n ) = Y <-> ( F ` ( `' F ` Y ) ) = Y ) )
113 112 adantl 
 |-  ( ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ ( X e. V /\ Y e. W ) ) /\ ( K e. E /\ { ( F ` X ) , Y } C_ K ) ) /\ n = ( `' F ` Y ) ) -> ( ( F ` n ) = Y <-> ( F ` ( `' F ` Y ) ) = Y ) )
114 1 2 grimf1o 
 |-  ( F e. ( G GraphIso H ) -> F : V -1-1-onto-> W )
115 114 14 anim12i 
 |-  ( ( F e. ( G GraphIso H ) /\ ( X e. V /\ Y e. W ) ) -> ( F : V -1-1-onto-> W /\ Y e. W ) )
116 115 3adant1 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ ( X e. V /\ Y e. W ) ) -> ( F : V -1-1-onto-> W /\ Y e. W ) )
117 116 adantr 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ ( X e. V /\ Y e. W ) ) /\ ( K e. E /\ { ( F ` X ) , Y } C_ K ) ) -> ( F : V -1-1-onto-> W /\ Y e. W ) )
118 117 63 syl 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ ( X e. V /\ Y e. W ) ) /\ ( K e. E /\ { ( F ` X ) , Y } C_ K ) ) -> ( F ` ( `' F ` Y ) ) = Y )
119 111 113 118 rspcedvd 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ ( X e. V /\ Y e. W ) ) /\ ( K e. E /\ { ( F ` X ) , Y } C_ K ) ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = Y )
120 119 ex 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ ( X e. V /\ Y e. W ) ) -> ( ( K e. E /\ { ( F ` X ) , Y } C_ K ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = Y ) )