Metamath Proof Explorer

Theorem isuspgrim0

Description: An isomorphism of simple pseudographs is a bijection between their vertices which induces a bijection between their edges. (Contributed by AV, 21-Apr-2025)

Ref Expression
Hypotheses isusgrim.v 
|- V = ( Vtx ` G )
isusgrim.w 
|- W = ( Vtx ` H )
isusgrim.e 
|- E = ( Edg ` G )
isusgrim.d 
|- D = ( Edg ` H )
Assertion isuspgrim0 
|- ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> ( F e. ( G GraphIso H ) <-> ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) )

Proof

Step Hyp Ref Expression
1 isusgrim.v 
 |-  V = ( Vtx ` G )
2 isusgrim.w 
 |-  W = ( Vtx ` H )
3 isusgrim.e 
 |-  E = ( Edg ` G )
4 isusgrim.d 
 |-  D = ( Edg ` H )
5 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
6 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
7 1 2 5 6 isgrim 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> ( F e. ( G GraphIso H ) <-> ( F : V -1-1-onto-> W /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) ) )
8 3 eleq2i 
 |-  ( e e. E <-> e e. ( Edg ` G ) )
9 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
10 5 uhgredgiedgb 
 |-  ( G e. UHGraph -> ( e e. ( Edg ` G ) <-> E. k e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` k ) ) )
11 9 10 syl 
 |-  ( G e. USPGraph -> ( e e. ( Edg ` G ) <-> E. k e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` k ) ) )
12 8 11 bitrid 
 |-  ( G e. USPGraph -> ( e e. E <-> E. k e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` k ) ) )
13 12 3ad2ant1 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> ( e e. E <-> E. k e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` k ) ) )
14 13 ad2antrr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( e e. E <-> E. k e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` k ) ) )
15 14 biimpa 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ e e. E ) -> E. k e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` k ) )
16 2fveq3 
 |-  ( i = k -> ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( iEdg ` H ) ` ( j ` k ) ) )
17 fveq2 
 |-  ( i = k -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` k ) )
18 17 imaeq2d 
 |-  ( i = k -> ( F " ( ( iEdg ` G ) ` i ) ) = ( F " ( ( iEdg ` G ) ` k ) ) )
19 16 18 eqeq12d 
 |-  ( i = k -> ( ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) <-> ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) ) )
20 19 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 ) ) ) )
21 20 adantl 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ 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 ) ) ) )
22 uspgruhgr 
 |-  ( H e. USPGraph -> H e. UHGraph )
23 6 uhgrfun 
 |-  ( H e. UHGraph -> Fun ( iEdg ` H ) )
24 22 23 syl 
 |-  ( H e. USPGraph -> Fun ( iEdg ` H ) )
25 24 3ad2ant2 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> Fun ( iEdg ` H ) )
26 25 ad3antrrr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. dom ( iEdg ` G ) ) -> Fun ( iEdg ` H ) )
27 f1of 
 |-  ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) -> j : dom ( iEdg ` G ) --> dom ( iEdg ` H ) )
28 27 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> j : dom ( iEdg ` G ) --> dom ( iEdg ` H ) )
29 28 ffvelcdmda 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. dom ( iEdg ` G ) ) -> ( j ` k ) e. dom ( iEdg ` H ) )
30 6 iedgedg 
 |-  ( ( Fun ( iEdg ` H ) /\ ( j ` k ) e. dom ( iEdg ` H ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) e. ( Edg ` H ) )
31 26 29 30 syl2anc 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. dom ( iEdg ` G ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) e. ( Edg ` H ) )
32 4 eleq2i 
 |-  ( ( ( iEdg ` H ) ` ( j ` k ) ) e. D <-> ( ( iEdg ` H ) ` ( j ` k ) ) e. ( Edg ` H ) )
33 31 32 sylibr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. dom ( iEdg ` G ) ) -> ( ( iEdg ` H ) ` ( j ` k ) ) e. D )
34 eleq1 
 |-  ( ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) -> ( ( ( iEdg ` H ) ` ( j ` k ) ) e. D <-> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
35 33 34 syl5ibcom 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. dom ( iEdg ` G ) ) -> ( ( ( iEdg ` H ) ` ( j ` k ) ) = ( F " ( ( iEdg ` G ) ` k ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
36 21 35 syld 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) /\ k e. dom ( iEdg ` G ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
37 36 ex 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( k e. dom ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) ) )
38 37 com23 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( k e. dom ( iEdg ` G ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) ) )
39 38 impr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( k e. dom ( iEdg ` G ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
40 39 adantr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ e e. E ) -> ( k e. dom ( iEdg ` G ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
41 40 imp 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ e e. E ) /\ k e. dom ( iEdg ` G ) ) -> ( F " ( ( iEdg ` G ) ` k ) ) e. D )
42 imaeq2 
 |-  ( e = ( ( iEdg ` G ) ` k ) -> ( F " e ) = ( F " ( ( iEdg ` G ) ` k ) ) )
43 42 eleq1d 
 |-  ( e = ( ( iEdg ` G ) ` k ) -> ( ( F " e ) e. D <-> ( F " ( ( iEdg ` G ) ` k ) ) e. D ) )
44 41 43 syl5ibrcom 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ e e. E ) /\ k e. dom ( iEdg ` G ) ) -> ( e = ( ( iEdg ` G ) ` k ) -> ( F " e ) e. D ) )
45 44 rexlimdva 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ e e. E ) -> ( E. k e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` k ) -> ( F " e ) e. D ) )
46 15 45 mpd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ e e. E ) -> ( F " e ) e. D )
47 46 ralrimiva 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> A. e e. E ( F " e ) e. D )
48 4 eleq2i 
 |-  ( d e. D <-> d e. ( Edg ` H ) )
49 6 uhgredgiedgb 
 |-  ( H e. UHGraph -> ( d e. ( Edg ` H ) <-> E. k e. dom ( iEdg ` H ) d = ( ( iEdg ` H ) ` k ) ) )
50 22 49 syl 
 |-  ( H e. USPGraph -> ( d e. ( Edg ` H ) <-> E. k e. dom ( iEdg ` H ) d = ( ( iEdg ` H ) ` k ) ) )
51 48 50 bitrid 
 |-  ( H e. USPGraph -> ( d e. D <-> E. k e. dom ( iEdg ` H ) d = ( ( iEdg ` H ) ` k ) ) )
52 51 3ad2ant2 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> ( d e. D <-> E. k e. dom ( iEdg ` H ) d = ( ( iEdg ` H ) ` k ) ) )
53 52 ad2antrr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( d e. D <-> E. k e. dom ( iEdg ` H ) d = ( ( iEdg ` H ) ` k ) ) )
54 simprl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) )
55 f1ocnvdm 
 |-  ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ k e. dom ( iEdg ` H ) ) -> ( `' j ` k ) e. dom ( iEdg ` G ) )
56 54 55 sylan 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( `' j ` k ) e. dom ( iEdg ` G ) )
57 2fveq3 
 |-  ( i = ( `' j ` k ) -> ( ( iEdg ` H ) ` ( j ` i ) ) = ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) )
58 fveq2 
 |-  ( i = ( `' j ` k ) -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` ( `' j ` k ) ) )
59 58 imaeq2d 
 |-  ( i = ( `' j ` k ) -> ( F " ( ( iEdg ` G ) ` i ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) )
60 57 59 eqeq12d 
 |-  ( i = ( `' j ` k ) -> ( ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) <-> ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
61 60 rspccv 
 |-  ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
62 61 adantl 
 |-  ( ( 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 ` k ) e. dom ( iEdg ` G ) -> ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
63 62 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
64 63 adantr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
65 f1ocnvfv2 
 |-  ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ k e. dom ( iEdg ` H ) ) -> ( j ` ( `' j ` k ) ) = k )
66 54 65 sylan 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( j ` ( `' j ` k ) ) = k )
67 66 fveqeq2d 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) <-> ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
68 eqeq2 
 |-  ( ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> ( d = ( ( iEdg ` H ) ` k ) <-> d = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
69 68 adantl 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) -> ( d = ( ( iEdg ` H ) ` k ) <-> d = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) )
70 simpll1 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> G e. USPGraph )
71 3 5 uspgriedgedg 
 |-  ( ( G e. USPGraph /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> E! e e. E e = ( ( iEdg ` G ) ` ( `' j ` k ) ) )
72 70 56 71 syl2an2r 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> E! e e. E e = ( ( iEdg ` G ) ` ( `' j ` k ) ) )
73 eqcom 
 |-  ( ( ( iEdg ` G ) ` ( `' j ` k ) ) = e <-> e = ( ( iEdg ` G ) ` ( `' j ` k ) ) )
74 73 reubii 
 |-  ( E! e e. E ( ( iEdg ` G ) ` ( `' j ` k ) ) = e <-> E! e e. E e = ( ( iEdg ` G ) ` ( `' j ` k ) ) )
75 72 74 sylibr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> E! e e. E ( ( iEdg ` G ) ` ( `' j ` k ) ) = e )
76 f1of1 
 |-  ( F : V -1-1-onto-> W -> F : V -1-1-> W )
77 76 ad4antlr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ e e. E ) -> F : V -1-1-> W )
78 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
79 78 3ad2ant1 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> G e. UPGraph )
80 79 ad3antrrr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> G e. UPGraph )
81 80 56 jca 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( G e. UPGraph /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) )
82 81 adantr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ e e. E ) -> ( G e. UPGraph /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) )
83 1 5 upgrss 
 |-  ( ( G e. UPGraph /\ ( `' j ` k ) e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` ( `' j ` k ) ) C_ V )
84 82 83 syl 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ e e. E ) -> ( ( iEdg ` G ) ` ( `' j ` k ) ) C_ V )
85 8 biimpi 
 |-  ( e e. E -> e e. ( Edg ` G ) )
86 edgupgr 
 |-  ( ( G e. UPGraph /\ e e. ( Edg ` G ) ) -> ( e e. ~P ( Vtx ` G ) /\ e =/= (/) /\ ( # ` e ) <_ 2 ) )
87 80 85 86 syl2an 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ e e. E ) -> ( e e. ~P ( Vtx ` G ) /\ e =/= (/) /\ ( # ` e ) <_ 2 ) )
88 87 simp1d 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ e e. E ) -> e e. ~P ( Vtx ` G ) )
89 88 elpwid 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ e e. E ) -> e C_ ( Vtx ` G ) )
90 89 1 sseqtrrdi 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ e e. E ) -> e C_ V )
91 f1imaeq 
 |-  ( ( F : V -1-1-> W /\ ( ( ( iEdg ` G ) ` ( `' j ` k ) ) C_ V /\ e C_ V ) ) -> ( ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) = ( F " e ) <-> ( ( iEdg ` G ) ` ( `' j ` k ) ) = e ) )
92 77 84 90 91 syl12anc 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ e e. E ) -> ( ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) = ( F " e ) <-> ( ( iEdg ` G ) ` ( `' j ` k ) ) = e ) )
93 92 reubidva 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( E! e e. E ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) = ( F " e ) <-> E! e e. E ( ( iEdg ` G ) ` ( `' j ` k ) ) = e ) )
94 75 93 mpbird 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> E! e e. E ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) = ( F " e ) )
95 94 ad2antrr 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) /\ d = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) -> E! e e. E ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) = ( F " e ) )
96 eqeq1 
 |-  ( d = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> ( d = ( F " e ) <-> ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) = ( F " e ) ) )
97 96 reubidv 
 |-  ( d = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> ( E! e e. E d = ( F " e ) <-> E! e e. E ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) = ( F " e ) ) )
98 97 adantl 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) /\ d = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) -> ( E! e e. E d = ( F " e ) <-> E! e e. E ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) = ( F " e ) ) )
99 95 98 mpbird 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) /\ d = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) -> E! e e. E d = ( F " e ) )
100 99 ex 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) -> ( d = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> E! e e. E d = ( F " e ) ) )
101 69 100 sylbid 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) /\ ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) ) -> ( d = ( ( iEdg ` H ) ` k ) -> E! e e. E d = ( F " e ) ) )
102 101 ex 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( ( ( iEdg ` H ) ` k ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> ( d = ( ( iEdg ` H ) ` k ) -> E! e e. E d = ( F " e ) ) ) )
103 67 102 sylbid 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( ( ( iEdg ` H ) ` ( j ` ( `' j ` k ) ) ) = ( F " ( ( iEdg ` G ) ` ( `' j ` k ) ) ) -> ( d = ( ( iEdg ` H ) ` k ) -> E! e e. E d = ( F " e ) ) ) )
104 64 103 syld 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( ( `' j ` k ) e. dom ( iEdg ` G ) -> ( d = ( ( iEdg ` H ) ` k ) -> E! e e. E d = ( F " e ) ) ) )
105 56 104 mpd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) /\ k e. dom ( iEdg ` H ) ) -> ( d = ( ( iEdg ` H ) ` k ) -> E! e e. E d = ( F " e ) ) )
106 105 rexlimdva 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( E. k e. dom ( iEdg ` H ) d = ( ( iEdg ` H ) ` k ) -> E! e e. E d = ( F " e ) ) )
107 53 106 sylbid 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( d e. D -> E! e e. E d = ( F " e ) ) )
108 107 ralrimiv 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> A. d e. D E! e e. E d = ( F " e ) )
109 imaeq2 
 |-  ( x = e -> ( F " x ) = ( F " e ) )
110 109 cbvmptv 
 |-  ( x e. E |-> ( F " x ) ) = ( e e. E |-> ( F " e ) )
111 110 f1ompt 
 |-  ( ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D <-> ( A. e e. E ( F " e ) e. D /\ A. d e. D E! e e. E d = ( F " e ) ) )
112 47 108 111 sylanbrc 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) -> ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D )
113 112 ex 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D ) )
114 113 exlimdv 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) -> ( E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) -> ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D ) )
115 fvex 
 |-  ( iEdg ` G ) e. _V
116 115 dmex 
 |-  dom ( iEdg ` G ) e. _V
117 116 mptex 
 |-  ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) e. _V
118 117 a1i 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D ) -> ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) e. _V )
119 eqid 
 |-  ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) = ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) )
120 1 2 3 4 5 6 110 119 isuspgrim0lem 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D ) -> ( ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) )
121 f1oeq1 
 |-  ( j = ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) -> ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) <-> ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) ) )
122 fveq1 
 |-  ( j = ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) -> ( j ` i ) = ( ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) ` i ) )
123 122 fveqeq2d 
 |-  ( j = ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) -> ( ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) <-> ( ( iEdg ` H ) ` ( ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) )
124 123 ralbidv 
 |-  ( j = ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) -> ( A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) <-> A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) )
125 121 124 anbi12d 
 |-  ( j = ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) -> ( ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) <-> ( ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( ( e e. dom ( iEdg ` G ) |-> ( `' ( iEdg ` H ) ` ( ( x e. E |-> ( F " x ) ) ` ( ( iEdg ` G ) ` e ) ) ) ) ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) )
126 118 120 125 spcedv 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D ) -> 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 ) ) ) )
127 126 ex 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) -> ( ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D -> 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 ) ) ) ) )
128 114 127 impbid 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) -> ( E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) <-> ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D ) )
129 f1oeq1 
 |-  ( ( x e. E |-> ( F " x ) ) = ( e e. E |-> ( F " e ) ) -> ( ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D <-> ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) )
130 110 129 mp1i 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) -> ( ( x e. E |-> ( F " x ) ) : E -1-1-onto-> D <-> ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) )
131 128 130 bitrd 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) -> ( E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) <-> ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) )
132 131 pm5.32da 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> ( ( F : V -1-1-onto-> W /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) <-> ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) )
133 7 132 bitrd 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> ( F e. ( G GraphIso H ) <-> ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) )