edgnbusgreu

Description: For each edge incident to a vertex there is exactly one neighbor of the vertex also incident to this edge in a simple graph. (Contributed by AV, 28-Oct-2020) (Revised by AV, 6-Jul-2022)

	Ref	Expression
Hypotheses	edgnbusgreu.e	$⊢ E = Edg (G)$
	edgnbusgreu.n	$⊢ N = G NeighbVtx M$
Assertion	edgnbusgreu	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to \exists! n \in N C = \{M, n\}$

Proof

Step	Hyp	Ref	Expression
1		edgnbusgreu.e	$⊢ E = Edg (G)$
2		edgnbusgreu.n	$⊢ N = G NeighbVtx M$
3		simpll	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to G \in USGraph$
4	1	eleq2i	$⊢ C \in E \leftrightarrow C \in Edg (G)$
5	4	biimpi	$⊢ C \in E \to C \in Edg (G)$
6	5	ad2antrl	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to C \in Edg (G)$
7		simprr	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to M \in C$
8		usgredg2vtxeu	$⊢ (G \in USGraph \land C \in Edg (G) \land M \in C) \to \exists! n \in Vtx (G) C = \{M, n\}$
9	3 6 7 8	syl3anc	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to \exists! n \in Vtx (G) C = \{M, n\}$
10		df-reu	$⊢ \exists! n \in Vtx (G) C = \{M, n\} \leftrightarrow \exists! n (n \in Vtx (G) \land C = \{M, n\})$
11		prcom	$⊢ \{M, n\} = \{n, M\}$
12	11	eqeq2i	$⊢ C = \{M, n\} \leftrightarrow C = \{n, M\}$
13	12	biimpi	$⊢ C = \{M, n\} \to C = \{n, M\}$
14	13	eleq1d	$⊢ C = \{M, n\} \to (C \in E \leftrightarrow \{n, M\} \in E)$
15	14	biimpcd	$⊢ C \in E \to (C = \{M, n\} \to \{n, M\} \in E)$
16	15	ad2antrl	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to (C = \{M, n\} \to \{n, M\} \in E)$
17	16	adantld	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to ((n \in Vtx (G) \land C = \{M, n\}) \to \{n, M\} \in E)$
18	17	imp	$⊢ (((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \land (n \in Vtx (G) \land C = \{M, n\})) \to \{n, M\} \in E$
19		simprr	$⊢ (((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \land (n \in Vtx (G) \land C = \{M, n\})) \to C = \{M, n\}$
20	18 19	jca	$⊢ (((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \land (n \in Vtx (G) \land C = \{M, n\})) \to (\{n, M\} \in E \land C = \{M, n\})$
21		simpl	$⊢ (\{n, M\} \in E \land C = \{M, n\}) \to \{n, M\} \in E$
22		eqid	$⊢ Vtx (G) = Vtx (G)$
23	1 22	usgrpredgv	$⊢ (G \in USGraph \land \{n, M\} \in E) \to (n \in Vtx (G) \land M \in Vtx (G))$
24	23	simpld	$⊢ (G \in USGraph \land \{n, M\} \in E) \to n \in Vtx (G)$
25	3 21 24	syl2an	$⊢ (((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \land (\{n, M\} \in E \land C = \{M, n\})) \to n \in Vtx (G)$
26		simprr	$⊢ (((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \land (\{n, M\} \in E \land C = \{M, n\})) \to C = \{M, n\}$
27	25 26	jca	$⊢ (((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \land (\{n, M\} \in E \land C = \{M, n\})) \to (n \in Vtx (G) \land C = \{M, n\})$
28	20 27	impbida	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to ((n \in Vtx (G) \land C = \{M, n\}) \leftrightarrow (\{n, M\} \in E \land C = \{M, n\}))$
29	28	eubidv	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to (\exists! n (n \in Vtx (G) \land C = \{M, n\}) \leftrightarrow \exists! n (\{n, M\} \in E \land C = \{M, n\}))$
30	29	biimpd	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to (\exists! n (n \in Vtx (G) \land C = \{M, n\}) \to \exists! n (\{n, M\} \in E \land C = \{M, n\}))$
31	10 30	syl5bi	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to (\exists! n \in Vtx (G) C = \{M, n\} \to \exists! n (\{n, M\} \in E \land C = \{M, n\}))$
32	9 31	mpd	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to \exists! n (\{n, M\} \in E \land C = \{M, n\})$
33	2	eleq2i	$⊢ n \in N \leftrightarrow n \in (G NeighbVtx M)$
34	1	nbusgreledg	$⊢ G \in USGraph \to (n \in (G NeighbVtx M) \leftrightarrow \{n, M\} \in E)$
35	33 34	syl5bb	$⊢ G \in USGraph \to (n \in N \leftrightarrow \{n, M\} \in E)$
36	35	anbi1d	$⊢ G \in USGraph \to ((n \in N \land C = \{M, n\}) \leftrightarrow (\{n, M\} \in E \land C = \{M, n\}))$
37	36	ad2antrr	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to ((n \in N \land C = \{M, n\}) \leftrightarrow (\{n, M\} \in E \land C = \{M, n\}))$
38	37	eubidv	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to (\exists! n (n \in N \land C = \{M, n\}) \leftrightarrow \exists! n (\{n, M\} \in E \land C = \{M, n\}))$
39	32 38	mpbird	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to \exists! n (n \in N \land C = \{M, n\})$
40		df-reu	$⊢ \exists! n \in N C = \{M, n\} \leftrightarrow \exists! n (n \in N \land C = \{M, n\})$
41	39 40	sylibr	$⊢ ((G \in USGraph \land M \in V) \land (C \in E \land M \in C)) \to \exists! n \in N C = \{M, n\}$

Metamath Proof Explorer

Theorem edgnbusgreu

Proof