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

Metamath Proof Explorer

Theorem grimedg

Description: For two isomorphic graphs, a set of vertices is an edge in one graph iff its image by a graph isomorphism is an edge of the other graph. (Contributed by AV, 7-Jun-2025)

Ref Expression
Hypotheses grimedg.v 
|- V = ( Vtx ` G )
grimedg.i 
|- I = ( Edg ` G )
grimedg.e 
|- E = ( Edg ` H )
Assertion grimedg 
|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) )

Proof

Step Hyp Ref Expression
1 grimedg.v 
 |-  V = ( Vtx ` G )
2 grimedg.i 
 |-  I = ( Edg ` G )
3 grimedg.e 
 |-  E = ( Edg ` H )
4 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
5 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
6 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
7 1 4 5 6 grimprop 
 |-  ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> ( Vtx ` H ) /\ 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 ) ) ) ) )
8 2 eleq2i 
 |-  ( K e. I <-> K e. ( Edg ` G ) )
9 5 uhgredgiedgb 
 |-  ( G e. UHGraph -> ( K e. ( Edg ` G ) <-> E. k e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` k ) ) )
10 9 ad2antll 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( K e. ( Edg ` G ) <-> E. k e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` k ) ) )
11 8 10 bitrid 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( K e. I <-> E. k e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` k ) ) )
12 2fveq3 
 |-  ( i = k -> ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( iEdg ` H ) ` ( j ` k ) ) )
13 fveq2 
 |-  ( i = k -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` k ) )
14 13 imaeq2d 
 |-  ( i = k -> ( F " ( ( iEdg ` G ) ` i ) ) = ( F " ( ( iEdg ` G ) ` k ) ) )
15 12 14 eqeq12d 
 |-  ( i = k -> ( ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) <-> ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) ) )
16 15 rspcv 
 |-  ( k e. dom ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) ) )
17 16 adantl 
 |-  ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) ) )
18 6 uhgrfun 
 |-  ( H e. UHGraph -> Fun ( iEdg ` H ) )
19 18 ad2antrr 
 |-  ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) -> Fun ( iEdg ` H ) )
20 f1of 
 |-  ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> j : dom ( iEdg ` G ) --> dom ( iEdg ` H ) )
21 20 ad2antll 
 |-  ( ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) ) -> j : dom ( iEdg ` G ) --> dom ( iEdg ` H ) )
22 simplr 
 |-  ( ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) ) -> k e. dom ( iEdg ` G ) )
23 21 22 ffvelcdmd 
 |-  ( ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) ) -> ( j ` k ) e. dom ( iEdg ` H ) )
24 6 iedgedg 
 |-  ( ( Fun ( iEdg ` H ) /\ ( j ` k ) e. dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) e. ( Edg ` H ) )
25 24 3 eleqtrrdi 
 |-  ( ( Fun ( iEdg ` H ) /\ ( j ` k ) e. dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) e. E )
26 19 23 25 syl2an2r 
 |-  ( ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) e. E )
27 eleq1 
 |-  ( ( F " ( ( iEdg ` G ) ` k ) ) = ( ( iEdg ` H ) ` ( j ` k ) ) -> ( ( F " ( ( iEdg ` G ) ` k ) ) e. E <-> ( ( iEdg ` H ) ` ( j ` k ) ) e. E ) )
28 27 eqcoms 
 |-  ( ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) -> ( ( F " ( ( iEdg ` G ) ` k ) ) e. E <-> ( ( iEdg ` H ) ` ( j ` k ) ) e. E ) )
29 26 28 syl5ibrcom 
 |-  ( ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) /\ ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) ) -> ( ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. E ) )
30 29 ex 
 |-  ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) -> ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. E ) ) )
31 30 com23 
 |-  ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) -> ( ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) -> ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. E ) ) )
32 17 31 syld 
 |-  ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. E ) ) )
33 32 com13 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. E ) ) )
34 33 impr 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` G ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. E ) )
35 34 impl 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. E )
36 35 adantr 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. E )
37 imaeq2 
 |-  ( K = ( ( iEdg ` G ) ` k ) -> ( F " K ) = ( F " ( ( iEdg ` G ) ` k ) ) )
38 37 eleq1d 
 |-  ( K = ( ( iEdg ` G ) ` k ) -> ( ( F " K ) e. E <-> ( F " ( ( iEdg ` G ) ` k ) ) e. E ) )
39 38 adantl 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> ( ( F " K ) e. E <-> ( F " ( ( iEdg ` G ) ` k ) ) e. E ) )
40 36 39 mpbird 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> ( F " K ) e. E )
41 1 5 uhgrss 
 |-  ( ( G e. UHGraph /\ k e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` k ) C_ V )
42 41 ex 
 |-  ( G e. UHGraph -> ( k e. dom ( iEdg ` G ) -> ( ( iEdg ` G ) ` k ) C_ V ) )
43 42 ad2antll 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( k e. dom ( iEdg ` G ) -> ( ( iEdg ` G ) ` k ) C_ V ) )
44 43 imp 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` k ) C_ V )
45 44 adantr 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> ( ( iEdg ` G ) ` k ) C_ V )
46 sseq1 
 |-  ( K = ( ( iEdg ` G ) ` k ) -> ( K C_ V <-> ( ( iEdg ` G ) ` k ) C_ V ) )
47 46 adantl 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> ( K C_ V <-> ( ( iEdg ` G ) ` k ) C_ V ) )
48 45 47 mpbird 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> K C_ V )
49 40 48 jca 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) /\ K = ( ( iEdg ` G ) ` k ) ) -> ( ( F " K ) e. E /\ K C_ V ) )
50 49 ex 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` G ) ) -> ( K = ( ( iEdg ` G ) ` k ) -> ( ( F " K ) e. E /\ K C_ V ) ) )
51 50 rexlimdva 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( E. k e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` k ) -> ( ( F " K ) e. E /\ K C_ V ) ) )
52 11 51 sylbid 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( K e. I -> ( ( F " K ) e. E /\ K C_ V ) ) )
53 3 eleq2i 
 |-  ( ( F " K ) e. E <-> ( F " K ) e. ( Edg ` H ) )
54 6 uhgredgiedgb 
 |-  ( H e. UHGraph -> ( ( F " K ) e. ( Edg ` H ) <-> E. k e. dom ( iEdg ` H ) ( F " K ) = ( ( iEdg ` H ) ` k ) ) )
55 54 ad2antrl 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( ( F " K ) e. ( Edg ` H ) <-> E. k e. dom ( iEdg ` H ) ( F " K ) = ( ( iEdg ` H ) ` k ) ) )
56 53 55 bitrid 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( ( F " K ) e. E <-> E. k e. dom ( iEdg ` H ) ( F " K ) = ( ( iEdg ` H ) ` k ) ) )
57 f1ofo 
 |-  ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> j : dom ( iEdg ` G ) -onto-> dom ( iEdg ` H ) )
58 57 adantr 
 |-  ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> j : dom ( iEdg ` G ) -onto-> dom ( iEdg ` H ) )
59 58 ad2antlr 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> j : dom ( iEdg ` G ) -onto-> dom ( iEdg ` H ) )
60 foelrn 
 |-  ( ( j : dom ( iEdg ` G ) -onto-> dom ( iEdg ` H ) /\ k e. dom ( iEdg ` H ) ) -> E. l e. dom ( iEdg ` G ) k = ( j ` l ) )
61 59 60 sylan 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` H ) ) -> E. l e. dom ( iEdg ` G ) k = ( j ` l ) )
62 2fveq3 
 |-  ( i = l -> ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( iEdg ` H ) ` ( j ` l ) ) )
63 fveq2 
 |-  ( i = l -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` l ) )
64 63 imaeq2d 
 |-  ( i = l -> ( F " ( ( iEdg ` G ) ` i ) ) = ( F " ( ( iEdg ` G ) ` l ) ) )
65 62 64 eqeq12d 
 |-  ( i = l -> ( ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) <-> ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) )
66 65 rspcv 
 |-  ( l e. dom ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) )
67 66 adantl 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` k ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ l e. dom ( iEdg ` G ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) )
68 fveq2 
 |-  ( k = ( j ` l ) -> ( ( iEdg ` H ) ` k ) = ( ( iEdg ` H ) ` ( j ` l ) ) )
69 68 eqeq2d 
 |-  ( k = ( j ` l ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) <-> ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) ) )
70 69 ad2antll 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) <-> ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) ) )
71 simpl 
 |-  ( ( H e. UHGraph /\ G e. UHGraph ) -> H e. UHGraph )
72 71 ad2antrl 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) -> H e. UHGraph )
73 simplrr 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> k e. dom ( iEdg ` H ) )
74 eleq1 
 |-  ( k = ( j ` l ) -> ( k e. dom ( iEdg ` H ) <-> ( j ` l ) e. dom ( iEdg ` H ) ) )
75 74 ad2antll 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( k e. dom ( iEdg ` H ) <-> ( j ` l ) e. dom ( iEdg ` H ) ) )
76 73 75 mpbid 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( j ` l ) e. dom ( iEdg ` H ) )
77 4 6 uhgrss 
 |-  ( ( H e. UHGraph /\ ( j ` l ) e. dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) ` ( j ` l ) ) C_ ( Vtx ` H ) )
78 72 76 77 syl2an2r 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( ( iEdg ` H ) ` ( j ` l ) ) C_ ( Vtx ` H ) )
79 78 ad2antrr 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) ) -> ( ( iEdg ` H ) ` ( j ` l ) ) C_ ( Vtx ` H ) )
80 sseq1 
 |-  ( ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) -> ( ( F " K ) C_ ( Vtx ` H ) <-> ( ( iEdg ` H ) ` ( j ` l ) ) C_ ( Vtx ` H ) ) )
81 80 adantl 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) ) -> ( ( F " K ) C_ ( Vtx ` H ) <-> ( ( iEdg ` H ) ` ( j ` l ) ) C_ ( Vtx ` H ) ) )
82 79 81 mpbird 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) ) -> ( F " K ) C_ ( Vtx ` H ) )
83 eqeq2 
 |-  ( ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) <-> ( F " K ) = ( F " ( ( iEdg ` G ) ` l ) ) ) )
84 83 adantl 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) <-> ( F " K ) = ( F " ( ( iEdg ` G ) ` l ) ) ) )
85 f1of1 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> F : V -1-1-> ( Vtx ` H ) )
86 85 ad3antrrr 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> F : V -1-1-> ( Vtx ` H ) )
87 86 ad3antrrr 
 |-  ( ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) C_ ( Vtx ` H ) ) /\ K C_ V ) -> F : V -1-1-> ( Vtx ` H ) )
88 simplr 
 |-  ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) -> G e. UHGraph )
89 88 adantl 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) -> G e. UHGraph )
90 simpl 
 |-  ( ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) -> l e. dom ( iEdg ` G ) )
91 1 5 uhgrss 
 |-  ( ( G e. UHGraph /\ l e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` l ) C_ V )
92 89 90 91 syl2an 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( ( iEdg ` G ) ` l ) C_ V )
93 92 ad2antrr 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) C_ ( Vtx ` H ) ) -> ( ( iEdg ` G ) ` l ) C_ V )
94 93 anim1ci 
 |-  ( ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) C_ ( Vtx ` H ) ) /\ K C_ V ) -> ( K C_ V /\ ( ( iEdg ` G ) ` l ) C_ V ) )
95 f1imaeq 
 |-  ( ( F : V -1-1-> ( Vtx ` H ) /\ ( K C_ V /\ ( ( iEdg ` G ) ` l ) C_ V ) ) -> ( ( F " K ) = ( F " ( ( iEdg ` G ) ` l ) ) <-> K = ( ( iEdg ` G ) ` l ) ) )
96 87 94 95 syl2anc 
 |-  ( ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) C_ ( Vtx ` H ) ) /\ K C_ V ) -> ( ( F " K ) = ( F " ( ( iEdg ` G ) ` l ) ) <-> K = ( ( iEdg ` G ) ` l ) ) )
97 5 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
98 97 ad2antlr 
 |-  ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) -> Fun ( iEdg ` G ) )
99 98 adantl 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) -> Fun ( iEdg ` G ) )
100 5 iedgedg 
 |-  ( ( Fun ( iEdg ` G ) /\ l e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` l ) e. ( Edg ` G ) )
101 99 90 100 syl2an 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( ( iEdg ` G ) ` l ) e. ( Edg ` G ) )
102 101 2 eleqtrrdi 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( ( iEdg ` G ) ` l ) e. I )
103 eleq1 
 |-  ( K = ( ( iEdg ` G ) ` l ) -> ( K e. I <-> ( ( iEdg ` G ) ` l ) e. I ) )
104 102 103 syl5ibrcom 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( K = ( ( iEdg ` G ) ` l ) -> K e. I ) )
105 104 ad3antrrr 
 |-  ( ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) C_ ( Vtx ` H ) ) /\ K C_ V ) -> ( K = ( ( iEdg ` G ) ` l ) -> K e. I ) )
106 96 105 sylbid 
 |-  ( ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) C_ ( Vtx ` H ) ) /\ K C_ V ) -> ( ( F " K ) = ( F " ( ( iEdg ` G ) ` l ) ) -> K e. I ) )
107 106 ex 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) C_ ( Vtx ` H ) ) -> ( K C_ V -> ( ( F " K ) = ( F " ( ( iEdg ` G ) ` l ) ) -> K e. I ) ) )
108 107 com23 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) C_ ( Vtx ` H ) ) -> ( ( F " K ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( K C_ V -> K e. I ) ) )
109 108 ex 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) -> ( ( F " K ) C_ ( Vtx ` H ) -> ( ( F " K ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( K C_ V -> K e. I ) ) ) )
110 109 com23 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) -> ( ( F " K ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( ( F " K ) C_ ( Vtx ` H ) -> ( K C_ V -> K e. I ) ) ) )
111 84 110 sylbid 
 |-  ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) -> ( ( F " K ) C_ ( Vtx ` H ) -> ( K C_ V -> K e. I ) ) ) )
112 111 imp 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) ) -> ( ( F " K ) C_ ( Vtx ` H ) -> ( K C_ V -> K e. I ) ) )
113 82 112 mpd 
 |-  ( ( ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) /\ ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) ) -> ( K C_ V -> K e. I ) )
114 113 exp31 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) -> ( K C_ V -> K e. I ) ) ) )
115 114 com23 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` ( j ` l ) ) -> ( ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( K C_ V -> K e. I ) ) ) )
116 70 115 sylbid 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( K C_ V -> K e. I ) ) ) )
117 116 exp31 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) -> ( ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( K C_ V -> K e. I ) ) ) ) ) )
118 117 com23 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) -> ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( K C_ V -> K e. I ) ) ) ) ) )
119 118 com24 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) -> ( ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) -> ( ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( K C_ V -> K e. I ) ) ) ) ) )
120 119 3imp 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` k ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) -> ( ( l e. dom ( iEdg ` G ) /\ k = ( j ` l ) ) -> ( ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( K C_ V -> K e. I ) ) ) )
121 120 expdimp 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` k ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ l e. dom ( iEdg ` G ) ) -> ( k = ( j ` l ) -> ( ( ( iEdg ` H ) ` ( j ` l ) ) = ( F " ( ( iEdg ` G ) ` l ) ) -> ( K C_ V -> K e. I ) ) ) )
122 67 121 syl5d 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` k ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) /\ l e. dom ( iEdg ` G ) ) -> ( k = ( j ` l ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( K C_ V -> K e. I ) ) ) )
123 122 rexlimdva 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ ( F " K ) = ( ( iEdg ` H ) ` k ) /\ ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) ) -> ( E. l e. dom ( iEdg ` G ) k = ( j ` l ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( K C_ V -> K e. I ) ) ) )
124 123 3exp 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) -> ( E. l e. dom ( iEdg ` G ) k = ( j ` l ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( K C_ V -> K e. I ) ) ) ) ) )
125 124 com25 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) -> ( E. l e. dom ( iEdg ` G ) k = ( j ` l ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( K C_ V -> K e. I ) ) ) ) ) )
126 125 impr 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( ( ( H e. UHGraph /\ G e. UHGraph ) /\ k e. dom ( iEdg ` H ) ) -> ( E. l e. dom ( iEdg ` G ) k = ( j ` l ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( K C_ V -> K e. I ) ) ) ) )
127 126 impl 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` H ) ) -> ( E. l e. dom ( iEdg ` G ) k = ( j ` l ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( K C_ V -> K e. I ) ) ) )
128 61 127 mpd 
 |-  ( ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) /\ k e. dom ( iEdg ` H ) ) -> ( ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( K C_ V -> K e. I ) ) )
129 128 rexlimdva 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( E. k e. dom ( iEdg ` H ) ( F " K ) = ( ( iEdg ` H ) ` k ) -> ( K C_ V -> K e. I ) ) )
130 56 129 sylbid 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( ( F " K ) e. E -> ( K C_ V -> K e. I ) ) )
131 130 impd 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( ( ( F " K ) e. E /\ K C_ V ) -> K e. I ) )
132 52 131 impbid 
 |-  ( ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ ( H e. UHGraph /\ G e. UHGraph ) ) -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) )
133 132 exp31 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( ( H e. UHGraph /\ G e. UHGraph ) -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) ) ) )
134 133 exlimdv 
 |-  ( F : V -1-1-onto-> ( Vtx ` H ) -> ( 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 ) ) ) -> ( ( H e. UHGraph /\ G e. UHGraph ) -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) ) ) )
135 134 imp 
 |-  ( ( F : V -1-1-onto-> ( Vtx ` H ) /\ 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 ) ) ) ) -> ( ( H e. UHGraph /\ G e. UHGraph ) -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) ) )
136 7 135 syl 
 |-  ( F e. ( G GraphIso H ) -> ( ( H e. UHGraph /\ G e. UHGraph ) -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) ) )
137 136 expd 
 |-  ( F e. ( G GraphIso H ) -> ( H e. UHGraph -> ( G e. UHGraph -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) ) ) )
138 137 com13 
 |-  ( G e. UHGraph -> ( H e. UHGraph -> ( F e. ( G GraphIso H ) -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) ) ) )
139 138 3imp 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) )