Theorem grlimedgnedg 48485

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 48484). This theorem proves that the analogon (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ 𝐾 ∈ 𝐼)) → (𝐹 “ 𝐾) ∈ 𝐸) of grimedgi 48290 for ordinarily isomorphic graphs does not hold in general. (Contributed by AV, 30-Dec-2025.)

Assertion

Ref	Expression
grlimedgnedg	⊢ ∃𝑔 ∈ USGraph ∃ℎ ∈ USGraph ∃𝑓 ∈ (𝑔 GraphLocIso ℎ)∃𝑎 ∈ (Vtx‘𝑔)∃𝑏 ∈ (Vtx‘𝑔)({𝑎, 𝑏} ∈ (Edg‘𝑔) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ))

Distinct variable group:   𝑎,𝑏,𝑓,𝑔,ℎ

Proof of Theorem grlimedgnedg

Step	Hyp	Ref	Expression
1		oveq1 7375	. . . 4 ⊢ (𝑔 = (5 gPetersenGr 1) → (𝑔 GraphLocIso ℎ) = ((5 gPetersenGr 1) GraphLocIso ℎ))
2		fveq2 6842	. . . . 5 ⊢ (𝑔 = (5 gPetersenGr 1) → (Vtx‘𝑔) = (Vtx‘(5 gPetersenGr 1)))
3		fveq2 6842	. . . . . . . 8 ⊢ (𝑔 = (5 gPetersenGr 1) → (Edg‘𝑔) = (Edg‘(5 gPetersenGr 1)))
4	3	eleq2d 2823	. . . . . . 7 ⊢ (𝑔 = (5 gPetersenGr 1) → ({𝑎, 𝑏} ∈ (Edg‘𝑔) ↔ {𝑎, 𝑏} ∈ (Edg‘(5 gPetersenGr 1))))
5	4	anbi1d 632	. . . . . 6 ⊢ (𝑔 = (5 gPetersenGr 1) → (({𝑎, 𝑏} ∈ (Edg‘𝑔) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ)) ↔ ({𝑎, 𝑏} ∈ (Edg‘(5 gPetersenGr 1)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ))))
6	2, 5	rexeqbidv 3319	. . . . 5 ⊢ (𝑔 = (5 gPetersenGr 1) → (∃𝑏 ∈ (Vtx‘𝑔)({𝑎, 𝑏} ∈ (Edg‘𝑔) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ)) ↔ ∃𝑏 ∈ (Vtx‘(5 gPetersenGr 1))({𝑎, 𝑏} ∈ (Edg‘(5 gPetersenGr 1)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ))))
7	2, 6	rexeqbidv 3319	. . . 4 ⊢ (𝑔 = (5 gPetersenGr 1) → (∃𝑎 ∈ (Vtx‘𝑔)∃𝑏 ∈ (Vtx‘𝑔)({𝑎, 𝑏} ∈ (Edg‘𝑔) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ)) ↔ ∃𝑎 ∈ (Vtx‘(5 gPetersenGr 1))∃𝑏 ∈ (Vtx‘(5 gPetersenGr 1))({𝑎, 𝑏} ∈ (Edg‘(5 gPetersenGr 1)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ))))
8	1, 7	rexeqbidv 3319	. . 3 ⊢ (𝑔 = (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 7376	. . . 4 ⊢ (ℎ = (5 gPetersenGr 2) → ((5 gPetersenGr 1) GraphLocIso ℎ) = ((5 gPetersenGr 1) GraphLocIso (5 gPetersenGr 2)))
10		eqidd 2738	. . . . . . 7 ⊢ (ℎ = (5 gPetersenGr 2) → {(𝑓‘𝑎), (𝑓‘𝑏)} = {(𝑓‘𝑎), (𝑓‘𝑏)})
11		fveq2 6842	. . . . . . 7 ⊢ (ℎ = (5 gPetersenGr 2) → (Edg‘ℎ) = (Edg‘(5 gPetersenGr 2)))
12	10, 11	neleq12d 3042	. . . . . 6 ⊢ (ℎ = (5 gPetersenGr 2) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ) ↔ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘(5 gPetersenGr 2))))
13	12	anbi2d 631	. . . . 5 ⊢ (ℎ = (5 gPetersenGr 2) → (({𝑎, 𝑏} ∈ (Edg‘(5 gPetersenGr 1)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ)) ↔ ({𝑎, 𝑏} ∈ (Edg‘(5 gPetersenGr 1)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘(5 gPetersenGr 2)))))
14	13	2rexbidv 3203	. . . 4 ⊢ (ℎ = (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 3319	. . 3 ⊢ (ℎ = (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 12808	. . . 4 ⊢ 5 ∈ (ℤ≥‘3)
17		gpgprismgrusgra 48412	. . . 4 ⊢ (5 ∈ (ℤ≥‘3) → (5 gPetersenGr 1) ∈ USGraph)
18	16, 17	mp1i 13	. . 3 ⊢ (⊤ → (5 gPetersenGr 1) ∈ USGraph)
19		pgjsgr 48446	. . . 4 ⊢ (5 gPetersenGr 2) ∈ USGraph
20	19	a1i 11	. . 3 ⊢ (⊤ → (5 gPetersenGr 2) ∈ USGraph)
21		fveq1 6841	. . . . . . 7 ⊢ (𝑓 = ( I ↾ ({0, 1} × (0..^5))) → (𝑓‘𝑎) = (( I ↾ ({0, 1} × (0..^5)))‘𝑎))
22		fveq1 6841	. . . . . . 7 ⊢ (𝑓 = ( I ↾ ({0, 1} × (0..^5))) → (𝑓‘𝑏) = (( I ↾ ({0, 1} × (0..^5)))‘𝑏))
23	21, 22	preq12d 4700	. . . . . 6 ⊢ (𝑓 = ( I ↾ ({0, 1} × (0..^5))) → {(𝑓‘𝑎), (𝑓‘𝑏)} = {(( I ↾ ({0, 1} × (0..^5)))‘𝑎), (( I ↾ ({0, 1} × (0..^5)))‘𝑏)})
24		eqidd 2738	. . . . . 6 ⊢ (𝑓 = ( I ↾ ({0, 1} × (0..^5))) → (Edg‘(5 gPetersenGr 2)) = (Edg‘(5 gPetersenGr 2)))
25	23, 24	neleq12d 3042	. . . . 5 ⊢ (𝑓 = ( 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 631	. . . 4 ⊢ (𝑓 = ( 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 4692	. . . . . 6 ⊢ (𝑎 = ⟨1, 0⟩ → {𝑎, 𝑏} = {⟨1, 0⟩, 𝑏})
28	27	eleq1d 2822	. . . . 5 ⊢ (𝑎 = ⟨1, 0⟩ → ({𝑎, 𝑏} ∈ (Edg‘(5 gPetersenGr 1)) ↔ {⟨1, 0⟩, 𝑏} ∈ (Edg‘(5 gPetersenGr 1))))
29		fveq2 6842	. . . . . . 7 ⊢ (𝑎 = ⟨1, 0⟩ → (( I ↾ ({0, 1} × (0..^5)))‘𝑎) = (( I ↾ ({0, 1} × (0..^5)))‘⟨1, 0⟩))
30	29	preq1d 4698	. . . . . 6 ⊢ (𝑎 = ⟨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 2738	. . . . . 6 ⊢ (𝑎 = ⟨1, 0⟩ → (Edg‘(5 gPetersenGr 2)) = (Edg‘(5 gPetersenGr 2)))
32	30, 31	neleq12d 3042	. . . . 5 ⊢ (𝑎 = ⟨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 633	. . . 4 ⊢ (𝑎 = ⟨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 4693	. . . . . 6 ⊢ (𝑏 = ⟨1, 1⟩ → {⟨1, 0⟩, 𝑏} = {⟨1, 0⟩, ⟨1, 1⟩})
35	34	eleq1d 2822	. . . . 5 ⊢ (𝑏 = ⟨1, 1⟩ → ({⟨1, 0⟩, 𝑏} ∈ (Edg‘(5 gPetersenGr 1)) ↔ {⟨1, 0⟩, ⟨1, 1⟩} ∈ (Edg‘(5 gPetersenGr 1))))
36		fveq2 6842	. . . . . . 7 ⊢ (𝑏 = ⟨1, 1⟩ → (( I ↾ ({0, 1} × (0..^5)))‘𝑏) = (( I ↾ ({0, 1} × (0..^5)))‘⟨1, 1⟩))
37	36	preq2d 4699	. . . . . 6 ⊢ (𝑏 = ⟨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 2738	. . . . . 6 ⊢ (𝑏 = ⟨1, 1⟩ → (Edg‘(5 gPetersenGr 2)) = (Edg‘(5 gPetersenGr 2)))
39	37, 38	neleq12d 3042	. . . . 5 ⊢ (𝑏 = ⟨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 633	. . . 4 ⊢ (𝑏 = ⟨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 48447	. . . . 5 ⊢ ( I ↾ ({0, 1} × (0..^5))) ∈ ((5 gPetersenGr 1) GraphLocIso (5 gPetersenGr 2))
42	41	a1i 11	. . . 4 ⊢ (⊤ → ( I ↾ ({0, 1} × (0..^5))) ∈ ((5 gPetersenGr 1) GraphLocIso (5 gPetersenGr 2)))
43		1ex 11140	. . . . . . . 8 ⊢ 1 ∈ V
44	43	prid2 4722	. . . . . . 7 ⊢ 1 ∈ {0, 1}
45		5nn 12243	. . . . . . . 8 ⊢ 5 ∈ ℕ
46		lbfzo0 13627	. . . . . . . 8 ⊢ (0 ∈ (0..^5) ↔ 5 ∈ ℕ)
47	45, 46	mpbir 231	. . . . . . 7 ⊢ 0 ∈ (0..^5)
48	44, 47	opelxpii 5670	. . . . . 6 ⊢ ⟨1, 0⟩ ∈ ({0, 1} × (0..^5))
49		1elfzo1ceilhalf1 47691	. . . . . . . 8 ⊢ (5 ∈ (ℤ≥‘3) → 1 ∈ (1..^(⌈‘(5 / 2))))
50	16, 49	ax-mp 5	. . . . . . 7 ⊢ 1 ∈ (1..^(⌈‘(5 / 2)))
51		eqid 2737	. . . . . . . 8 ⊢ (1..^(⌈‘(5 / 2))) = (1..^(⌈‘(5 / 2)))
52		eqid 2737	. . . . . . . 8 ⊢ (0..^5) = (0..^5)
53	51, 52	gpgvtx 48397	. . . . . . 7 ⊢ ((5 ∈ ℕ ∧ 1 ∈ (1..^(⌈‘(5 / 2)))) → (Vtx‘(5 gPetersenGr 1)) = ({0, 1} × (0..^5)))
54	45, 50, 53	mp2an 693	. . . . . 6 ⊢ (Vtx‘(5 gPetersenGr 1)) = ({0, 1} × (0..^5))
55	48, 54	eleqtrri 2836	. . . . 5 ⊢ ⟨1, 0⟩ ∈ (Vtx‘(5 gPetersenGr 1))
56	55	a1i 11	. . . 4 ⊢ (⊤ → ⟨1, 0⟩ ∈ (Vtx‘(5 gPetersenGr 1)))
57		1nn0 12429	. . . . . . . 8 ⊢ 1 ∈ ℕ0
58	45	nnzi 12527	. . . . . . . 8 ⊢ 5 ∈ ℤ
59		1lt5 12332	. . . . . . . 8 ⊢ 1 < 5
60		elfzo0z 13629	. . . . . . . 8 ⊢ (1 ∈ (0..^5) ↔ (1 ∈ ℕ0 ∧ 5 ∈ ℤ ∧ 1 < 5))
61	57, 58, 59, 60	mpbir3an 1343	. . . . . . 7 ⊢ 1 ∈ (0..^5)
62	44, 61	opelxpii 5670	. . . . . 6 ⊢ ⟨1, 1⟩ ∈ ({0, 1} × (0..^5))
63	62, 54	eleqtrri 2836	. . . . 5 ⊢ ⟨1, 1⟩ ∈ (Vtx‘(5 gPetersenGr 1))
64	63	a1i 11	. . . 4 ⊢ (⊤ → ⟨1, 1⟩ ∈ (Vtx‘(5 gPetersenGr 1)))
65		gpg5edgnedg 48484	. . . . . 6 ⊢ ({⟨1, 0⟩, ⟨1, 1⟩} ∈ (Edg‘(5 gPetersenGr 1)) ∧ {⟨1, 0⟩, ⟨1, 1⟩} ∉ (Edg‘(5 gPetersenGr 2)))
66		fvresi 7129	. . . . . . . . . 10 ⊢ (⟨1, 0⟩ ∈ ({0, 1} × (0..^5)) → (( I ↾ ({0, 1} × (0..^5)))‘⟨1, 0⟩) = ⟨1, 0⟩)
67	48, 66	ax-mp 5	. . . . . . . . 9 ⊢ (( I ↾ ({0, 1} × (0..^5)))‘⟨1, 0⟩) = ⟨1, 0⟩
68		fvresi 7129	. . . . . . . . . 10 ⊢ (⟨1, 1⟩ ∈ ({0, 1} × (0..^5)) → (( I ↾ ({0, 1} × (0..^5)))‘⟨1, 1⟩) = ⟨1, 1⟩)
69	62, 68	ax-mp 5	. . . . . . . . 9 ⊢ (( I ↾ ({0, 1} × (0..^5)))‘⟨1, 1⟩) = ⟨1, 1⟩
70	67, 69	preq12i 4697	. . . . . . . 8 ⊢ {(( I ↾ ({0, 1} × (0..^5)))‘⟨1, 0⟩), (( I ↾ ({0, 1} × (0..^5)))‘⟨1, 1⟩)} = {⟨1, 0⟩, ⟨1, 1⟩}
71		neleq1 3043	. . . . . . . 8 ⊢ ({(( 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 5	. . . . . . 7 ⊢ ({(( 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 624	. . . . . 6 ⊢ (({⟨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 231	. . . . 5 ⊢ ({⟨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 11	. . . 4 ⊢ (⊤ → ({⟨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 3596	. . 3 ⊢ (⊤ → ∃𝑓 ∈ ((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 3592	. 2 ⊢ (⊤ → ∃𝑔 ∈ USGraph ∃ℎ ∈ USGraph ∃𝑓 ∈ (𝑔 GraphLocIso ℎ)∃𝑎 ∈ (Vtx‘𝑔)∃𝑏 ∈ (Vtx‘𝑔)({𝑎, 𝑏} ∈ (Edg‘𝑔) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ)))
78	77	mptru 1549	1 ⊢ ∃𝑔 ∈ USGraph ∃ℎ ∈ USGraph ∃𝑓 ∈ (𝑔 GraphLocIso ℎ)∃𝑎 ∈ (Vtx‘𝑔)∃𝑏 ∈ (Vtx‘𝑔)({𝑎, 𝑏} ∈ (Edg‘𝑔) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114   ∉ wnel 3037  ∃wrex 3062  {cpr 4584  ⟨cop 4588   class class class wbr 5100   I cid 5526   × cxp 5630   ↾ cres 5634  ‘cfv 6500  (class class class)co 7368  0cc0 11038  1c1 11039   < clt 11178   / cdiv 11806  ℕcn 12157  2c2 12212  3c3 12213  5c5 12215  ℕ₀cn0 12413  ℤcz 12500  ℤ_≥cuz 12763  ..^cfzo 13582  ⌈cceil 13723  Vtxcvtx 29081  Edgcedg 29132  USGraphcusgr 29234   GraphLocIso cgrlim 48330   gPetersenGr cgpg 48394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-oadd 8411  df-er 8645  df-map 8777  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-sup 9357  df-inf 9358  df-dju 9825  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-xnn0 12487  df-z 12501  df-dec 12620  df-uz 12764  df-rp 12918  df-ico 13279  df-fz 13436  df-fzo 13583  df-fl 13724  df-ceil 13725  df-mod 13802  df-seq 13937  df-exp 13997  df-hash 14266  df-cj 15034  df-re 15035  df-im 15036  df-sqrt 15170  df-abs 15171  df-dvds 16192  df-struct 17086  df-slot 17121  df-ndx 17133  df-base 17149  df-edgf 29074  df-vtx 29083  df-iedg 29084  df-edg 29133  df-uhgr 29143  df-ushgr 29144  df-upgr 29167  df-umgr 29168  df-uspgr 29235  df-usgr 29236  df-subgr 29353  df-nbgr 29418  df-clnbgr 48173  df-isubgr 48215  df-grim 48232  df-gric 48235  df-stgr 48306  df-grlim 48332  df-gpg 48395

This theorem is referenced by: (None)