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 1elpr01 ⊢ 1 ∈ { 0 , 1 }
44 5nn ⊢ 5 ∈ ℕ
45 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 5 ) ↔ 5 ∈ ℕ )
46 44 45 mpbir ⊢ 0 ∈ ( 0 ..^ 5 )
47 43 46 opelxpii ⊢ ⟨ 1 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 5 ) )
48 1elfzo1ceilhalf1 ⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
49 16 48 ax-mp ⊢ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
50 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
51 eqid ⊢ ( 0 ..^ 5 ) = ( 0 ..^ 5 )
52 50 51 gpgvtx ⊢ ( ( 5 ∈ ℕ ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 5 ) ) )
53 44 49 52 mp2an ⊢ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 5 ) )
54 47 53 eleqtrri ⊢ ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) )
55 54 a1i ⊢ ( ⊤ → ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) )
56 1nn0 ⊢ 1 ∈ ℕ0
57 44 nnzi ⊢ 5 ∈ ℤ
58 1lt5 ⊢ 1 < 5
59 elfzo0z ⊢ ( 1 ∈ ( 0 ..^ 5 ) ↔ ( 1 ∈ ℕ0 ∧ 5 ∈ ℤ ∧ 1 < 5 ) )
60 56 57 58 59 mpbir3an ⊢ 1 ∈ ( 0 ..^ 5 )
61 43 60 opelxpii ⊢ ⟨ 1 , 1 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 5 ) )
62 61 53 eleqtrri ⊢ ⟨ 1 , 1 ⟩ ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) )
63 62 a1i ⊢ ( ⊤ → ⟨ 1 , 1 ⟩ ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) )
64 gpg5edgnedg ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) )
65 fvresi ⊢ ( ⟨ 1 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 5 ) ) → ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) = ⟨ 1 , 0 ⟩ )
66 47 65 ax-mp ⊢ ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) = ⟨ 1 , 0 ⟩
67 fvresi ⊢ ( ⟨ 1 , 1 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 5 ) ) → ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) = ⟨ 1 , 1 ⟩ )
68 61 67 ax-mp ⊢ ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) = ⟨ 1 , 1 ⟩
69 66 68 preq12i ⊢ { ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 0 ⟩ ) , ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ‘ ⟨ 1 , 1 ⟩ ) } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ }
70 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 ) ) ) )
71 69 70 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 ) ) )
72 71 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 ) ) ) )
73 64 72 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 ) ) )
74 73 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 ) ) ) )
75 26 33 40 42 55 63 74 3rspcedvdw ⊢ ( ⊤ → ∃ 𝑓 ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) ∃ 𝑎 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∃ 𝑏 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ) )
76 8 15 18 20 75 2rspcedvdw ⊢ ( ⊤ → ∃ 𝑔 ∈ USGraph ∃ ℎ ∈ USGraph ∃ 𝑓 ∈ ( 𝑔 GraphLocIso ℎ ) ∃ 𝑎 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝑔 ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) ) )
77 76 mptru ⊢ ∃ 𝑔 ∈ USGraph ∃ ℎ ∈ USGraph ∃ 𝑓 ∈ ( 𝑔 GraphLocIso ℎ ) ∃ 𝑎 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝑔 ) ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝑔 ) ∧ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∉ ( Edg ‘ ℎ ) )