Metamath Proof Explorer

Theorem clnbgrgrim

Description: Graph isomorphisms between hypergraphs map closed neighborhoods onto closed neighborhoods. (Contributed by AV, 2-Jun-2025)

Ref Expression
Hypothesis clnbgrgrim.v 
|- V = ( Vtx ` G )
Assertion clnbgrgrim 
|- ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) /\ X e. V ) -> ( H ClNeighbVtx ( F ` X ) ) = ( F " ( G ClNeighbVtx X ) ) )

Proof

Step Hyp Ref Expression
1 clnbgrgrim.v 
 |-  V = ( Vtx ` G )
2 fveqeq2 
 |-  ( n = X -> ( ( F ` n ) = ( F ` X ) <-> ( F ` X ) = ( F ` X ) ) )
3 1 clnbgrvtxel 
 |-  ( X e. V -> X e. ( G ClNeighbVtx X ) )
4 3 3ad2ant3 
 |-  ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) -> X e. ( G ClNeighbVtx X ) )
5 eqidd 
 |-  ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) -> ( F ` X ) = ( F ` X ) )
6 2 4 5 rspcedvdw 
 |-  ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = ( F ` X ) )
7 6 adantr 
 |-  ( ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) /\ ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = ( F ` X ) )
8 eqeq2 
 |-  ( x = ( F ` X ) -> ( ( F ` n ) = x <-> ( F ` n ) = ( F ` X ) ) )
9 8 rexbidv 
 |-  ( x = ( F ` X ) -> ( E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x <-> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = ( F ` X ) ) )
10 7 9 syl5ibrcom 
 |-  ( ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) /\ ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) ) -> ( x = ( F ` X ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
11 simpl2 
 |-  ( ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) /\ ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) ) -> ( G e. UHGraph /\ H e. UHGraph ) )
12 simpl1 
 |-  ( ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) /\ ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) ) -> F e. ( G GraphIso H ) )
13 simp3 
 |-  ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) -> X e. V )
14 simpl 
 |-  ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) -> x e. ( Vtx ` H ) )
15 13 14 anim12i 
 |-  ( ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) /\ ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) ) -> ( X e. V /\ x e. ( Vtx ` H ) ) )
16 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
17 eqid 
 |-  ( Edg ` H ) = ( Edg ` H )
18 1 16 17 clnbgrgrimlem 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) /\ ( X e. V /\ x e. ( Vtx ` H ) ) ) -> ( ( e e. ( Edg ` H ) /\ { ( F ` X ) , x } C_ e ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
19 11 12 15 18 syl3anc 
 |-  ( ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) /\ ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) ) -> ( ( e e. ( Edg ` H ) /\ { ( F ` X ) , x } C_ e ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
20 19 expd 
 |-  ( ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) /\ ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) ) -> ( e e. ( Edg ` H ) -> ( { ( F ` X ) , x } C_ e -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) ) )
21 20 rexlimdv 
 |-  ( ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) /\ ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) ) -> ( E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
22 10 21 jaod 
 |-  ( ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) /\ ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) ) -> ( ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
23 22 expimpd 
 |-  ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) -> ( ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) -> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
24 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
25 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
26 1 16 24 25 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 ) ) ) ) )
27 f1of 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> F : V --> ( Vtx ` H ) )
28 27 adantr 
 |-  ( ( 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 ) ) ) ) -> F : V --> ( Vtx ` H ) )
29 28 3ad2ant1 
 |-  ( ( ( 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. UHGraph ) /\ X e. V ) -> F : V --> ( Vtx ` H ) )
30 29 ad2antrr 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> F : V --> ( Vtx ` H ) )
31 1 clnbgrisvtx 
 |-  ( n e. ( G ClNeighbVtx X ) -> n e. V )
32 31 adantl 
 |-  ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) -> n e. V )
33 32 adantr 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> n e. V )
34 30 33 ffvelcdmd 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> ( F ` n ) e. ( Vtx ` H ) )
35 eleq1 
 |-  ( x = ( F ` n ) -> ( x e. ( Vtx ` H ) <-> ( F ` n ) e. ( Vtx ` H ) ) )
36 35 eqcoms 
 |-  ( ( F ` n ) = x -> ( x e. ( Vtx ` H ) <-> ( F ` n ) e. ( Vtx ` H ) ) )
37 36 adantl 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> ( x e. ( Vtx ` H ) <-> ( F ` n ) e. ( Vtx ` H ) ) )
38 34 37 mpbird 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> x e. ( Vtx ` H ) )
39 simp3 
 |-  ( ( ( 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. UHGraph ) /\ X e. V ) -> X e. V )
40 29 39 ffvelcdmd 
 |-  ( ( ( 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. UHGraph ) /\ X e. V ) -> ( F ` X ) e. ( Vtx ` H ) )
41 40 ad2antrr 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> ( F ` X ) e. ( Vtx ` H ) )
42 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
43 1 42 clnbgrel 
 |-  ( n e. ( G ClNeighbVtx X ) <-> ( ( n e. V /\ X e. V ) /\ ( n = X \/ E. k e. ( Edg ` G ) { X , n } C_ k ) ) )
44 fveq2 
 |-  ( n = X -> ( F ` n ) = ( F ` X ) )
45 44 orcd 
 |-  ( n = X -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) )
46 45 2a1d 
 |-  ( n = X -> ( ( n e. V /\ X e. V ) -> ( ( ( 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. UHGraph ) /\ X e. V ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) )
47 24 uhgredgiedgb 
 |-  ( G e. UHGraph -> ( k e. ( Edg ` G ) <-> E. j e. dom ( iEdg ` G ) k = ( ( iEdg ` G ) ` j ) ) )
48 47 adantr 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> ( k e. ( Edg ` G ) <-> E. j e. dom ( iEdg ` G ) k = ( ( iEdg ` G ) ` j ) ) )
49 48 3ad2ant2 
 |-  ( ( ( 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. UHGraph ) /\ X e. V ) -> ( k e. ( Edg ` G ) <-> E. j e. dom ( iEdg ` G ) k = ( ( iEdg ` G ) ` j ) ) )
50 49 biimpa 
 |-  ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ k e. ( Edg ` G ) ) -> E. j e. dom ( iEdg ` G ) k = ( ( iEdg ` G ) ` j ) )
51 2fveq3 
 |-  ( i = j -> ( ( iEdg ` H ) ` ( g ` i ) ) = ( ( iEdg ` H ) ` ( g ` j ) ) )
52 fveq2 
 |-  ( i = j -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` j ) )
53 52 imaeq2d 
 |-  ( i = j -> ( F " ( ( iEdg ` G ) ` i ) ) = ( F " ( ( iEdg ` G ) ` j ) ) )
54 51 53 eqeq12d 
 |-  ( i = j -> ( ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) <-> ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) )
55 54 rspcv 
 |-  ( j e. dom ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) )
56 55 3ad2ant3 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) )
57 sseq2 
 |-  ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k <-> { X , n } C_ ( ( iEdg ` G ) ` j ) ) )
58 57 3ad2ant3 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) /\ k = ( ( iEdg ` G ) ` j ) ) -> ( { X , n } C_ k <-> { X , n } C_ ( ( iEdg ` G ) ` j ) ) )
59 sseq2 
 |-  ( e = ( ( iEdg ` H ) ` ( g ` j ) ) -> ( { ( F ` X ) , ( F ` n ) } C_ e <-> { ( F ` X ) , ( F ` n ) } C_ ( ( iEdg ` H ) ` ( g ` j ) ) ) )
60 25 uhgrfun 
 |-  ( H e. UHGraph -> Fun ( iEdg ` H ) )
61 60 adantl 
 |-  ( ( G e. UHGraph /\ H e. UHGraph ) -> Fun ( iEdg ` H ) )
62 61 3ad2ant3 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) -> Fun ( iEdg ` H ) )
63 f1of 
 |-  ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> g : dom ( iEdg ` G ) --> dom ( iEdg ` H ) )
64 63 adantl 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> g : dom ( iEdg ` G ) --> dom ( iEdg ` H ) )
65 64 3ad2ant1 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) -> g : dom ( iEdg ` G ) --> dom ( iEdg ` H ) )
66 65 ffvelcdmda 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ j e. dom ( iEdg ` G ) ) -> ( g ` j ) e. dom ( iEdg ` H ) )
67 25 iedgedg 
 |-  ( ( Fun ( iEdg ` H ) /\ ( g ` j ) e. dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) ` ( g ` j ) ) e. ( Edg ` H ) )
68 62 66 67 syl2an2r 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ j e. dom ( iEdg ` G ) ) -> ( ( iEdg ` H ) ` ( g ` j ) ) e. ( Edg ` H ) )
69 68 3adant2 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) -> ( ( iEdg ` H ) ` ( g ` j ) ) e. ( Edg ` H ) )
70 69 adantr 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) -> ( ( iEdg ` H ) ` ( g ` j ) ) e. ( Edg ` H ) )
71 70 3ad2ant1 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ { X , n } C_ ( ( iEdg ` G ) ` j ) /\ ( n e. V /\ X e. V ) ) -> ( ( iEdg ` H ) ` ( g ` j ) ) e. ( Edg ` H ) )
72 f1ofn 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> F Fn V )
73 72 adantr 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> F Fn V )
74 73 3ad2ant1 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) -> F Fn V )
75 74 3ad2ant1 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) -> F Fn V )
76 75 adantr 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) -> F Fn V )
77 pm3.22 
 |-  ( ( n e. V /\ X e. V ) -> ( X e. V /\ n e. V ) )
78 76 77 anim12i 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ ( n e. V /\ X e. V ) ) -> ( F Fn V /\ ( X e. V /\ n e. V ) ) )
79 78 3adant2 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ { X , n } C_ ( ( iEdg ` G ) ` j ) /\ ( n e. V /\ X e. V ) ) -> ( F Fn V /\ ( X e. V /\ n e. V ) ) )
80 3anass 
 |-  ( ( F Fn V /\ X e. V /\ n e. V ) <-> ( F Fn V /\ ( X e. V /\ n e. V ) ) )
81 79 80 sylibr 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ { X , n } C_ ( ( iEdg ` G ) ` j ) /\ ( n e. V /\ X e. V ) ) -> ( F Fn V /\ X e. V /\ n e. V ) )
82 fnimapr 
 |-  ( ( F Fn V /\ X e. V /\ n e. V ) -> ( F " { X , n } ) = { ( F ` X ) , ( F ` n ) } )
83 81 82 syl 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ { X , n } C_ ( ( iEdg ` G ) ` j ) /\ ( n e. V /\ X e. V ) ) -> ( F " { X , n } ) = { ( F ` X ) , ( F ` n ) } )
84 imass2 
 |-  ( { X , n } C_ ( ( iEdg ` G ) ` j ) -> ( F " { X , n } ) C_ ( F " ( ( iEdg ` G ) ` j ) ) )
85 84 3ad2ant2 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ { X , n } C_ ( ( iEdg ` G ) ` j ) /\ ( n e. V /\ X e. V ) ) -> ( F " { X , n } ) C_ ( F " ( ( iEdg ` G ) ` j ) ) )
86 83 85 eqsstrrd 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ { X , n } C_ ( ( iEdg ` G ) ` j ) /\ ( n e. V /\ X e. V ) ) -> { ( F ` X ) , ( F ` n ) } C_ ( F " ( ( iEdg ` G ) ` j ) ) )
87 simp1r 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ { X , n } C_ ( ( iEdg ` G ) ` j ) /\ ( n e. V /\ X e. V ) ) -> ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) )
88 86 87 sseqtrrd 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ { X , n } C_ ( ( iEdg ` G ) ` j ) /\ ( n e. V /\ X e. V ) ) -> { ( F ` X ) , ( F ` n ) } C_ ( ( iEdg ` H ) ` ( g ` j ) ) )
89 59 71 88 rspcedvdw 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) /\ { X , n } C_ ( ( iEdg ` G ) ` j ) /\ ( n e. V /\ X e. V ) ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e )
90 89 3exp 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) ) -> ( { X , n } C_ ( ( iEdg ` G ) ` j ) -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
91 90 3adant3 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) /\ k = ( ( iEdg ` G ) ` j ) ) -> ( { X , n } C_ ( ( iEdg ` G ) ` j ) -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
92 58 91 sylbid 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) /\ k = ( ( iEdg ` G ) ` j ) ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
93 92 3exp 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) -> ( ( ( iEdg ` H ) ` ( g ` j ) ) = ( F " ( ( iEdg ` G ) ` j ) ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) )
94 56 93 syld 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) /\ X e. V /\ j e. dom ( iEdg ` G ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) )
95 94 3exp 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) -> ( X e. V -> ( j e. dom ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) ) ) )
96 95 com34 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. ( Edg ` G ) /\ ( G e. UHGraph /\ H e. UHGraph ) ) -> ( X e. V -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( j e. dom ( iEdg ` G ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) ) ) )
97 96 3exp 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( k e. ( Edg ` G ) -> ( ( G e. UHGraph /\ H e. UHGraph ) -> ( X e. V -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( g ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( j e. dom ( iEdg ` G ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) ) ) ) ) )
98 97 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. UHGraph ) -> ( X e. V -> ( k e. ( Edg ` G ) -> ( j e. dom ( iEdg ` G ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) ) ) ) ) )
99 98 expimpd 
 |-  ( 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. UHGraph ) -> ( X e. V -> ( k e. ( Edg ` G ) -> ( j e. dom ( iEdg ` G ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) ) ) ) ) )
100 99 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. UHGraph ) -> ( X e. V -> ( k e. ( Edg ` G ) -> ( j e. dom ( iEdg ` G ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) ) ) ) ) )
101 100 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. UHGraph ) -> ( X e. V -> ( k e. ( Edg ` G ) -> ( j e. dom ( iEdg ` G ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) ) ) ) )
102 101 3imp 
 |-  ( ( ( 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. UHGraph ) /\ X e. V ) -> ( k e. ( Edg ` G ) -> ( j e. dom ( iEdg ` G ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) ) ) )
103 102 imp31 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ k e. ( Edg ` G ) ) /\ j e. dom ( iEdg ` G ) ) -> ( k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) )
104 103 rexlimdva 
 |-  ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ k e. ( Edg ` G ) ) -> ( E. j e. dom ( iEdg ` G ) k = ( ( iEdg ` G ) ` j ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) )
105 50 104 mpd 
 |-  ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ k e. ( Edg ` G ) ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
106 105 ex 
 |-  ( ( ( 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. UHGraph ) /\ X e. V ) -> ( k e. ( Edg ` G ) -> ( { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) )
107 106 com14 
 |-  ( ( n e. V /\ X e. V ) -> ( k e. ( Edg ` G ) -> ( { X , n } C_ k -> ( ( ( 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. UHGraph ) /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) )
108 107 imp 
 |-  ( ( ( n e. V /\ X e. V ) /\ k e. ( Edg ` G ) ) -> ( { X , n } C_ k -> ( ( ( 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. UHGraph ) /\ X e. V ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
109 108 3imp 
 |-  ( ( ( ( n e. V /\ X e. V ) /\ k e. ( Edg ` G ) ) /\ { X , n } C_ k /\ ( ( 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. UHGraph ) /\ X e. V ) ) -> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e )
110 109 olcd 
 |-  ( ( ( ( n e. V /\ X e. V ) /\ k e. ( Edg ` G ) ) /\ { X , n } C_ k /\ ( ( 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. UHGraph ) /\ X e. V ) ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) )
111 110 3exp 
 |-  ( ( ( n e. V /\ X e. V ) /\ k e. ( Edg ` G ) ) -> ( { X , n } C_ k -> ( ( ( 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. UHGraph ) /\ X e. V ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) )
112 111 rexlimdva 
 |-  ( ( n e. V /\ X e. V ) -> ( E. k e. ( Edg ` G ) { X , n } C_ k -> ( ( ( 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. UHGraph ) /\ X e. V ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) )
113 112 com12 
 |-  ( E. k e. ( Edg ` G ) { X , n } C_ k -> ( ( n e. V /\ X e. V ) -> ( ( ( 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. UHGraph ) /\ X e. V ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) )
114 46 113 jaoi 
 |-  ( ( n = X \/ E. k e. ( Edg ` G ) { X , n } C_ k ) -> ( ( n e. V /\ X e. V ) -> ( ( ( 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. UHGraph ) /\ X e. V ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) ) )
115 114 impcom 
 |-  ( ( ( n e. V /\ X e. V ) /\ ( n = X \/ E. k e. ( Edg ` G ) { X , n } C_ k ) ) -> ( ( ( 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. UHGraph ) /\ X e. V ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
116 43 115 sylbi 
 |-  ( n e. ( G ClNeighbVtx X ) -> ( ( ( 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. UHGraph ) /\ X e. V ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
117 116 impcom 
 |-  ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) )
118 117 adantr 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) )
119 eqeq1 
 |-  ( x = ( F ` n ) -> ( x = ( F ` X ) <-> ( F ` n ) = ( F ` X ) ) )
120 preq2 
 |-  ( x = ( F ` n ) -> { ( F ` X ) , x } = { ( F ` X ) , ( F ` n ) } )
121 120 sseq1d 
 |-  ( x = ( F ` n ) -> ( { ( F ` X ) , x } C_ e <-> { ( F ` X ) , ( F ` n ) } C_ e ) )
122 121 rexbidv 
 |-  ( x = ( F ` n ) -> ( E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e <-> E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) )
123 119 122 orbi12d 
 |-  ( x = ( F ` n ) -> ( ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) <-> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
124 123 eqcoms 
 |-  ( ( F ` n ) = x -> ( ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) <-> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
125 124 adantl 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> ( ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) <-> ( ( F ` n ) = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , ( F ` n ) } C_ e ) ) )
126 118 125 mpbird 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) )
127 38 41 126 jca31 
 |-  ( ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) /\ ( F ` n ) = x ) -> ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) )
128 127 ex 
 |-  ( ( ( ( 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. UHGraph ) /\ X e. V ) /\ n e. ( G ClNeighbVtx X ) ) -> ( ( F ` n ) = x -> ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) ) )
129 128 rexlimdva 
 |-  ( ( ( 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. UHGraph ) /\ X e. V ) -> ( E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x -> ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) ) )
130 26 129 syl3an1 
 |-  ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) -> ( E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x -> ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) ) )
131 23 130 impbid 
 |-  ( ( F e. ( G GraphIso H ) /\ ( G e. UHGraph /\ H e. UHGraph ) /\ X e. V ) -> ( ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) <-> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
132 131 3exp 
 |-  ( F e. ( G GraphIso H ) -> ( ( G e. UHGraph /\ H e. UHGraph ) -> ( X e. V -> ( ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) <-> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) ) ) )
133 132 impcom 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) -> ( X e. V -> ( ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) <-> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) ) )
134 133 imp 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) /\ X e. V ) -> ( ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) <-> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
135 16 17 clnbgrel 
 |-  ( x e. ( H ClNeighbVtx ( F ` X ) ) <-> ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) )
136 135 a1i 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) /\ X e. V ) -> ( x e. ( H ClNeighbVtx ( F ` X ) ) <-> ( ( x e. ( Vtx ` H ) /\ ( F ` X ) e. ( Vtx ` H ) ) /\ ( x = ( F ` X ) \/ E. e e. ( Edg ` H ) { ( F ` X ) , x } C_ e ) ) ) )
137 1 16 grimf1o 
 |-  ( F e. ( G GraphIso H ) -> F : V -1-1-onto-> ( Vtx ` H ) )
138 137 72 syl 
 |-  ( F e. ( G GraphIso H ) -> F Fn V )
139 138 adantl 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) -> F Fn V )
140 1 clnbgrssvtx 
 |-  ( G ClNeighbVtx X ) C_ V
141 140 a1i 
 |-  ( X e. V -> ( G ClNeighbVtx X ) C_ V )
142 fvelimab 
 |-  ( ( F Fn V /\ ( G ClNeighbVtx X ) C_ V ) -> ( x e. ( F " ( G ClNeighbVtx X ) ) <-> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
143 139 141 142 syl2an 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) /\ X e. V ) -> ( x e. ( F " ( G ClNeighbVtx X ) ) <-> E. n e. ( G ClNeighbVtx X ) ( F ` n ) = x ) )
144 134 136 143 3bitr4d 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) /\ X e. V ) -> ( x e. ( H ClNeighbVtx ( F ` X ) ) <-> x e. ( F " ( G ClNeighbVtx X ) ) ) )
145 144 eqrdv 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) /\ X e. V ) -> ( H ClNeighbVtx ( F ` X ) ) = ( F " ( G ClNeighbVtx X ) ) )