Metamath Proof Explorer

Theorem uspgrimprop

Description: An isomorphism of simple pseudographs is a bijection between their vertices that preserves adjacency, i.e. there is an edge in one graph connecting one or two vertices iff there is an edge in the other graph connecting the vertices which are the images of the vertices. (Contributed by AV, 27-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 uspgrimprop 
|- ( ( G e. USPGraph /\ H e. USPGraph ) -> ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> W /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. 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 1 2 3 4 isuspgrim0 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. ( G GraphIso H ) ) -> ( F e. ( G GraphIso H ) <-> ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) )
6 5 3expa 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphIso H ) ) -> ( F e. ( G GraphIso H ) <-> ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) )
7 simprl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) -> F : V -1-1-onto-> W )
8 imaeq2 
 |-  ( e = { x , y } -> ( F " e ) = ( F " { x , y } ) )
9 eqidd 
 |-  ( ( F : V -1-1-onto-> W /\ { x , y } e. E ) -> ( e e. E |-> ( F " e ) ) = ( e e. E |-> ( F " e ) ) )
10 simpr 
 |-  ( ( F : V -1-1-onto-> W /\ { x , y } e. E ) -> { x , y } e. E )
11 f1ofun 
 |-  ( F : V -1-1-onto-> W -> Fun F )
12 zfpair2 
 |-  { x , y } e. _V
13 funimaexg 
 |-  ( ( Fun F /\ { x , y } e. _V ) -> ( F " { x , y } ) e. _V )
14 11 12 13 sylancl 
 |-  ( F : V -1-1-onto-> W -> ( F " { x , y } ) e. _V )
15 14 adantr 
 |-  ( ( F : V -1-1-onto-> W /\ { x , y } e. E ) -> ( F " { x , y } ) e. _V )
16 8 9 10 15 fvmptd4 
 |-  ( ( F : V -1-1-onto-> W /\ { x , y } e. E ) -> ( ( e e. E |-> ( F " e ) ) ` { x , y } ) = ( F " { x , y } ) )
17 16 ex 
 |-  ( F : V -1-1-onto-> W -> ( { x , y } e. E -> ( ( e e. E |-> ( F " e ) ) ` { x , y } ) = ( F " { x , y } ) ) )
18 17 adantr 
 |-  ( ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) -> ( { x , y } e. E -> ( ( e e. E |-> ( F " e ) ) ` { x , y } ) = ( F " { x , y } ) ) )
19 18 ad2antlr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( { x , y } e. E -> ( ( e e. E |-> ( F " e ) ) ` { x , y } ) = ( F " { x , y } ) ) )
20 19 imp 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( ( e e. E |-> ( F " e ) ) ` { x , y } ) = ( F " { x , y } ) )
21 f1of 
 |-  ( ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D -> ( e e. E |-> ( F " e ) ) : E --> D )
22 21 ad2antll 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) -> ( e e. E |-> ( F " e ) ) : E --> D )
23 ax-1 
 |-  ( (/) e/ D -> ( H e. USPGraph -> (/) e/ D ) )
24 nnel 
 |-  ( -. (/) e/ D <-> (/) e. D )
25 uspgruhgr 
 |-  ( H e. USPGraph -> H e. UHGraph )
26 uhgredgn0 
 |-  ( ( H e. UHGraph /\ (/) e. ( Edg ` H ) ) -> (/) e. ( ~P ( Vtx ` H ) \ { (/) } ) )
27 25 26 sylan 
 |-  ( ( H e. USPGraph /\ (/) e. ( Edg ` H ) ) -> (/) e. ( ~P ( Vtx ` H ) \ { (/) } ) )
28 neldifsn 
 |-  -. (/) e. ( ~P ( Vtx ` H ) \ { (/) } )
29 28 pm2.21i 
 |-  ( (/) e. ( ~P ( Vtx ` H ) \ { (/) } ) -> (/) e/ D )
30 27 29 syl 
 |-  ( ( H e. USPGraph /\ (/) e. ( Edg ` H ) ) -> (/) e/ D )
31 30 expcom 
 |-  ( (/) e. ( Edg ` H ) -> ( H e. USPGraph -> (/) e/ D ) )
32 31 4 eleq2s 
 |-  ( (/) e. D -> ( H e. USPGraph -> (/) e/ D ) )
33 24 32 sylbi 
 |-  ( -. (/) e/ D -> ( H e. USPGraph -> (/) e/ D ) )
34 23 33 pm2.61i 
 |-  ( H e. USPGraph -> (/) e/ D )
35 34 ad2antlr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) -> (/) e/ D )
36 22 35 jca 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) -> ( ( e e. E |-> ( F " e ) ) : E --> D /\ (/) e/ D ) )
37 36 adantr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( ( e e. E |-> ( F " e ) ) : E --> D /\ (/) e/ D ) )
38 feldmfvelcdm 
 |-  ( ( ( e e. E |-> ( F " e ) ) : E --> D /\ (/) e/ D ) -> ( { x , y } e. E <-> ( ( e e. E |-> ( F " e ) ) ` { x , y } ) e. D ) )
39 37 38 syl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( { x , y } e. E <-> ( ( e e. E |-> ( F " e ) ) ` { x , y } ) e. D ) )
40 39 biimpa 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( ( e e. E |-> ( F " e ) ) ` { x , y } ) e. D )
41 20 40 eqeltrrd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ { x , y } e. E ) -> ( F " { x , y } ) e. D )
42 imaeq2 
 |-  ( z = ( F " { x , y } ) -> ( `' F " z ) = ( `' F " ( F " { x , y } ) ) )
43 imaeq2 
 |-  ( e = y -> ( F " e ) = ( F " y ) )
44 43 cbvmptv 
 |-  ( e e. E |-> ( F " e ) ) = ( y e. E |-> ( F " y ) )
45 f1oeq1 
 |-  ( ( e e. E |-> ( F " e ) ) = ( y e. E |-> ( F " y ) ) -> ( ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D <-> ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D ) )
46 44 45 mp1i 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) -> ( ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D <-> ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D ) )
47 imaeq2 
 |-  ( e = x -> ( F " e ) = ( F " x ) )
48 47 cbvmptv 
 |-  ( e e. E |-> ( F " e ) ) = ( x e. E |-> ( F " x ) )
49 simpr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) -> F : V -1-1-onto-> W )
50 49 adantr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D ) -> F : V -1-1-onto-> W )
51 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
52 uhgredgss 
 |-  ( G e. UHGraph -> ( Edg ` G ) C_ ( ~P ( Vtx ` G ) \ { (/) } ) )
53 difss2 
 |-  ( ( Edg ` G ) C_ ( ~P ( Vtx ` G ) \ { (/) } ) -> ( Edg ` G ) C_ ~P ( Vtx ` G ) )
54 51 52 53 3syl 
 |-  ( G e. USPGraph -> ( Edg ` G ) C_ ~P ( Vtx ` G ) )
55 1 pweqi 
 |-  ~P V = ~P ( Vtx ` G )
56 54 3 55 3sstr4g 
 |-  ( G e. USPGraph -> E C_ ~P V )
57 56 adantr 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> E C_ ~P V )
58 57 ad2antrr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D ) -> E C_ ~P V )
59 f1ofo 
 |-  ( ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D -> ( y e. E |-> ( F " y ) ) : E -onto-> D )
60 44 rneqi 
 |-  ran ( e e. E |-> ( F " e ) ) = ran ( y e. E |-> ( F " y ) )
61 forn 
 |-  ( ( y e. E |-> ( F " y ) ) : E -onto-> D -> ran ( y e. E |-> ( F " y ) ) = D )
62 60 61 eqtrid 
 |-  ( ( y e. E |-> ( F " y ) ) : E -onto-> D -> ran ( e e. E |-> ( F " e ) ) = D )
63 59 62 syl 
 |-  ( ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D -> ran ( e e. E |-> ( F " e ) ) = D )
64 63 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D ) -> ran ( e e. E |-> ( F " e ) ) = D )
65 uhgredgss 
 |-  ( H e. UHGraph -> ( Edg ` H ) C_ ( ~P ( Vtx ` H ) \ { (/) } ) )
66 difss2 
 |-  ( ( Edg ` H ) C_ ( ~P ( Vtx ` H ) \ { (/) } ) -> ( Edg ` H ) C_ ~P ( Vtx ` H ) )
67 25 65 66 3syl 
 |-  ( H e. USPGraph -> ( Edg ` H ) C_ ~P ( Vtx ` H ) )
68 2 pweqi 
 |-  ~P W = ~P ( Vtx ` H )
69 67 4 68 3sstr4g 
 |-  ( H e. USPGraph -> D C_ ~P W )
70 69 adantl 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> D C_ ~P W )
71 70 ad2antrr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D ) -> D C_ ~P W )
72 64 71 eqsstrd 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D ) -> ran ( e e. E |-> ( F " e ) ) C_ ~P W )
73 1 fvexi 
 |-  V e. _V
74 73 a1i 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D ) -> V e. _V )
75 48 50 58 72 74 mptcnfimad 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) /\ ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D ) -> `' ( e e. E |-> ( F " e ) ) = ( z e. ran ( e e. E |-> ( F " e ) ) |-> ( `' F " z ) ) )
76 75 ex 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) -> ( ( y e. E |-> ( F " y ) ) : E -1-1-onto-> D -> `' ( e e. E |-> ( F " e ) ) = ( z e. ran ( e e. E |-> ( F " e ) ) |-> ( `' F " z ) ) ) )
77 46 76 sylbid 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F : V -1-1-onto-> W ) -> ( ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D -> `' ( e e. E |-> ( F " e ) ) = ( z e. ran ( e e. E |-> ( F " e ) ) |-> ( `' F " z ) ) ) )
78 77 impr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) -> `' ( e e. E |-> ( F " e ) ) = ( z e. ran ( e e. E |-> ( F " e ) ) |-> ( `' F " z ) ) )
79 78 ad2antrr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ ( F " { x , y } ) e. D ) -> `' ( e e. E |-> ( F " e ) ) = ( z e. ran ( e e. E |-> ( F " e ) ) |-> ( `' F " z ) ) )
80 f1ofo 
 |-  ( ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D -> ( e e. E |-> ( F " e ) ) : E -onto-> D )
81 forn 
 |-  ( ( e e. E |-> ( F " e ) ) : E -onto-> D -> ran ( e e. E |-> ( F " e ) ) = D )
82 81 eqcomd 
 |-  ( ( e e. E |-> ( F " e ) ) : E -onto-> D -> D = ran ( e e. E |-> ( F " e ) ) )
83 80 82 syl 
 |-  ( ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D -> D = ran ( e e. E |-> ( F " e ) ) )
84 83 adantl 
 |-  ( ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) -> D = ran ( e e. E |-> ( F " e ) ) )
85 84 ad2antlr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> D = ran ( e e. E |-> ( F " e ) ) )
86 85 eleq2d 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( ( F " { x , y } ) e. D <-> ( F " { x , y } ) e. ran ( e e. E |-> ( F " e ) ) ) )
87 86 biimpa 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ ( F " { x , y } ) e. D ) -> ( F " { x , y } ) e. ran ( e e. E |-> ( F " e ) ) )
88 dff1o2 
 |-  ( F : V -1-1-onto-> W <-> ( F Fn V /\ Fun `' F /\ ran F = W ) )
89 88 simp2bi 
 |-  ( F : V -1-1-onto-> W -> Fun `' F )
90 89 adantr 
 |-  ( ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) -> Fun `' F )
91 90 ad2antlr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> Fun `' F )
92 funimaexg 
 |-  ( ( Fun `' F /\ ( F " { x , y } ) e. D ) -> ( `' F " ( F " { x , y } ) ) e. _V )
93 91 92 sylan 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ ( F " { x , y } ) e. D ) -> ( `' F " ( F " { x , y } ) ) e. _V )
94 42 79 87 93 fvmptd4 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ ( F " { x , y } ) e. D ) -> ( `' ( e e. E |-> ( F " e ) ) ` ( F " { x , y } ) ) = ( `' F " ( F " { x , y } ) ) )
95 simplrr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D )
96 f1ocnvdm 
 |-  ( ( ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D /\ ( F " { x , y } ) e. D ) -> ( `' ( e e. E |-> ( F " e ) ) ` ( F " { x , y } ) ) e. E )
97 95 96 sylan 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ ( F " { x , y } ) e. D ) -> ( `' ( e e. E |-> ( F " e ) ) ` ( F " { x , y } ) ) e. E )
98 94 97 eqeltrrd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ ( F " { x , y } ) e. D ) -> ( `' F " ( F " { x , y } ) ) e. E )
99 f1of1 
 |-  ( F : V -1-1-onto-> W -> F : V -1-1-> W )
100 99 ad2antrl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) -> F : V -1-1-> W )
101 prssi 
 |-  ( ( x e. V /\ y e. V ) -> { x , y } C_ V )
102 f1imacnv 
 |-  ( ( F : V -1-1-> W /\ { x , y } C_ V ) -> ( `' F " ( F " { x , y } ) ) = { x , y } )
103 100 101 102 syl2an 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( `' F " ( F " { x , y } ) ) = { x , y } )
104 103 eqcomd 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> { x , y } = ( `' F " ( F " { x , y } ) ) )
105 104 eleq1d 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( { x , y } e. E <-> ( `' F " ( F " { x , y } ) ) e. E ) )
106 105 adantr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ ( F " { x , y } ) e. D ) -> ( { x , y } e. E <-> ( `' F " ( F " { x , y } ) ) e. E ) )
107 98 106 mpbird 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) /\ ( F " { x , y } ) e. D ) -> { x , y } e. E )
108 41 107 impbida 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( { x , y } e. E <-> ( F " { x , y } ) e. D ) )
109 f1ofn 
 |-  ( F : V -1-1-onto-> W -> F Fn V )
110 109 ad2antrl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) -> F Fn V )
111 110 anim1i 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( F Fn V /\ ( x e. V /\ y e. V ) ) )
112 3anass 
 |-  ( ( F Fn V /\ x e. V /\ y e. V ) <-> ( F Fn V /\ ( x e. V /\ y e. V ) ) )
113 111 112 sylibr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( F Fn V /\ x e. V /\ y e. V ) )
114 fnimapr 
 |-  ( ( F Fn V /\ x e. V /\ y e. V ) -> ( F " { x , y } ) = { ( F ` x ) , ( F ` y ) } )
115 113 114 syl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( F " { x , y } ) = { ( F ` x ) , ( F ` y ) } )
116 115 eleq1d 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( ( F " { x , y } ) e. D <-> { ( F ` x ) , ( F ` y ) } e. D ) )
117 108 116 bitrd 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) /\ ( x e. V /\ y e. V ) ) -> ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) )
118 117 ralrimivva 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) -> A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) )
119 7 118 jca 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) ) -> ( F : V -1-1-onto-> W /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) )
120 119 ex 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) -> ( F : V -1-1-onto-> W /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) ) )
121 120 adantr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphIso H ) ) -> ( ( F : V -1-1-onto-> W /\ ( e e. E |-> ( F " e ) ) : E -1-1-onto-> D ) -> ( F : V -1-1-onto-> W /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) ) )
122 6 121 sylbid 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphIso H ) ) -> ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> W /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) ) )
123 122 syldbl2 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphIso H ) ) -> ( F : V -1-1-onto-> W /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) )
124 123 ex 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> W /\ A. x e. V A. y e. V ( { x , y } e. E <-> { ( F ` x ) , ( F ` y ) } e. D ) ) ) )