Metamath Proof Explorer

Theorem gricushgr

Description: The "is isomorphic to" relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022)

Ref Expression
Hypotheses gricushgr.v 
|- V = ( Vtx ` A )
gricushgr.w 
|- W = ( Vtx ` B )
gricushgr.e 
|- E = ( Edg ` A )
gricushgr.k 
|- K = ( Edg ` B )
Assertion gricushgr 
|- ( ( A e. USHGraph /\ B e. USHGraph ) -> ( A ~=gr B <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gricushgr.v 
 |-  V = ( Vtx ` A )
2 gricushgr.w 
 |-  W = ( Vtx ` B )
3 gricushgr.e 
 |-  E = ( Edg ` A )
4 gricushgr.k 
 |-  K = ( Edg ` B )
5 eqid 
 |-  ( iEdg ` A ) = ( iEdg ` A )
6 eqid 
 |-  ( iEdg ` B ) = ( iEdg ` B )
7 1 2 5 6 dfgric2 
 |-  ( ( A e. USHGraph /\ B e. USHGraph ) -> ( A ~=gr B <-> E. f ( f : V -1-1-onto-> W /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) ) )
8 fvex 
 |-  ( iEdg ` B ) e. _V
9 vex 
 |-  h e. _V
10 fvex 
 |-  ( iEdg ` A ) e. _V
11 10 cnvex 
 |-  `' ( iEdg ` A ) e. _V
12 9 11 coex 
 |-  ( h o. `' ( iEdg ` A ) ) e. _V
13 8 12 coex 
 |-  ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) e. _V
14 13 a1i 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) e. _V )
15 2 6 ushgrf 
 |-  ( B e. USHGraph -> ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-> ( ~P W \ { (/) } ) )
16 f1f1orn 
 |-  ( ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-> ( ~P W \ { (/) } ) -> ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> ran ( iEdg ` B ) )
17 15 16 syl 
 |-  ( B e. USHGraph -> ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> ran ( iEdg ` B ) )
18 edgval 
 |-  ( Edg ` B ) = ran ( iEdg ` B )
19 4 18 eqtri 
 |-  K = ran ( iEdg ` B )
20 f1oeq3 
 |-  ( K = ran ( iEdg ` B ) -> ( ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> K <-> ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> ran ( iEdg ` B ) ) )
21 19 20 ax-mp 
 |-  ( ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> K <-> ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> ran ( iEdg ` B ) )
22 17 21 sylibr 
 |-  ( B e. USHGraph -> ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> K )
23 22 ad3antlr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> K )
24 simprl 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) )
25 1 5 ushgrf 
 |-  ( A e. USHGraph -> ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-> ( ~P V \ { (/) } ) )
26 f1f1orn 
 |-  ( ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-> ( ~P V \ { (/) } ) -> ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` A ) )
27 25 26 syl 
 |-  ( A e. USHGraph -> ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` A ) )
28 edgval 
 |-  ( Edg ` A ) = ran ( iEdg ` A )
29 3 28 eqtri 
 |-  E = ran ( iEdg ` A )
30 f1oeq3 
 |-  ( E = ran ( iEdg ` A ) -> ( ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> E <-> ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` A ) ) )
31 29 30 ax-mp 
 |-  ( ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> E <-> ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` A ) )
32 27 31 sylibr 
 |-  ( A e. USHGraph -> ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> E )
33 f1ocnv 
 |-  ( ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> E -> `' ( iEdg ` A ) : E -1-1-onto-> dom ( iEdg ` A ) )
34 32 33 syl 
 |-  ( A e. USHGraph -> `' ( iEdg ` A ) : E -1-1-onto-> dom ( iEdg ` A ) )
35 34 ad3antrrr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> `' ( iEdg ` A ) : E -1-1-onto-> dom ( iEdg ` A ) )
36 f1oco 
 |-  ( ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ `' ( iEdg ` A ) : E -1-1-onto-> dom ( iEdg ` A ) ) -> ( h o. `' ( iEdg ` A ) ) : E -1-1-onto-> dom ( iEdg ` B ) )
37 24 35 36 syl2anc 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( h o. `' ( iEdg ` A ) ) : E -1-1-onto-> dom ( iEdg ` B ) )
38 f1oco 
 |-  ( ( ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> K /\ ( h o. `' ( iEdg ` A ) ) : E -1-1-onto-> dom ( iEdg ` B ) ) -> ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) : E -1-1-onto-> K )
39 23 37 38 syl2anc 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) : E -1-1-onto-> K )
40 29 eleq2i 
 |-  ( e e. E <-> e e. ran ( iEdg ` A ) )
41 f1fn 
 |-  ( ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-> ( ~P V \ { (/) } ) -> ( iEdg ` A ) Fn dom ( iEdg ` A ) )
42 25 41 syl 
 |-  ( A e. USHGraph -> ( iEdg ` A ) Fn dom ( iEdg ` A ) )
43 fvelrnb 
 |-  ( ( iEdg ` A ) Fn dom ( iEdg ` A ) -> ( e e. ran ( iEdg ` A ) <-> E. j e. dom ( iEdg ` A ) ( ( iEdg ` A ) ` j ) = e ) )
44 42 43 syl 
 |-  ( A e. USHGraph -> ( e e. ran ( iEdg ` A ) <-> E. j e. dom ( iEdg ` A ) ( ( iEdg ` A ) ` j ) = e ) )
45 44 ad3antrrr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( e e. ran ( iEdg ` A ) <-> E. j e. dom ( iEdg ` A ) ( ( iEdg ` A ) ` j ) = e ) )
46 fveq2 
 |-  ( i = j -> ( ( iEdg ` A ) ` i ) = ( ( iEdg ` A ) ` j ) )
47 46 imaeq2d 
 |-  ( i = j -> ( f " ( ( iEdg ` A ) ` i ) ) = ( f " ( ( iEdg ` A ) ` j ) ) )
48 2fveq3 
 |-  ( i = j -> ( ( iEdg ` B ) ` ( h ` i ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) )
49 47 48 eqeq12d 
 |-  ( i = j -> ( ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) <-> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) ) )
50 49 rspccv 
 |-  ( A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) -> ( j e. dom ( iEdg ` A ) -> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) ) )
51 50 ad2antll 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( j e. dom ( iEdg ` A ) -> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) ) )
52 51 imp 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) )
53 coass 
 |-  ( ( ( iEdg ` B ) o. h ) o. `' ( iEdg ` A ) ) = ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) )
54 53 eqcomi 
 |-  ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) = ( ( ( iEdg ` B ) o. h ) o. `' ( iEdg ` A ) )
55 54 fveq1i 
 |-  ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` ( ( iEdg ` A ) ` j ) ) = ( ( ( ( iEdg ` B ) o. h ) o. `' ( iEdg ` A ) ) ` ( ( iEdg ` A ) ` j ) )
56 dff1o4 
 |-  ( ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` A ) <-> ( ( iEdg ` A ) Fn dom ( iEdg ` A ) /\ `' ( iEdg ` A ) Fn ran ( iEdg ` A ) ) )
57 27 56 sylib 
 |-  ( A e. USHGraph -> ( ( iEdg ` A ) Fn dom ( iEdg ` A ) /\ `' ( iEdg ` A ) Fn ran ( iEdg ` A ) ) )
58 57 simprd 
 |-  ( A e. USHGraph -> `' ( iEdg ` A ) Fn ran ( iEdg ` A ) )
59 58 ad4antr 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> `' ( iEdg ` A ) Fn ran ( iEdg ` A ) )
60 f1of 
 |-  ( ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` A ) -> ( iEdg ` A ) : dom ( iEdg ` A ) --> ran ( iEdg ` A ) )
61 27 60 syl 
 |-  ( A e. USHGraph -> ( iEdg ` A ) : dom ( iEdg ` A ) --> ran ( iEdg ` A ) )
62 61 ad3antrrr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( iEdg ` A ) : dom ( iEdg ` A ) --> ran ( iEdg ` A ) )
63 62 ffvelcdmda 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) ` j ) e. ran ( iEdg ` A ) )
64 fvco2 
 |-  ( ( `' ( iEdg ` A ) Fn ran ( iEdg ` A ) /\ ( ( iEdg ` A ) ` j ) e. ran ( iEdg ` A ) ) -> ( ( ( ( iEdg ` B ) o. h ) o. `' ( iEdg ` A ) ) ` ( ( iEdg ` A ) ` j ) ) = ( ( ( iEdg ` B ) o. h ) ` ( `' ( iEdg ` A ) ` ( ( iEdg ` A ) ` j ) ) ) )
65 59 63 64 syl2anc 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( ( ( iEdg ` B ) o. h ) o. `' ( iEdg ` A ) ) ` ( ( iEdg ` A ) ` j ) ) = ( ( ( iEdg ` B ) o. h ) ` ( `' ( iEdg ` A ) ` ( ( iEdg ` A ) ` j ) ) ) )
66 32 ad3antrrr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> E )
67 f1ocnvfv1 
 |-  ( ( ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> E /\ j e. dom ( iEdg ` A ) ) -> ( `' ( iEdg ` A ) ` ( ( iEdg ` A ) ` j ) ) = j )
68 66 67 sylan 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( `' ( iEdg ` A ) ` ( ( iEdg ` A ) ` j ) ) = j )
69 68 fveq2d 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( ( iEdg ` B ) o. h ) ` ( `' ( iEdg ` A ) ` ( ( iEdg ` A ) ` j ) ) ) = ( ( ( iEdg ` B ) o. h ) ` j ) )
70 f1ofn 
 |-  ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) -> h Fn dom ( iEdg ` A ) )
71 70 ad2antrl 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> h Fn dom ( iEdg ` A ) )
72 fvco2 
 |-  ( ( h Fn dom ( iEdg ` A ) /\ j e. dom ( iEdg ` A ) ) -> ( ( ( iEdg ` B ) o. h ) ` j ) = ( ( iEdg ` B ) ` ( h ` j ) ) )
73 71 72 sylan 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( ( iEdg ` B ) o. h ) ` j ) = ( ( iEdg ` B ) ` ( h ` j ) ) )
74 65 69 73 3eqtrd 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( ( ( iEdg ` B ) o. h ) o. `' ( iEdg ` A ) ) ` ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) )
75 55 74 eqtr2id 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( iEdg ` B ) ` ( h ` j ) ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` ( ( iEdg ` A ) ` j ) ) )
76 75 ad2antrr 
 |-  ( ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) /\ ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) ) /\ ( ( iEdg ` A ) ` j ) = e ) -> ( ( iEdg ` B ) ` ( h ` j ) ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` ( ( iEdg ` A ) ` j ) ) )
77 imaeq2 
 |-  ( e = ( ( iEdg ` A ) ` j ) -> ( f " e ) = ( f " ( ( iEdg ` A ) ` j ) ) )
78 77 eqcoms 
 |-  ( ( ( iEdg ` A ) ` j ) = e -> ( f " e ) = ( f " ( ( iEdg ` A ) ` j ) ) )
79 simpr 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) /\ ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) ) -> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) )
80 78 79 sylan9eqr 
 |-  ( ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) /\ ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) ) /\ ( ( iEdg ` A ) ` j ) = e ) -> ( f " e ) = ( ( iEdg ` B ) ` ( h ` j ) ) )
81 fveq2 
 |-  ( e = ( ( iEdg ` A ) ` j ) -> ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` ( ( iEdg ` A ) ` j ) ) )
82 81 eqcoms 
 |-  ( ( ( iEdg ` A ) ` j ) = e -> ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` ( ( iEdg ` A ) ` j ) ) )
83 82 adantl 
 |-  ( ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) /\ ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) ) /\ ( ( iEdg ` A ) ` j ) = e ) -> ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` ( ( iEdg ` A ) ` j ) ) )
84 76 80 83 3eqtr4d 
 |-  ( ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) /\ ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) ) /\ ( ( iEdg ` A ) ` j ) = e ) -> ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) )
85 84 ex 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) /\ ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( h ` j ) ) ) -> ( ( ( iEdg ` A ) ` j ) = e -> ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) ) )
86 52 85 mpdan 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( ( iEdg ` A ) ` j ) = e -> ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) ) )
87 86 rexlimdva 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( E. j e. dom ( iEdg ` A ) ( ( iEdg ` A ) ` j ) = e -> ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) ) )
88 45 87 sylbid 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( e e. ran ( iEdg ` A ) -> ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) ) )
89 40 88 biimtrid 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( e e. E -> ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) ) )
90 89 ralrimiv 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> A. e e. E ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) )
91 39 90 jca 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) ) )
92 f1oeq1 
 |-  ( g = ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) -> ( g : E -1-1-onto-> K <-> ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) : E -1-1-onto-> K ) )
93 fveq1 
 |-  ( g = ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) -> ( g ` e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) )
94 93 eqeq2d 
 |-  ( g = ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) -> ( ( f " e ) = ( g ` e ) <-> ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) ) )
95 94 ralbidv 
 |-  ( g = ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) -> ( A. e e. E ( f " e ) = ( g ` e ) <-> A. e e. E ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) ) )
96 92 95 anbi12d 
 |-  ( g = ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) -> ( ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) <-> ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( ( ( iEdg ` B ) o. ( h o. `' ( iEdg ` A ) ) ) ` e ) ) ) )
97 14 91 96 spcedv 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) -> E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) )
98 97 ex 
 |-  ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) -> ( ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) -> E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) )
99 98 exlimdv 
 |-  ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) -> ( E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) -> E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) )
100 8 cnvex 
 |-  `' ( iEdg ` B ) e. _V
101 vex 
 |-  g e. _V
102 101 10 coex 
 |-  ( g o. ( iEdg ` A ) ) e. _V
103 100 102 coex 
 |-  ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) e. _V
104 103 a1i 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) e. _V )
105 17 ad3antlr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> ran ( iEdg ` B ) )
106 f1ocnv 
 |-  ( ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> ran ( iEdg ` B ) -> `' ( iEdg ` B ) : ran ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` B ) )
107 105 106 syl 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> `' ( iEdg ` B ) : ran ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` B ) )
108 f1oeq23 
 |-  ( ( E = ran ( iEdg ` A ) /\ K = ran ( iEdg ` B ) ) -> ( g : E -1-1-onto-> K <-> g : ran ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` B ) ) )
109 29 19 108 mp2an 
 |-  ( g : E -1-1-onto-> K <-> g : ran ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` B ) )
110 109 biimpi 
 |-  ( g : E -1-1-onto-> K -> g : ran ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` B ) )
111 110 ad2antrl 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> g : ran ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` B ) )
112 27 ad3antrrr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` A ) )
113 f1oco 
 |-  ( ( g : ran ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` B ) /\ ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` A ) ) -> ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` B ) )
114 111 112 113 syl2anc 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` B ) )
115 f1oco 
 |-  ( ( `' ( iEdg ` B ) : ran ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` B ) /\ ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) -1-1-onto-> ran ( iEdg ` B ) ) -> ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) )
116 107 114 115 syl2anc 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) )
117 61 ad2antrr 
 |-  ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) -> ( iEdg ` A ) : dom ( iEdg ` A ) --> ran ( iEdg ` A ) )
118 117 ffund 
 |-  ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) -> Fun ( iEdg ` A ) )
119 118 adantr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> Fun ( iEdg ` A ) )
120 fvelrn 
 |-  ( ( Fun ( iEdg ` A ) /\ i e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) )
121 119 120 sylan 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) )
122 29 raleqi 
 |-  ( A. e e. E ( f " e ) = ( g ` e ) <-> A. e e. ran ( iEdg ` A ) ( f " e ) = ( g ` e ) )
123 122 biimpi 
 |-  ( A. e e. E ( f " e ) = ( g ` e ) -> A. e e. ran ( iEdg ` A ) ( f " e ) = ( g ` e ) )
124 123 ad2antll 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> A. e e. ran ( iEdg ` A ) ( f " e ) = ( g ` e ) )
125 124 adantr 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) -> A. e e. ran ( iEdg ` A ) ( f " e ) = ( g ` e ) )
126 imaeq2 
 |-  ( e = ( ( iEdg ` A ) ` i ) -> ( f " e ) = ( f " ( ( iEdg ` A ) ` i ) ) )
127 fveq2 
 |-  ( e = ( ( iEdg ` A ) ` i ) -> ( g ` e ) = ( g ` ( ( iEdg ` A ) ` i ) ) )
128 126 127 eqeq12d 
 |-  ( e = ( ( iEdg ` A ) ` i ) -> ( ( f " e ) = ( g ` e ) <-> ( f " ( ( iEdg ` A ) ` i ) ) = ( g ` ( ( iEdg ` A ) ` i ) ) ) )
129 128 rspccva 
 |-  ( ( A. e e. ran ( iEdg ` A ) ( f " e ) = ( g ` e ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( f " ( ( iEdg ` A ) ` i ) ) = ( g ` ( ( iEdg ` A ) ` i ) ) )
130 125 129 sylan 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( f " ( ( iEdg ` A ) ` i ) ) = ( g ` ( ( iEdg ` A ) ` i ) ) )
131 feq3 
 |-  ( E = ran ( iEdg ` A ) -> ( ( iEdg ` A ) : dom ( iEdg ` A ) --> E <-> ( iEdg ` A ) : dom ( iEdg ` A ) --> ran ( iEdg ` A ) ) )
132 29 131 ax-mp 
 |-  ( ( iEdg ` A ) : dom ( iEdg ` A ) --> E <-> ( iEdg ` A ) : dom ( iEdg ` A ) --> ran ( iEdg ` A ) )
133 61 132 sylibr 
 |-  ( A e. USHGraph -> ( iEdg ` A ) : dom ( iEdg ` A ) --> E )
134 133 ad2antrr 
 |-  ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) -> ( iEdg ` A ) : dom ( iEdg ` A ) --> E )
135 f1ofn 
 |-  ( g : E -1-1-onto-> K -> g Fn E )
136 135 adantr 
 |-  ( ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) -> g Fn E )
137 134 136 anim12ci 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( g Fn E /\ ( iEdg ` A ) : dom ( iEdg ` A ) --> E ) )
138 137 ad2antrr 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( g Fn E /\ ( iEdg ` A ) : dom ( iEdg ` A ) --> E ) )
139 fnfco 
 |-  ( ( g Fn E /\ ( iEdg ` A ) : dom ( iEdg ` A ) --> E ) -> ( g o. ( iEdg ` A ) ) Fn dom ( iEdg ` A ) )
140 138 139 syl 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( g o. ( iEdg ` A ) ) Fn dom ( iEdg ` A ) )
141 simplr 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> i e. dom ( iEdg ` A ) )
142 fvco2 
 |-  ( ( ( g o. ( iEdg ` A ) ) Fn dom ( iEdg ` A ) /\ i e. dom ( iEdg ` A ) ) -> ( ( ( _I |` ran ( iEdg ` B ) ) o. ( g o. ( iEdg ` A ) ) ) ` i ) = ( ( _I |` ran ( iEdg ` B ) ) ` ( ( g o. ( iEdg ` A ) ) ` i ) ) )
143 140 141 142 syl2anc 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( ( _I |` ran ( iEdg ` B ) ) o. ( g o. ( iEdg ` A ) ) ) ` i ) = ( ( _I |` ran ( iEdg ` B ) ) ` ( ( g o. ( iEdg ` A ) ) ` i ) ) )
144 f1of 
 |-  ( ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> K -> ( iEdg ` B ) : dom ( iEdg ` B ) --> K )
145 22 144 syl 
 |-  ( B e. USHGraph -> ( iEdg ` B ) : dom ( iEdg ` B ) --> K )
146 145 ffund 
 |-  ( B e. USHGraph -> Fun ( iEdg ` B ) )
147 funcocnv2 
 |-  ( Fun ( iEdg ` B ) -> ( ( iEdg ` B ) o. `' ( iEdg ` B ) ) = ( _I |` ran ( iEdg ` B ) ) )
148 146 147 syl 
 |-  ( B e. USHGraph -> ( ( iEdg ` B ) o. `' ( iEdg ` B ) ) = ( _I |` ran ( iEdg ` B ) ) )
149 148 eqcomd 
 |-  ( B e. USHGraph -> ( _I |` ran ( iEdg ` B ) ) = ( ( iEdg ` B ) o. `' ( iEdg ` B ) ) )
150 149 ad5antlr 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( _I |` ran ( iEdg ` B ) ) = ( ( iEdg ` B ) o. `' ( iEdg ` B ) ) )
151 150 coeq1d 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( _I |` ran ( iEdg ` B ) ) o. ( g o. ( iEdg ` A ) ) ) = ( ( ( iEdg ` B ) o. `' ( iEdg ` B ) ) o. ( g o. ( iEdg ` A ) ) ) )
152 151 fveq1d 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( ( _I |` ran ( iEdg ` B ) ) o. ( g o. ( iEdg ` A ) ) ) ` i ) = ( ( ( ( iEdg ` B ) o. `' ( iEdg ` B ) ) o. ( g o. ( iEdg ` A ) ) ) ` i ) )
153 coass 
 |-  ( ( ( iEdg ` B ) o. `' ( iEdg ` B ) ) o. ( g o. ( iEdg ` A ) ) ) = ( ( iEdg ` B ) o. ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) )
154 153 fveq1i 
 |-  ( ( ( ( iEdg ` B ) o. `' ( iEdg ` B ) ) o. ( g o. ( iEdg ` A ) ) ) ` i ) = ( ( ( iEdg ` B ) o. ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ) ` i )
155 152 154 eqtrdi 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( ( _I |` ran ( iEdg ` B ) ) o. ( g o. ( iEdg ` A ) ) ) ` i ) = ( ( ( iEdg ` B ) o. ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ) ` i ) )
156 f1of 
 |-  ( g : E -1-1-onto-> K -> g : E --> K )
157 eqid 
 |-  E = E
158 157 19 feq23i 
 |-  ( g : E --> K <-> g : E --> ran ( iEdg ` B ) )
159 156 158 sylib 
 |-  ( g : E -1-1-onto-> K -> g : E --> ran ( iEdg ` B ) )
160 159 adantr 
 |-  ( ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) -> g : E --> ran ( iEdg ` B ) )
161 f1of 
 |-  ( ( iEdg ` A ) : dom ( iEdg ` A ) -1-1-onto-> E -> ( iEdg ` A ) : dom ( iEdg ` A ) --> E )
162 32 161 syl 
 |-  ( A e. USHGraph -> ( iEdg ` A ) : dom ( iEdg ` A ) --> E )
163 162 ad2antrr 
 |-  ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) -> ( iEdg ` A ) : dom ( iEdg ` A ) --> E )
164 fco 
 |-  ( ( g : E --> ran ( iEdg ` B ) /\ ( iEdg ` A ) : dom ( iEdg ` A ) --> E ) -> ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) --> ran ( iEdg ` B ) )
165 160 163 164 syl2anr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) --> ran ( iEdg ` B ) )
166 165 anim1i 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) --> ran ( iEdg ` B ) /\ i e. dom ( iEdg ` A ) ) )
167 166 adantr 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) --> ran ( iEdg ` B ) /\ i e. dom ( iEdg ` A ) ) )
168 ffvelcdm 
 |-  ( ( ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) --> ran ( iEdg ` B ) /\ i e. dom ( iEdg ` A ) ) -> ( ( g o. ( iEdg ` A ) ) ` i ) e. ran ( iEdg ` B ) )
169 167 168 syl 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( g o. ( iEdg ` A ) ) ` i ) e. ran ( iEdg ` B ) )
170 fvresi 
 |-  ( ( ( g o. ( iEdg ` A ) ) ` i ) e. ran ( iEdg ` B ) -> ( ( _I |` ran ( iEdg ` B ) ) ` ( ( g o. ( iEdg ` A ) ) ` i ) ) = ( ( g o. ( iEdg ` A ) ) ` i ) )
171 169 170 syl 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( _I |` ran ( iEdg ` B ) ) ` ( ( g o. ( iEdg ` A ) ) ` i ) ) = ( ( g o. ( iEdg ` A ) ) ` i ) )
172 162 ad3antrrr 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( iEdg ` A ) : dom ( iEdg ` A ) --> E )
173 172 anim1i 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) : dom ( iEdg ` A ) --> E /\ i e. dom ( iEdg ` A ) ) )
174 173 adantr 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( iEdg ` A ) : dom ( iEdg ` A ) --> E /\ i e. dom ( iEdg ` A ) ) )
175 fvco3 
 |-  ( ( ( iEdg ` A ) : dom ( iEdg ` A ) --> E /\ i e. dom ( iEdg ` A ) ) -> ( ( g o. ( iEdg ` A ) ) ` i ) = ( g ` ( ( iEdg ` A ) ` i ) ) )
176 174 175 syl 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( g o. ( iEdg ` A ) ) ` i ) = ( g ` ( ( iEdg ` A ) ` i ) ) )
177 171 176 eqtrd 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( _I |` ran ( iEdg ` B ) ) ` ( ( g o. ( iEdg ` A ) ) ` i ) ) = ( g ` ( ( iEdg ` A ) ` i ) ) )
178 143 155 177 3eqtr3rd 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( g ` ( ( iEdg ` A ) ` i ) ) = ( ( ( iEdg ` B ) o. ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ) ` i ) )
179 dff1o4 
 |-  ( ( iEdg ` B ) : dom ( iEdg ` B ) -1-1-onto-> K <-> ( ( iEdg ` B ) Fn dom ( iEdg ` B ) /\ `' ( iEdg ` B ) Fn K ) )
180 22 179 sylib 
 |-  ( B e. USHGraph -> ( ( iEdg ` B ) Fn dom ( iEdg ` B ) /\ `' ( iEdg ` B ) Fn K ) )
181 180 simprd 
 |-  ( B e. USHGraph -> `' ( iEdg ` B ) Fn K )
182 181 ad5antlr 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> `' ( iEdg ` B ) Fn K )
183 156 adantr 
 |-  ( ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) -> g : E --> K )
184 134 183 anim12ci 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( g : E --> K /\ ( iEdg ` A ) : dom ( iEdg ` A ) --> E ) )
185 184 ad2antrr 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( g : E --> K /\ ( iEdg ` A ) : dom ( iEdg ` A ) --> E ) )
186 fco 
 |-  ( ( g : E --> K /\ ( iEdg ` A ) : dom ( iEdg ` A ) --> E ) -> ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) --> K )
187 185 186 syl 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) --> K )
188 fnfco 
 |-  ( ( `' ( iEdg ` B ) Fn K /\ ( g o. ( iEdg ` A ) ) : dom ( iEdg ` A ) --> K ) -> ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) Fn dom ( iEdg ` A ) )
189 182 187 188 syl2anc 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) Fn dom ( iEdg ` A ) )
190 fvco2 
 |-  ( ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) Fn dom ( iEdg ` A ) /\ i e. dom ( iEdg ` A ) ) -> ( ( ( iEdg ` B ) o. ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ) ` i ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) )
191 189 141 190 syl2anc 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( ( ( iEdg ` B ) o. ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ) ` i ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) )
192 130 178 191 3eqtrd 
 |-  ( ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) /\ ( ( iEdg ` A ) ` i ) e. ran ( iEdg ` A ) ) -> ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) )
193 121 192 mpdan 
 |-  ( ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) )
194 193 ralrimiva 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) )
195 116 194 jca 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) ) )
196 f1oeq1 
 |-  ( h = ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) -> ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) <-> ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) ) )
197 fveq1 
 |-  ( h = ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) -> ( h ` i ) = ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) )
198 197 fveq2d 
 |-  ( h = ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) -> ( ( iEdg ` B ) ` ( h ` i ) ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) )
199 198 eqeq2d 
 |-  ( h = ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) -> ( ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) <-> ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) ) )
200 199 ralbidv 
 |-  ( h = ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) -> ( A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) <-> A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) ) )
201 196 200 anbi12d 
 |-  ( h = ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) -> ( ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) <-> ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( `' ( iEdg ` B ) o. ( g o. ( iEdg ` A ) ) ) ` i ) ) ) ) )
202 104 195 201 spcedv 
 |-  ( ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) /\ ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) )
203 202 ex 
 |-  ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) -> ( ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) )
204 203 exlimdv 
 |-  ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) -> ( E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) )
205 99 204 impbid 
 |-  ( ( ( A e. USHGraph /\ B e. USHGraph ) /\ f : V -1-1-onto-> W ) -> ( E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) <-> E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) )
206 205 pm5.32da 
 |-  ( ( A e. USHGraph /\ B e. USHGraph ) -> ( ( f : V -1-1-onto-> W /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) <-> ( f : V -1-1-onto-> W /\ E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) ) )
207 206 exbidv 
 |-  ( ( A e. USHGraph /\ B e. USHGraph ) -> ( E. f ( f : V -1-1-onto-> W /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( h ` i ) ) ) ) <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) ) )
208 7 207 bitrd 
 |-  ( ( A e. USHGraph /\ B e. USHGraph ) -> ( A ~=gr B <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : E -1-1-onto-> K /\ A. e e. E ( f " e ) = ( g ` e ) ) ) ) )