pgnbgreunbgr

Description: In a Petersen graph, two different neighbors of a vertex have exactly one common neighbor, which is the vertex itself. (Contributed by AV, 9-Nov-2025)

	Ref	Expression
Hypotheses	pgnbgreunbgr.g	No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
	pgnbgreunbgr.v	$⊢ V = Vtx (G)$
	pgnbgreunbgr.e	$⊢ E = Edg (G)$
	pgnbgreunbgr.n	$⊢ N = G NeighbVtx X$
Assertion	pgnbgreunbgr	$⊢ (K \in N \land L \in N \land K \neq L) \to \exists! x \in V \{\{K, x\}, \{x, L\}\} \subseteq E$

Proof

Step	Hyp	Ref	Expression
1		pgnbgreunbgr.g	Could not format G = ( 5 gPetersenGr 2 ) : No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
2		pgnbgreunbgr.v	$⊢ V = Vtx (G)$
3		pgnbgreunbgr.e	$⊢ E = Edg (G)$
4		pgnbgreunbgr.n	$⊢ N = G NeighbVtx X$
5		preq2	$⊢ x = X \to \{K, x\} = \{K, X\}$
6		preq1	$⊢ x = X \to \{x, L\} = \{X, L\}$
7	5 6	preq12d	$⊢ x = X \to \{\{K, x\}, \{x, L\}\} = \{\{K, X\}, \{X, L\}\}$
8	7	sseq1d	$⊢ x = X \to (\{\{K, x\}, \{x, L\}\} \subseteq E \leftrightarrow \{\{K, X\}, \{X, L\}\} \subseteq E)$
9		eqeq1	$⊢ x = X \to (x = y \leftrightarrow X = y)$
10	9	imbi2d	$⊢ x = X \to ((\{\{K, y\}, \{y, L\}\} \subseteq E \to x = y) \leftrightarrow (\{\{K, y\}, \{y, L\}\} \subseteq E \to X = y))$
11	10	ralbidv	$⊢ x = X \to (\forall y \in V (\{\{K, y\}, \{y, L\}\} \subseteq E \to x = y) \leftrightarrow \forall y \in V (\{\{K, y\}, \{y, L\}\} \subseteq E \to X = y))$
12	8 11	anbi12d	$⊢ x = X \to ((\{\{K, x\}, \{x, L\}\} \subseteq E \land \forall y \in V (\{\{K, y\}, \{y, L\}\} \subseteq E \to x = y)) \leftrightarrow (\{\{K, X\}, \{X, L\}\} \subseteq E \land \forall y \in V (\{\{K, y\}, \{y, L\}\} \subseteq E \to X = y)))$
13	4	eleq2i	$⊢ K \in N \leftrightarrow K \in (G NeighbVtx X)$
14	13	biimpi	$⊢ K \in N \to K \in (G NeighbVtx X)$
15	14	3ad2ant1	$⊢ (K \in N \land L \in N \land K \neq L) \to K \in (G NeighbVtx X)$
16		pgjsgr	Could not format ( 5 gPetersenGr 2 ) e. USGraph : No typesetting found for \|- ( 5 gPetersenGr 2 ) e. USGraph with typecode \|-
17	1 16	eqeltri	$⊢ G \in USGraph$
18	3	nbusgreledg	$⊢ G \in USGraph \to (K \in (G NeighbVtx X) \leftrightarrow \{K, X\} \in E)$
19	17 18	ax-mp	$⊢ K \in (G NeighbVtx X) \leftrightarrow \{K, X\} \in E$
20	15 19	sylib	$⊢ (K \in N \land L \in N \land K \neq L) \to \{K, X\} \in E$
21		usgrumgr	$⊢ G \in USGraph \to G \in UMGraph$
22	17 21	ax-mp	$⊢ G \in UMGraph$
23	20 22	jctil	$⊢ (K \in N \land L \in N \land K \neq L) \to (G \in UMGraph \land \{K, X\} \in E)$
24	2 3	umgrpredgv	$⊢ (G \in UMGraph \land \{K, X\} \in E) \to (K \in V \land X \in V)$
25		simpr	$⊢ (K \in V \land X \in V) \to X \in V$
26	23 24 25	3syl	$⊢ (K \in N \land L \in N \land K \neq L) \to X \in V$
27	4	eleq2i	$⊢ L \in N \leftrightarrow L \in (G NeighbVtx X)$
28	13 27	anbi12i	$⊢ (K \in N \land L \in N) \leftrightarrow (K \in (G NeighbVtx X) \land L \in (G NeighbVtx X))$
29	3	nbusgreledg	$⊢ G \in USGraph \to (L \in (G NeighbVtx X) \leftrightarrow \{L, X\} \in E)$
30		prcom	$⊢ \{L, X\} = \{X, L\}$
31	30	eleq1i	$⊢ \{L, X\} \in E \leftrightarrow \{X, L\} \in E$
32	29 31	bitrdi	$⊢ G \in USGraph \to (L \in (G NeighbVtx X) \leftrightarrow \{X, L\} \in E)$
33	18 32	anbi12d	$⊢ G \in USGraph \to ((K \in (G NeighbVtx X) \land L \in (G NeighbVtx X)) \leftrightarrow (\{K, X\} \in E \land \{X, L\} \in E))$
34	17 33	ax-mp	$⊢ (K \in (G NeighbVtx X) \land L \in (G NeighbVtx X)) \leftrightarrow (\{K, X\} \in E \land \{X, L\} \in E)$
35	28 34	sylbb	$⊢ (K \in N \land L \in N) \to (\{K, X\} \in E \land \{X, L\} \in E)$
36	35	3adant3	$⊢ (K \in N \land L \in N \land K \neq L) \to (\{K, X\} \in E \land \{X, L\} \in E)$
37		prssi	$⊢ (\{K, X\} \in E \land \{X, L\} \in E) \to \{\{K, X\}, \{X, L\}\} \subseteq E$
38	36 37	syl	$⊢ (K \in N \land L \in N \land K \neq L) \to \{\{K, X\}, \{X, L\}\} \subseteq E$
39		prex	$⊢ \{K, y\} \in V$
40		prex	$⊢ \{y, L\} \in V$
41	39 40	prss	$⊢ (\{K, y\} \in E \land \{y, L\} \in E) \leftrightarrow \{\{K, y\}, \{y, L\}\} \subseteq E$
42		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
43		pglem	$⊢ 2 \in (1 ..^⌈\frac{5}{2}⌉)$
44		eqid	$⊢ (0 ..^5) = (0 ..^5)$
45		eqid	$⊢ (1 ..^⌈\frac{5}{2}⌉) = (1 ..^⌈\frac{5}{2}⌉)$
46	44 45 1 2	gpgvtxel	$⊢ (5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \to (y \in V \leftrightarrow \exists a \in \{0, 1\} \exists b \in (0 ..^5) y = ⟨a, b⟩)$
47	42 43 46	mp2an	$⊢ y \in V \leftrightarrow \exists a \in \{0, 1\} \exists b \in (0 ..^5) y = ⟨a, b⟩$
48	47	biimpi	$⊢ y \in V \to \exists a \in \{0, 1\} \exists b \in (0 ..^5) y = ⟨a, b⟩$
49	48	adantl	$⊢ ((K \in N \land L \in N \land K \neq L) \land y \in V) \to \exists a \in \{0, 1\} \exists b \in (0 ..^5) y = ⟨a, b⟩$
50		opeq1	$⊢ a = 0 \to ⟨a, b⟩ = ⟨0, b⟩$
51	50	eqeq2d	$⊢ a = 0 \to (y = ⟨a, b⟩ \leftrightarrow y = ⟨0, b⟩)$
52	51	adantr	$⊢ (a = 0 \land (((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5))) \to (y = ⟨a, b⟩ \leftrightarrow y = ⟨0, b⟩)$
53	1 2 3 4	pgnbgreunbgrlem3	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)$
54	53	adantlr	$⊢ (((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)$
55		preq2	$⊢ y = ⟨0, b⟩ \to \{K, y\} = \{K, ⟨0, b⟩\}$
56	55	eleq1d	$⊢ y = ⟨0, b⟩ \to (\{K, y\} \in E \leftrightarrow \{K, ⟨0, b⟩\} \in E)$
57		preq1	$⊢ y = ⟨0, b⟩ \to \{y, L\} = \{⟨0, b⟩, L\}$
58	57	eleq1d	$⊢ y = ⟨0, b⟩ \to (\{y, L\} \in E \leftrightarrow \{⟨0, b⟩, L\} \in E)$
59	56 58	anbi12d	$⊢ y = ⟨0, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \leftrightarrow (\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E))$
60		eqeq2	$⊢ y = ⟨0, b⟩ \to (X = y \leftrightarrow X = ⟨0, b⟩)$
61	59 60	imbi12d	$⊢ y = ⟨0, b⟩ \to (((\{K, y\} \in E \land \{y, L\} \in E) \to X = y) \leftrightarrow ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))$
62	54 61	syl5ibrcom	$⊢ (((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5)) \to (y = ⟨0, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y))$
63	62	adantl	$⊢ (a = 0 \land (((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5))) \to (y = ⟨0, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y))$
64	52 63	sylbid	$⊢ (a = 0 \land (((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5))) \to (y = ⟨a, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y))$
65	64	ex	$⊢ a = 0 \to ((((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5)) \to (y = ⟨a, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y)))$
66	1 2 3 4	pgnbgreunbgrlem6	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$
67	66	adantlr	$⊢ (((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$
68		preq2	$⊢ y = ⟨1, b⟩ \to \{K, y\} = \{K, ⟨1, b⟩\}$
69	68	eleq1d	$⊢ y = ⟨1, b⟩ \to (\{K, y\} \in E \leftrightarrow \{K, ⟨1, b⟩\} \in E)$
70		preq1	$⊢ y = ⟨1, b⟩ \to \{y, L\} = \{⟨1, b⟩, L\}$
71	70	eleq1d	$⊢ y = ⟨1, b⟩ \to (\{y, L\} \in E \leftrightarrow \{⟨1, b⟩, L\} \in E)$
72	69 71	anbi12d	$⊢ y = ⟨1, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \leftrightarrow (\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E))$
73		eqeq2	$⊢ y = ⟨1, b⟩ \to (X = y \leftrightarrow X = ⟨1, b⟩)$
74	72 73	imbi12d	$⊢ y = ⟨1, b⟩ \to (((\{K, y\} \in E \land \{y, L\} \in E) \to X = y) \leftrightarrow ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
75	67 74	syl5ibrcom	$⊢ (((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5)) \to (y = ⟨1, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y))$
76		opeq1	$⊢ a = 1 \to ⟨a, b⟩ = ⟨1, b⟩$
77	76	eqeq2d	$⊢ a = 1 \to (y = ⟨a, b⟩ \leftrightarrow y = ⟨1, b⟩)$
78	77	imbi1d	$⊢ a = 1 \to ((y = ⟨a, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y)) \leftrightarrow (y = ⟨1, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y)))$
79	75 78	imbitrrid	$⊢ a = 1 \to ((((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5)) \to (y = ⟨a, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y)))$
80	65 79	jaoi	$⊢ (a = 0 \lor a = 1) \to ((((K \in N \land L \in N \land K \neq L) \land y \in V) \land b \in (0 ..^5)) \to (y = ⟨a, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y)))$
81	80	expd	$⊢ (a = 0 \lor a = 1) \to (((K \in N \land L \in N \land K \neq L) \land y \in V) \to (b \in (0 ..^5) \to (y = ⟨a, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y))))$
82		elpri	$⊢ a \in \{0, 1\} \to (a = 0 \lor a = 1)$
83	81 82	syl11	$⊢ ((K \in N \land L \in N \land K \neq L) \land y \in V) \to (a \in \{0, 1\} \to (b \in (0 ..^5) \to (y = ⟨a, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y))))$
84	83	impd	$⊢ ((K \in N \land L \in N \land K \neq L) \land y \in V) \to ((a \in \{0, 1\} \land b \in (0 ..^5)) \to (y = ⟨a, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y)))$
85	84	rexlimdvv	$⊢ ((K \in N \land L \in N \land K \neq L) \land y \in V) \to (\exists a \in \{0, 1\} \exists b \in (0 ..^5) y = ⟨a, b⟩ \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y))$
86	49 85	mpd	$⊢ ((K \in N \land L \in N \land K \neq L) \land y \in V) \to ((\{K, y\} \in E \land \{y, L\} \in E) \to X = y)$
87	41 86	biimtrrid	$⊢ ((K \in N \land L \in N \land K \neq L) \land y \in V) \to (\{\{K, y\}, \{y, L\}\} \subseteq E \to X = y)$
88	87	ralrimiva	$⊢ (K \in N \land L \in N \land K \neq L) \to \forall y \in V (\{\{K, y\}, \{y, L\}\} \subseteq E \to X = y)$
89	38 88	jca	$⊢ (K \in N \land L \in N \land K \neq L) \to (\{\{K, X\}, \{X, L\}\} \subseteq E \land \forall y \in V (\{\{K, y\}, \{y, L\}\} \subseteq E \to X = y))$
90	12 26 89	rspcedvdw	$⊢ (K \in N \land L \in N \land K \neq L) \to \exists x \in V (\{\{K, x\}, \{x, L\}\} \subseteq E \land \forall y \in V (\{\{K, y\}, \{y, L\}\} \subseteq E \to x = y))$
91		preq2	$⊢ x = y \to \{K, x\} = \{K, y\}$
92		preq1	$⊢ x = y \to \{x, L\} = \{y, L\}$
93	91 92	preq12d	$⊢ x = y \to \{\{K, x\}, \{x, L\}\} = \{\{K, y\}, \{y, L\}\}$
94	93	sseq1d	$⊢ x = y \to (\{\{K, x\}, \{x, L\}\} \subseteq E \leftrightarrow \{\{K, y\}, \{y, L\}\} \subseteq E)$
95	94	reu8	$⊢ \exists! x \in V \{\{K, x\}, \{x, L\}\} \subseteq E \leftrightarrow \exists x \in V (\{\{K, x\}, \{x, L\}\} \subseteq E \land \forall y \in V (\{\{K, y\}, \{y, L\}\} \subseteq E \to x = y))$
96	90 95	sylibr	$⊢ (K \in N \land L \in N \land K \neq L) \to \exists! x \in V \{\{K, x\}, \{x, L\}\} \subseteq E$

Metamath Proof Explorer

Theorem pgnbgreunbgr

Proof