nbusgredgeu0

Description: For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 27-Oct-2020) (Proof shortened by AV, 13-Feb-2022)

	Ref	Expression
Hypotheses	nbusgrf1o1.v	$⊢ V = Vtx (G)$
	nbusgrf1o1.e	$⊢ E = Edg (G)$
	nbusgrf1o1.n	$⊢ N = G NeighbVtx U$
	nbusgrf1o1.i	$⊢ I = \{e \in E \| U \in e\}$
Assertion	nbusgredgeu0	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to \exists! i \in I i = \{U, M\}$

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o1.v	$⊢ V = Vtx (G)$
2		nbusgrf1o1.e	$⊢ E = Edg (G)$
3		nbusgrf1o1.n	$⊢ N = G NeighbVtx U$
4		nbusgrf1o1.i	$⊢ I = \{e \in E \| U \in e\}$
5		simpll	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to G \in USGraph$
6	3	eleq2i	$⊢ M \in N \leftrightarrow M \in (G NeighbVtx U)$
7		nbgrsym	$⊢ M \in (G NeighbVtx U) \leftrightarrow U \in (G NeighbVtx M)$
8	7	a1i	$⊢ (G \in USGraph \land U \in V) \to (M \in (G NeighbVtx U) \leftrightarrow U \in (G NeighbVtx M))$
9	8	biimpd	$⊢ (G \in USGraph \land U \in V) \to (M \in (G NeighbVtx U) \to U \in (G NeighbVtx M))$
10	6 9	syl5bi	$⊢ (G \in USGraph \land U \in V) \to (M \in N \to U \in (G NeighbVtx M))$
11	10	imp	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to U \in (G NeighbVtx M)$
12	2	nbusgredgeu	$⊢ (G \in USGraph \land U \in (G NeighbVtx M)) \to \exists! i \in E i = \{U, M\}$
13	5 11 12	syl2anc	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to \exists! i \in E i = \{U, M\}$
14		df-reu	$⊢ \exists! i \in E i = \{U, M\} \leftrightarrow \exists! i (i \in E \land i = \{U, M\})$
15	13 14	sylib	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to \exists! i (i \in E \land i = \{U, M\})$
16		anass	$⊢ ((i \in E \land U \in i) \land i = \{U, M\}) \leftrightarrow (i \in E \land (U \in i \land i = \{U, M\}))$
17		prid1g	$⊢ U \in V \to U \in \{U, M\}$
18	17	ad2antlr	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to U \in \{U, M\}$
19		eleq2	$⊢ i = \{U, M\} \to (U \in i \leftrightarrow U \in \{U, M\})$
20	18 19	syl5ibrcom	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to (i = \{U, M\} \to U \in i)$
21	20	pm4.71rd	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to (i = \{U, M\} \leftrightarrow (U \in i \land i = \{U, M\}))$
22	21	bicomd	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to ((U \in i \land i = \{U, M\}) \leftrightarrow i = \{U, M\})$
23	22	anbi2d	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to ((i \in E \land (U \in i \land i = \{U, M\})) \leftrightarrow (i \in E \land i = \{U, M\}))$
24	16 23	syl5bb	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to (((i \in E \land U \in i) \land i = \{U, M\}) \leftrightarrow (i \in E \land i = \{U, M\}))$
25	24	eubidv	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to (\exists! i ((i \in E \land U \in i) \land i = \{U, M\}) \leftrightarrow \exists! i (i \in E \land i = \{U, M\}))$
26	15 25	mpbird	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to \exists! i ((i \in E \land U \in i) \land i = \{U, M\})$
27		df-reu	$⊢ \exists! i \in I i = \{U, M\} \leftrightarrow \exists! i (i \in I \land i = \{U, M\})$
28		eleq2	$⊢ e = i \to (U \in e \leftrightarrow U \in i)$
29	28 4	elrab2	$⊢ i \in I \leftrightarrow (i \in E \land U \in i)$
30	29	anbi1i	$⊢ (i \in I \land i = \{U, M\}) \leftrightarrow ((i \in E \land U \in i) \land i = \{U, M\})$
31	30	eubii	$⊢ \exists! i (i \in I \land i = \{U, M\}) \leftrightarrow \exists! i ((i \in E \land U \in i) \land i = \{U, M\})$
32	27 31	bitri	$⊢ \exists! i \in I i = \{U, M\} \leftrightarrow \exists! i ((i \in E \land U \in i) \land i = \{U, M\})$
33	26 32	sylibr	$⊢ ((G \in USGraph \land U \in V) \land M \in N) \to \exists! i \in I i = \{U, M\}$

Metamath Proof Explorer

Theorem nbusgredgeu0

Proof