Metamath Proof Explorer


Theorem isomushgr

Description: The isomorphy relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022)

Ref Expression
Hypotheses isomushgr.v
|- V = ( Vtx ` A )
isomushgr.w
|- W = ( Vtx ` B )
isomushgr.e
|- E = ( Edg ` A )
isomushgr.k
|- K = ( Edg ` B )
Assertion isomushgr
|- ( ( A e. USHGraph /\ B e. USHGraph ) -> ( A IsomGr 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 isomushgr.v
 |-  V = ( Vtx ` A )
2 isomushgr.w
 |-  W = ( Vtx ` B )
3 isomushgr.e
 |-  E = ( Edg ` A )
4 isomushgr.k
 |-  K = ( Edg ` B )
5 eqid
 |-  ( iEdg ` A ) = ( iEdg ` A )
6 eqid
 |-  ( iEdg ` B ) = ( iEdg ` B )
7 1 2 5 6 isomgr
 |-  ( ( A e. USHGraph /\ B e. USHGraph ) -> ( A IsomGr 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 ffvelrnda
 |-  ( ( ( ( ( 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 syl5bi
 |-  ( ( ( ( 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 ffvelrn
 |-  ( ( ( 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 IsomGr 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 ) ) ) ) )