Theorem 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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	dfvopnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	dfvopnbgr2.u	⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
Assertion	dfvopnbgr2	⊢ ( 𝑁 ∈ 𝑉 → 𝑈 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } )

Proof

Step	Hyp	Ref	Expression
1		dfvopnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfvopnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		dfvopnbgr2.u	⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
4	1 2	nbgrel	⊢ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
5	4	a1i	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) )
6	5	orbi1d	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ↔ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ) )
7		df-3an	⊢ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
8		r19.42v	⊢ ( ∃ 𝑒 ∈ 𝐸 ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
9	7 8	bitr4i	⊢ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
10	9	orbi1i	⊢ ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ↔ ( ∃ 𝑒 ∈ 𝐸 ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) )
11	10	a1i	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ↔ ( ∃ 𝑒 ∈ 𝐸 ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ) )
12		r19.43	⊢ ( ∃ 𝑒 ∈ 𝐸 ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ↔ ( ∃ 𝑒 ∈ 𝐸 ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) )
13	11 12	bitr4di	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ) )
14	6 13	bitrd	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ) )
15		anass	⊢ ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) )
16	15	a1i	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) ) )
17		ibar	⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) ) )
18	17	ancoms	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) ) )
19	18	adantr	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) ) )
20		prssg	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
21	20	bicomd	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) )
22	21	adantr	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) )
23	22	anbi2d	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( 𝑛 ≠ 𝑁 ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) ) )
24		3anass	⊢ ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ ( 𝑛 ≠ 𝑁 ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) )
25	23 24	bitr4di	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( ( 𝑛 ≠ 𝑁 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) )
26	16 19 25	3bitr2d	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ↔ ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) )
27		eqcom	⊢ ( 𝑁 = 𝑛 ↔ 𝑛 = 𝑁 )
28	27	anbi1i	⊢ ( ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ↔ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑁 } ) )
29		sneq	⊢ ( 𝑁 = 𝑛 → { 𝑁 } = { 𝑛 } )
30	29	eqcoms	⊢ ( 𝑛 = 𝑁 → { 𝑁 } = { 𝑛 } )
31	30	eqeq2d	⊢ ( 𝑛 = 𝑁 → ( 𝑒 = { 𝑁 } ↔ 𝑒 = { 𝑛 } ) )
32	31	pm5.32i	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑁 } ) ↔ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) )
33	28 32	bitri	⊢ ( ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ↔ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) )
34	33	a1i	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ↔ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) )
35	26 34	orbi12d	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ↔ ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) ) )
36	35	rexbidva	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ∃ 𝑒 ∈ 𝐸 ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑁 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∨ ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) ) )
37	14 36	bitrd	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) ) )
38	37	rabbidva	⊢ ( 𝑁 ∈ 𝑉 → { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) } = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } )
39	3 38	eqtrid	⊢ ( 𝑁 ∈ 𝑉 → 𝑈 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } )