Metamath Proof Explorer

Theorem grlimedgnedg

Description: In general, the image of an edge of a graph by a local isomprphism is not an edge of the other graph, proven by an example (see gpg5edgnedg ). This theorem proves that the analogon ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ ( F e. ( G GraphLocIso H ) /\ K e. I ) ) -> ( F " K ) e. E ) of grimedgi for ordinarily isomorphic graphs does not hold in general. (Contributed by AV, 30-Dec-2025)

Ref Expression
Assertion grlimedgnedg 
|- E. g e. USGraph E. h e. USGraph E. f e. ( g GraphLocIso h ) E. a e. ( Vtx ` g ) E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( g = ( 5 gPetersenGr 1 ) -> ( g GraphLocIso h ) = ( ( 5 gPetersenGr 1 ) GraphLocIso h ) )
2 fveq2 
 |-  ( g = ( 5 gPetersenGr 1 ) -> ( Vtx ` g ) = ( Vtx ` ( 5 gPetersenGr 1 ) ) )
3 fveq2 
 |-  ( g = ( 5 gPetersenGr 1 ) -> ( Edg ` g ) = ( Edg ` ( 5 gPetersenGr 1 ) ) )
4 3 eleq2d 
 |-  ( g = ( 5 gPetersenGr 1 ) -> ( { a , b } e. ( Edg ` g ) <-> { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) ) )
5 4 anbi1d 
 |-  ( g = ( 5 gPetersenGr 1 ) -> ( ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) )
6 2 5 rexeqbidv 
 |-  ( g = ( 5 gPetersenGr 1 ) -> ( E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) )
7 2 6 rexeqbidv 
 |-  ( g = ( 5 gPetersenGr 1 ) -> ( E. a e. ( Vtx ` g ) E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) )
8 1 7 rexeqbidv 
 |-  ( g = ( 5 gPetersenGr 1 ) -> ( E. f e. ( g GraphLocIso h ) E. a e. ( Vtx ` g ) E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso h ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) ) )
9 oveq2 
 |-  ( h = ( 5 gPetersenGr 2 ) -> ( ( 5 gPetersenGr 1 ) GraphLocIso h ) = ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) )
10 eqidd 
 |-  ( h = ( 5 gPetersenGr 2 ) -> { ( f ` a ) , ( f ` b ) } = { ( f ` a ) , ( f ` b ) } )
11 fveq2 
 |-  ( h = ( 5 gPetersenGr 2 ) -> ( Edg ` h ) = ( Edg ` ( 5 gPetersenGr 2 ) ) )
12 10 11 neleq12d 
 |-  ( h = ( 5 gPetersenGr 2 ) -> ( { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) <-> { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) )
13 12 anbi2d 
 |-  ( h = ( 5 gPetersenGr 2 ) -> ( ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) )
14 13 2rexbidv 
 |-  ( h = ( 5 gPetersenGr 2 ) -> ( E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) )
15 9 14 rexeqbidv 
 |-  ( h = ( 5 gPetersenGr 2 ) -> ( E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso h ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) <-> E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) )
16 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
17 gpgprismgrusgra 
 |-  ( 5 e. ( ZZ>= ` 3 ) -> ( 5 gPetersenGr 1 ) e. USGraph )
18 16 17 mp1i 
 |-  ( T. -> ( 5 gPetersenGr 1 ) e. USGraph )
19 pgjsgr 
 |-  ( 5 gPetersenGr 2 ) e. USGraph
20 19 a1i 
 |-  ( T. -> ( 5 gPetersenGr 2 ) e. USGraph )
21 fveq1 
 |-  ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( f ` a ) = ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) )
22 fveq1 
 |-  ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( f ` b ) = ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) )
23 21 22 preq12d 
 |-  ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> { ( f ` a ) , ( f ` b ) } = { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } )
24 eqidd 
 |-  ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) ) )
25 23 24 neleq12d 
 |-  ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) )
26 25 anbi2d 
 |-  ( f = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) -> ( ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) )
27 preq1 
 |-  ( a = <. 1 , 0 >. -> { a , b } = { <. 1 , 0 >. , b } )
28 27 eleq1d 
 |-  ( a = <. 1 , 0 >. -> ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) <-> { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) ) )
29 fveq2 
 |-  ( a = <. 1 , 0 >. -> ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) = ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) )
30 29 preq1d 
 |-  ( a = <. 1 , 0 >. -> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } = { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } )
31 eqidd 
 |-  ( a = <. 1 , 0 >. -> ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) ) )
32 30 31 neleq12d 
 |-  ( a = <. 1 , 0 >. -> ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) )
33 28 32 anbi12d 
 |-  ( a = <. 1 , 0 >. -> ( ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` a ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) )
34 preq2 
 |-  ( b = <. 1 , 1 >. -> { <. 1 , 0 >. , b } = { <. 1 , 0 >. , <. 1 , 1 >. } )
35 34 eleq1d 
 |-  ( b = <. 1 , 1 >. -> ( { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) <-> { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) ) )
36 fveq2 
 |-  ( b = <. 1 , 1 >. -> ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) = ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) )
37 36 preq2d 
 |-  ( b = <. 1 , 1 >. -> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } = { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } )
38 eqidd 
 |-  ( b = <. 1 , 1 >. -> ( Edg ` ( 5 gPetersenGr 2 ) ) = ( Edg ` ( 5 gPetersenGr 2 ) ) )
39 37 38 neleq12d 
 |-  ( b = <. 1 , 1 >. -> ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) )
40 35 39 anbi12d 
 |-  ( b = <. 1 , 1 >. -> ( ( { <. 1 , 0 >. , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) ) )
41 gpg5grlim 
 |-  ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) )
42 41 a1i 
 |-  ( T. -> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) )
43 1ex 
 |-  1 e. _V
44 43 prid2 
 |-  1 e. { 0 , 1 }
45 5nn 
 |-  5 e. NN
46 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 5 ) <-> 5 e. NN )
47 45 46 mpbir 
 |-  0 e. ( 0 ..^ 5 )
48 44 47 opelxpii 
 |-  <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ 5 ) )
49 1elfzo1ceilhalf1 
 |-  ( 5 e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
50 16 49 ax-mp 
 |-  1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
51 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
52 eqid 
 |-  ( 0 ..^ 5 ) = ( 0 ..^ 5 )
53 51 52 gpgvtx 
 |-  ( ( 5 e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) )
54 45 50 53 mp2an 
 |-  ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) )
55 48 54 eleqtrri 
 |-  <. 1 , 0 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) )
56 55 a1i 
 |-  ( T. -> <. 1 , 0 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) )
57 1nn0 
 |-  1 e. NN0
58 45 nnzi 
 |-  5 e. ZZ
59 1lt5 
 |-  1 < 5
60 elfzo0z 
 |-  ( 1 e. ( 0 ..^ 5 ) <-> ( 1 e. NN0 /\ 5 e. ZZ /\ 1 < 5 ) )
61 57 58 59 60 mpbir3an 
 |-  1 e. ( 0 ..^ 5 )
62 44 61 opelxpii 
 |-  <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ 5 ) )
63 62 54 eleqtrri 
 |-  <. 1 , 1 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) )
64 63 a1i 
 |-  ( T. -> <. 1 , 1 >. e. ( Vtx ` ( 5 gPetersenGr 1 ) ) )
65 gpg5edgnedg 
 |-  ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) )
66 fvresi 
 |-  ( <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ 5 ) ) -> ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) = <. 1 , 0 >. )
67 48 66 ax-mp 
 |-  ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) = <. 1 , 0 >.
68 fvresi 
 |-  ( <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ 5 ) ) -> ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) = <. 1 , 1 >. )
69 62 68 ax-mp 
 |-  ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) = <. 1 , 1 >.
70 67 69 preq12i 
 |-  { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } = { <. 1 , 0 >. , <. 1 , 1 >. }
71 neleq1 
 |-  ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } = { <. 1 , 0 >. , <. 1 , 1 >. } -> ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) )
72 70 71 ax-mp 
 |-  ( { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) <-> { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) )
73 72 anbi2i 
 |-  ( ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) <-> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { <. 1 , 0 >. , <. 1 , 1 >. } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) )
74 65 73 mpbir 
 |-  ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) )
75 74 a1i 
 |-  ( T. -> ( { <. 1 , 0 >. , <. 1 , 1 >. } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 0 >. ) , ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ` <. 1 , 1 >. ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) )
76 26 33 40 42 56 64 75 3rspcedvdw 
 |-  ( T. -> E. f e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) E. a e. ( Vtx ` ( 5 gPetersenGr 1 ) ) E. b e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( { a , b } e. ( Edg ` ( 5 gPetersenGr 1 ) ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` ( 5 gPetersenGr 2 ) ) ) )
77 8 15 18 20 76 2rspcedvdw 
 |-  ( T. -> E. g e. USGraph E. h e. USGraph E. f e. ( g GraphLocIso h ) E. a e. ( Vtx ` g ) E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) ) )
78 77 mptru 
 |-  E. g e. USGraph E. h e. USGraph E. f e. ( g GraphLocIso h ) E. a e. ( Vtx ` g ) E. b e. ( Vtx ` g ) ( { a , b } e. ( Edg ` g ) /\ { ( f ` a ) , ( f ` b ) } e/ ( Edg ` h ) )