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 ∃ 𝑔 ∈ USGraph ∃ ℎ ∈ USGraph ∃ 𝑓 ∈ ( 𝑔 GraphLocIso ℎ ) ∃ 𝑎 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝑔 ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑔 = ( 5 gPetersenGr 1 ) → ( 𝑔 GraphLocIso ℎ ) = ( ( 5 gPetersenGr 1 ) GraphLocIso ℎ ) )
2 fveq2 ⊢ ( 𝑔 = ( 5 gPetersenGr 1 ) → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ ( 5 gPetersenGr 1 ) ) )
3 fveq2 ⊢ ( 𝑔 = ( 5 gPetersenGr 1 ) → ( Edg ‘ 𝑔 ) = ( Edg ‘ ( 5 gPetersenGr 1 ) ) )
4 3 eleq2d ⊢ ( 𝑔 = ( 5 gPetersenGr 1 ) → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ↔ { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ) )
5 4 anbi1d ⊢ ( 𝑔 = ( 5 gPetersenGr 1 ) → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ↔ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ) )
6 2 5 rexeqbidv ⊢ ( 𝑔 = ( 5 gPetersenGr 1 ) → ( ∃ 𝑏 ∈ ( Vtx ‘ 𝑔 ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ↔ ∃ 𝑏 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ) )
7 2 6 rexeqbidv ⊢ ( 𝑔 = ( 5 gPetersenGr 1 ) → ( ∃ 𝑎 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝑔 ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ↔ ∃ 𝑎 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∃ 𝑏 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ) )
8 1 7 rexeqbidv ⊢ ( 𝑔 = ( 5 gPetersenGr 1 ) → ( ∃ 𝑓 ∈ ( 𝑔 GraphLocIso ℎ ) ∃ 𝑎 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝑔 ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ↔ ∃ 𝑓 ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ℎ ) ∃ 𝑎 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∃ 𝑏 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ) )
9 oveq2 ⊢ ( ℎ = ( 5 gPetersenGr 2 ) → ( ( 5 gPetersenGr 1 ) GraphLocIso ℎ ) = ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) )
10 eqidd ⊢ ( ℎ = ( 5 gPetersenGr 2 ) → { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } = { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } )
11 fveq2 ⊢ ( ℎ = ( 5 gPetersenGr 2 ) → ( Edg ‘ ℎ ) = ( Edg ‘ ( 5 gPetersenGr 2 ) ) )
12 10 11 neleq12d ⊢ ( ℎ = ( 5 gPetersenGr 2 ) → ( { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) )
13 12 anbi2d ⊢ ( ℎ = ( 5 gPetersenGr 2 ) → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ↔ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ) )
14 13 2rexbidv ⊢ ( ℎ = ( 5 gPetersenGr 2 ) → ( ∃ 𝑎 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∃ 𝑏 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ↔ ∃ 𝑎 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∃ 𝑏 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ) )
15 9 14 rexeqbidv ⊢ ( ℎ = ( 5 gPetersenGr 2 ) → ( ∃ 𝑓 ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ℎ ) ∃ 𝑎 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∃ 𝑏 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) ↔ ∃ 𝑓 ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) ∃ 𝑎 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∃ 𝑏 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ) )
16 5eluz3 ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
17 gpgprismgrusgra ⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) → ( 5 gPetersenGr 1 ) ∈ USGraph )
18 16 17 mp1i ⊢ ( ⊤ → ( 5 gPetersenGr 1 ) ∈ USGraph )
19 pgjsgr ⊢ ( 5 gPetersenGr 2 ) ∈ USGraph
20 19 a1i ⊢ ( ⊤ → ( 5 gPetersenGr 2 ) ∈ USGraph )
21 fveq1 ⊢ ( 𝑓 = ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) → ( 𝑓 ‘ 𝑎 ) = ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑎 ) )
22 fveq1 ⊢ ( 𝑓 = ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) → ( 𝑓 ‘ 𝑏 ) = ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) )
23 21 22 preq12d ⊢ ( 𝑓 = ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) → { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } = { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑎 ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } )
24 eqidd ⊢ ( 𝑓 = ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) → ( Edg ‘ ( 5 gPetersenGr 2 ) ) = ( Edg ‘ ( 5 gPetersenGr 2 ) ) )
25 23 24 neleq12d ⊢ ( 𝑓 = ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) → ( { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ↔ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑎 ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) )
26 25 anbi2d ⊢ ( 𝑓 = ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ↔ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑎 ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ) )
27 preq1 ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → { 𝑎 , 𝑏 } = { ⟨ 1 , 0 ⟩ , 𝑏 } )
28 27 eleq1d ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ↔ { ⟨ 1 , 0 ⟩ , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ) )
29 fveq2 ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑎 ) = ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) )
30 29 preq1d ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑎 ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } = { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } )
31 eqidd ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → ( Edg ‘ ( 5 gPetersenGr 2 ) ) = ( Edg ‘ ( 5 gPetersenGr 2 ) ) )
32 30 31 neleq12d ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → ( { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑎 ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ↔ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) )
33 28 32 anbi12d ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑎 ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ↔ ( { ⟨ 1 , 0 ⟩ , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ) )
34 preq2 ⊢ ( 𝑏 = ⟨ 1 , 1 ⟩ → { ⟨ 1 , 0 ⟩ , 𝑏 } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } )
35 34 eleq1d ⊢ ( 𝑏 = ⟨ 1 , 1 ⟩ → ( { ⟨ 1 , 0 ⟩ , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ↔ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ) )
36 fveq2 ⊢ ( 𝑏 = ⟨ 1 , 1 ⟩ → ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) = ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) )
37 36 preq2d ⊢ ( 𝑏 = ⟨ 1 , 1 ⟩ → { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } = { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } )
38 eqidd ⊢ ( 𝑏 = ⟨ 1 , 1 ⟩ → ( Edg ‘ ( 5 gPetersenGr 2 ) ) = ( Edg ‘ ( 5 gPetersenGr 2 ) ) )
39 37 38 neleq12d ⊢ ( 𝑏 = ⟨ 1 , 1 ⟩ → ( { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ↔ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) )
40 35 39 anbi12d ⊢ ( 𝑏 = ⟨ 1 , 1 ⟩ → ( ( { ⟨ 1 , 0 ⟩ , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ) )
41 gpg5grlim ⊢ ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) )
42 41 a1i ⊢ ( ⊤ → ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) )
43 1ex ⊢ 1 ∈ V
44 43 prid2 ⊢ 1 ∈ { 0 , 1 }
45 5nn ⊢ 5 ∈ ℕ
46 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 5 ) ↔ 5 ∈ ℕ )
47 45 46 mpbir ⊢ 0 ∈ ( 0 ..^ 5 )
48 44 47 opelxpii ⊢ ⟨ 1 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 5 ) )
49 1elfzo1ceilhalf1 ⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
50 16 49 ax-mp ⊢ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
51 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
52 eqid ⊢ ( 0 ..^ 5 ) = ( 0 ..^ 5 )
53 51 52 gpgvtx ⊢ ( ( 5 ∈ ℕ ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 5 ) ) )
54 45 50 53 mp2an ⊢ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 5 ) )
55 48 54 eleqtrri ⊢ ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) )
56 55 a1i ⊢ ( ⊤ → ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) )
57 1nn0 ⊢ 1 ∈ ℕ0
58 45 nnzi ⊢ 5 ∈ ℤ
59 1lt5 ⊢ 1 < 5
60 elfzo0z ⊢ ( 1 ∈ ( 0 ..^ 5 ) ↔ ( 1 ∈ ℕ0 ∧ 5 ∈ ℤ ∧ 1 < 5 ) )
61 57 58 59 60 mpbir3an ⊢ 1 ∈ ( 0 ..^ 5 )
62 44 61 opelxpii ⊢ ⟨ 1 , 1 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 5 ) )
63 62 54 eleqtrri ⊢ ⟨ 1 , 1 ⟩ ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) )
64 63 a1i ⊢ ( ⊤ → ⟨ 1 , 1 ⟩ ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) )
65 gpg5edgnedg ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) )
66 fvresi ⊢ ( ⟨ 1 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 5 ) ) → ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) = ⟨ 1 , 0 ⟩ )
67 48 66 ax-mp ⊢ ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) = ⟨ 1 , 0 ⟩
68 fvresi ⊢ ( ⟨ 1 , 1 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 5 ) ) → ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) = ⟨ 1 , 1 ⟩ )
69 62 68 ax-mp ⊢ ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) = ⟨ 1 , 1 ⟩
70 67 69 preq12i ⊢ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ }
71 neleq1 ⊢ ( { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } → ( { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ↔ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) )
72 70 71 ax-mp ⊢ ( { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ↔ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) )
73 72 anbi2i ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) )
74 65 73 mpbir ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) )
75 74 a1i ⊢ ( ⊤ → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) )
76 26 33 40 42 56 64 75 3rspcedvdw ⊢ ( ⊤ → ∃ 𝑓 ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) ∃ 𝑎 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∃ 𝑏 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) )
77 8 15 18 20 76 2rspcedvdw ⊢ ( ⊤ → ∃ 𝑔 ∈ USGraph ∃ ℎ ∈ USGraph ∃ 𝑓 ∈ ( 𝑔 GraphLocIso ℎ ) ∃ 𝑎 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝑔 ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) )
78 77 mptru ⊢ ∃ 𝑔 ∈ USGraph ∃ ℎ ∈ USGraph ∃ 𝑓 ∈ ( 𝑔 GraphLocIso ℎ ) ∃ 𝑎 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝑔 ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) )