nbumgrvtx

Description: The set of neighbors of a vertex in a multigraph. (Contributed by AV, 27-Nov-2020) (Proof shortened by AV, 30-Dec-2020)

	Ref	Expression
Hypotheses	nbuhgr.v	$⊢ V = Vtx (G)$
	nbuhgr.e	$⊢ E = Edg (G)$
Assertion	nbumgrvtx	$⊢ (G \in UMGraph \land N \in V) \to G NeighbVtx N = \{n \in V \| \{N, n\} \in E\}$

Proof

Step	Hyp	Ref	Expression
1		nbuhgr.v	$⊢ V = Vtx (G)$
2		nbuhgr.e	$⊢ E = Edg (G)$
3	1 2	nbgrval	$⊢ N \in V \to G NeighbVtx N = \{v \in (V ∖ \{N\}) \| \exists e \in E \{N, v\} \subseteq e\}$
4	3	adantl	$⊢ (G \in UMGraph \land N \in V) \to G NeighbVtx N = \{v \in (V ∖ \{N\}) \| \exists e \in E \{N, v\} \subseteq e\}$
5		eldifi	$⊢ x \in (V ∖ \{N\}) \to x \in V$
6	5	adantl	$⊢ ((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \to x \in V$
7	6	adantr	$⊢ (((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land (e \in E \land \{N, x\} \subseteq e)) \to x \in V$
8		umgrupgr	$⊢ G \in UMGraph \to G \in UPGraph$
9	8	ad4antr	$⊢ ((((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land e \in E) \land \{N, x\} \subseteq e) \to G \in UPGraph$
10		simpr	$⊢ (((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land e \in E) \to e \in E$
11	10	adantr	$⊢ ((((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land e \in E) \land \{N, x\} \subseteq e) \to e \in E$
12		simpr	$⊢ ((((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land e \in E) \land \{N, x\} \subseteq e) \to \{N, x\} \subseteq e$
13		simpr	$⊢ (G \in UMGraph \land N \in V) \to N \in V$
14	13	adantr	$⊢ ((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \to N \in V$
15		vex	$⊢ x \in V$
16	15	a1i	$⊢ ((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \to x \in V$
17		eldifsn	$⊢ x \in (V ∖ \{N\}) \leftrightarrow (x \in V \land x \neq N)$
18		simpr	$⊢ (x \in V \land x \neq N) \to x \neq N$
19	18	necomd	$⊢ (x \in V \land x \neq N) \to N \neq x$
20	17 19	sylbi	$⊢ x \in (V ∖ \{N\}) \to N \neq x$
21	20	adantl	$⊢ ((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \to N \neq x$
22	14 16 21	3jca	$⊢ ((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \to (N \in V \land x \in V \land N \neq x)$
23	22	adantr	$⊢ (((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land e \in E) \to (N \in V \land x \in V \land N \neq x)$
24	23	adantr	$⊢ ((((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land e \in E) \land \{N, x\} \subseteq e) \to (N \in V \land x \in V \land N \neq x)$
25	1 2	upgredgpr	$⊢ ((G \in UPGraph \land e \in E \land \{N, x\} \subseteq e) \land (N \in V \land x \in V \land N \neq x)) \to \{N, x\} = e$
26	9 11 12 24 25	syl31anc	$⊢ ((((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land e \in E) \land \{N, x\} \subseteq e) \to \{N, x\} = e$
27	26	ex	$⊢ (((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land e \in E) \to (\{N, x\} \subseteq e \to \{N, x\} = e)$
28		eleq1	$⊢ \{N, x\} = e \to (\{N, x\} \in E \leftrightarrow e \in E)$
29	28	biimprd	$⊢ \{N, x\} = e \to (e \in E \to \{N, x\} \in E)$
30	27 10 29	syl6ci	$⊢ (((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land e \in E) \to (\{N, x\} \subseteq e \to \{N, x\} \in E)$
31	30	impr	$⊢ (((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land (e \in E \land \{N, x\} \subseteq e)) \to \{N, x\} \in E$
32	7 31	jca	$⊢ (((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \land (e \in E \land \{N, x\} \subseteq e)) \to (x \in V \land \{N, x\} \in E)$
33	32	rexlimdvaa	$⊢ ((G \in UMGraph \land N \in V) \land x \in (V ∖ \{N\})) \to (\exists e \in E \{N, x\} \subseteq e \to (x \in V \land \{N, x\} \in E))$
34	33	expimpd	$⊢ (G \in UMGraph \land N \in V) \to ((x \in (V ∖ \{N\}) \land \exists e \in E \{N, x\} \subseteq e) \to (x \in V \land \{N, x\} \in E))$
35		simprl	$⊢ ((G \in UMGraph \land N \in V) \land (x \in V \land \{N, x\} \in E)) \to x \in V$
36	2	umgredgne	$⊢ (G \in UMGraph \land \{N, x\} \in E) \to N \neq x$
37	36	ad2ant2rl	$⊢ ((G \in UMGraph \land N \in V) \land (x \in V \land \{N, x\} \in E)) \to N \neq x$
38	37	necomd	$⊢ ((G \in UMGraph \land N \in V) \land (x \in V \land \{N, x\} \in E)) \to x \neq N$
39	35 38 17	sylanbrc	$⊢ ((G \in UMGraph \land N \in V) \land (x \in V \land \{N, x\} \in E)) \to x \in (V ∖ \{N\})$
40		simpr	$⊢ (x \in V \land \{N, x\} \in E) \to \{N, x\} \in E$
41	40	adantl	$⊢ ((G \in UMGraph \land N \in V) \land (x \in V \land \{N, x\} \in E)) \to \{N, x\} \in E$
42		sseq2	$⊢ e = \{N, x\} \to (\{N, x\} \subseteq e \leftrightarrow \{N, x\} \subseteq \{N, x\})$
43	42	adantl	$⊢ (((G \in UMGraph \land N \in V) \land (x \in V \land \{N, x\} \in E)) \land e = \{N, x\}) \to (\{N, x\} \subseteq e \leftrightarrow \{N, x\} \subseteq \{N, x\})$
44		ssidd	$⊢ ((G \in UMGraph \land N \in V) \land (x \in V \land \{N, x\} \in E)) \to \{N, x\} \subseteq \{N, x\}$
45	41 43 44	rspcedvd	$⊢ ((G \in UMGraph \land N \in V) \land (x \in V \land \{N, x\} \in E)) \to \exists e \in E \{N, x\} \subseteq e$
46	39 45	jca	$⊢ ((G \in UMGraph \land N \in V) \land (x \in V \land \{N, x\} \in E)) \to (x \in (V ∖ \{N\}) \land \exists e \in E \{N, x\} \subseteq e)$
47	46	ex	$⊢ (G \in UMGraph \land N \in V) \to ((x \in V \land \{N, x\} \in E) \to (x \in (V ∖ \{N\}) \land \exists e \in E \{N, x\} \subseteq e))$
48	34 47	impbid	$⊢ (G \in UMGraph \land N \in V) \to ((x \in (V ∖ \{N\}) \land \exists e \in E \{N, x\} \subseteq e) \leftrightarrow (x \in V \land \{N, x\} \in E))$
49		preq2	$⊢ v = x \to \{N, v\} = \{N, x\}$
50	49	sseq1d	$⊢ v = x \to (\{N, v\} \subseteq e \leftrightarrow \{N, x\} \subseteq e)$
51	50	rexbidv	$⊢ v = x \to (\exists e \in E \{N, v\} \subseteq e \leftrightarrow \exists e \in E \{N, x\} \subseteq e)$
52	51	elrab	$⊢ x \in \{v \in (V ∖ \{N\}) \| \exists e \in E \{N, v\} \subseteq e\} \leftrightarrow (x \in (V ∖ \{N\}) \land \exists e \in E \{N, x\} \subseteq e)$
53		preq2	$⊢ n = x \to \{N, n\} = \{N, x\}$
54	53	eleq1d	$⊢ n = x \to (\{N, n\} \in E \leftrightarrow \{N, x\} \in E)$
55	54	elrab	$⊢ x \in \{n \in V \| \{N, n\} \in E\} \leftrightarrow (x \in V \land \{N, x\} \in E)$
56	48 52 55	3bitr4g	$⊢ (G \in UMGraph \land N \in V) \to (x \in \{v \in (V ∖ \{N\}) \| \exists e \in E \{N, v\} \subseteq e\} \leftrightarrow x \in \{n \in V \| \{N, n\} \in E\})$
57	56	eqrdv	$⊢ (G \in UMGraph \land N \in V) \to \{v \in (V ∖ \{N\}) \| \exists e \in E \{N, v\} \subseteq e\} = \{n \in V \| \{N, n\} \in E\}$
58	4 57	eqtrd	$⊢ (G \in UMGraph \land N \in V) \to G NeighbVtx N = \{n \in V \| \{N, n\} \in E\}$

Metamath Proof Explorer

Theorem nbumgrvtx

Proof