dfvopnbgr2

Description: Alternate definition of the semiopen neighborhood of a vertex breaking up the subset relationship of an unordered pair. Asemiopen neighborhood U of a vertex N is its open neighborhood together with itself if there is a loop at this vertex. (Contributed by AV, 15-May-2025)

	Ref	Expression
Hypotheses	dfvopnbgr2.v	$⊢ V = Vtx (G)$
	dfvopnbgr2.e	$⊢ E = Edg (G)$
	dfvopnbgr2.u	$⊢ U = \{n \in V \| (n \in (G NeighbVtx N) \lor \exists e \in E (N = n \land e = \{N\}))\}$
Assertion	dfvopnbgr2	$⊢ N \in V \to U = \{n \in V \| \exists e \in E ((n \neq N \land N \in e \land n \in e) \lor (n = N \land e = \{n\}))\}$

Proof

Step	Hyp	Ref	Expression
1		dfvopnbgr2.v	$⊢ V = Vtx (G)$
2		dfvopnbgr2.e	$⊢ E = Edg (G)$
3		dfvopnbgr2.u	$⊢ U = \{n \in V \| (n \in (G NeighbVtx N) \lor \exists e \in E (N = n \land e = \{N\}))\}$
4	1 2	nbgrel	$⊢ n \in (G NeighbVtx N) \leftrightarrow ((n \in V \land N \in V) \land n \neq N \land \exists e \in E \{N, n\} \subseteq e)$
5	4	a1i	$⊢ (N \in V \land n \in V) \to (n \in (G NeighbVtx N) \leftrightarrow ((n \in V \land N \in V) \land n \neq N \land \exists e \in E \{N, n\} \subseteq e))$
6	5	orbi1d	$⊢ (N \in V \land n \in V) \to ((n \in (G NeighbVtx N) \lor \exists e \in E (N = n \land e = \{N\})) \leftrightarrow (((n \in V \land N \in V) \land n \neq N \land \exists e \in E \{N, n\} \subseteq e) \lor \exists e \in E (N = n \land e = \{N\})))$
7		df-3an	$⊢ ((n \in V \land N \in V) \land n \neq N \land \exists e \in E \{N, n\} \subseteq e) \leftrightarrow (((n \in V \land N \in V) \land n \neq N) \land \exists e \in E \{N, n\} \subseteq e)$
8		r19.42v	$⊢ \exists e \in E (((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \leftrightarrow (((n \in V \land N \in V) \land n \neq N) \land \exists e \in E \{N, n\} \subseteq e)$
9	7 8	bitr4i	$⊢ ((n \in V \land N \in V) \land n \neq N \land \exists e \in E \{N, n\} \subseteq e) \leftrightarrow \exists e \in E (((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e)$
10	9	orbi1i	$⊢ (((n \in V \land N \in V) \land n \neq N \land \exists e \in E \{N, n\} \subseteq e) \lor \exists e \in E (N = n \land e = \{N\})) \leftrightarrow (\exists e \in E (((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \lor \exists e \in E (N = n \land e = \{N\}))$
11	10	a1i	$⊢ (N \in V \land n \in V) \to ((((n \in V \land N \in V) \land n \neq N \land \exists e \in E \{N, n\} \subseteq e) \lor \exists e \in E (N = n \land e = \{N\})) \leftrightarrow (\exists e \in E (((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \lor \exists e \in E (N = n \land e = \{N\})))$
12		r19.43	$⊢ \exists e \in E ((((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \lor (N = n \land e = \{N\})) \leftrightarrow (\exists e \in E (((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \lor \exists e \in E (N = n \land e = \{N\}))$
13	11 12	bitr4di	$⊢ (N \in V \land n \in V) \to ((((n \in V \land N \in V) \land n \neq N \land \exists e \in E \{N, n\} \subseteq e) \lor \exists e \in E (N = n \land e = \{N\})) \leftrightarrow \exists e \in E ((((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \lor (N = n \land e = \{N\})))$
14	6 13	bitrd	$⊢ (N \in V \land n \in V) \to ((n \in (G NeighbVtx N) \lor \exists e \in E (N = n \land e = \{N\})) \leftrightarrow \exists e \in E ((((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \lor (N = n \land e = \{N\})))$
15		anass	$⊢ (((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \leftrightarrow ((n \in V \land N \in V) \land (n \neq N \land \{N, n\} \subseteq e))$
16	15	a1i	$⊢ ((N \in V \land n \in V) \land e \in E) \to ((((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \leftrightarrow ((n \in V \land N \in V) \land (n \neq N \land \{N, n\} \subseteq e)))$
17		ibar	$⊢ (n \in V \land N \in V) \to ((n \neq N \land \{N, n\} \subseteq e) \leftrightarrow ((n \in V \land N \in V) \land (n \neq N \land \{N, n\} \subseteq e)))$
18	17	ancoms	$⊢ (N \in V \land n \in V) \to ((n \neq N \land \{N, n\} \subseteq e) \leftrightarrow ((n \in V \land N \in V) \land (n \neq N \land \{N, n\} \subseteq e)))$
19	18	adantr	$⊢ ((N \in V \land n \in V) \land e \in E) \to ((n \neq N \land \{N, n\} \subseteq e) \leftrightarrow ((n \in V \land N \in V) \land (n \neq N \land \{N, n\} \subseteq e)))$
20		prssg	$⊢ (N \in V \land n \in V) \to ((N \in e \land n \in e) \leftrightarrow \{N, n\} \subseteq e)$
21	20	bicomd	$⊢ (N \in V \land n \in V) \to (\{N, n\} \subseteq e \leftrightarrow (N \in e \land n \in e))$
22	21	adantr	$⊢ ((N \in V \land n \in V) \land e \in E) \to (\{N, n\} \subseteq e \leftrightarrow (N \in e \land n \in e))$
23	22	anbi2d	$⊢ ((N \in V \land n \in V) \land e \in E) \to ((n \neq N \land \{N, n\} \subseteq e) \leftrightarrow (n \neq N \land (N \in e \land n \in e)))$
24		3anass	$⊢ (n \neq N \land N \in e \land n \in e) \leftrightarrow (n \neq N \land (N \in e \land n \in e))$
25	23 24	bitr4di	$⊢ ((N \in V \land n \in V) \land e \in E) \to ((n \neq N \land \{N, n\} \subseteq e) \leftrightarrow (n \neq N \land N \in e \land n \in e))$
26	16 19 25	3bitr2d	$⊢ ((N \in V \land n \in V) \land e \in E) \to ((((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \leftrightarrow (n \neq N \land N \in e \land n \in e))$
27		eqcom	$⊢ N = n \leftrightarrow n = N$
28	27	anbi1i	$⊢ (N = n \land e = \{N\}) \leftrightarrow (n = N \land e = \{N\})$
29		sneq	$⊢ N = n \to \{N\} = \{n\}$
30	29	eqcoms	$⊢ n = N \to \{N\} = \{n\}$
31	30	eqeq2d	$⊢ n = N \to (e = \{N\} \leftrightarrow e = \{n\})$
32	31	pm5.32i	$⊢ (n = N \land e = \{N\}) \leftrightarrow (n = N \land e = \{n\})$
33	28 32	bitri	$⊢ (N = n \land e = \{N\}) \leftrightarrow (n = N \land e = \{n\})$
34	33	a1i	$⊢ ((N \in V \land n \in V) \land e \in E) \to ((N = n \land e = \{N\}) \leftrightarrow (n = N \land e = \{n\}))$
35	26 34	orbi12d	$⊢ ((N \in V \land n \in V) \land e \in E) \to (((((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \lor (N = n \land e = \{N\})) \leftrightarrow ((n \neq N \land N \in e \land n \in e) \lor (n = N \land e = \{n\})))$
36	35	rexbidva	$⊢ (N \in V \land n \in V) \to (\exists e \in E ((((n \in V \land N \in V) \land n \neq N) \land \{N, n\} \subseteq e) \lor (N = n \land e = \{N\})) \leftrightarrow \exists e \in E ((n \neq N \land N \in e \land n \in e) \lor (n = N \land e = \{n\})))$
37	14 36	bitrd	$⊢ (N \in V \land n \in V) \to ((n \in (G NeighbVtx N) \lor \exists e \in E (N = n \land e = \{N\})) \leftrightarrow \exists e \in E ((n \neq N \land N \in e \land n \in e) \lor (n = N \land e = \{n\})))$
38	37	rabbidva	$⊢ N \in V \to \{n \in V \| (n \in (G NeighbVtx N) \lor \exists e \in E (N = n \land e = \{N\}))\} = \{n \in V \| \exists e \in E ((n \neq N \land N \in e \land n \in e) \lor (n = N \land e = \{n\}))\}$
39	3 38	eqtrid	$⊢ N \in V \to U = \{n \in V \| \exists e \in E ((n \neq N \land N \in e \land n \in e) \lor (n = N \land e = \{n\}))\}$

Metamath Proof Explorer

Theorem dfvopnbgr2

Proof