Metamath Proof Explorer

Theorem dfsclnbgr6

Description: Alternate definition of a semiclosed neighborhood of a vertex as a union of a semiopen neighborhood and the vertex itself if there is a loop at this vertex. (Contributed by AV, 17-May-2025)

Ref Expression
Hypotheses dfvopnbgr2.v ⊢ V = Vtx ⁡ G
dfvopnbgr2.e ⊢ E = Edg ⁡ G
dfvopnbgr2.u ⊢ U = n ∈ V | n ∈ G NeighbVtx N ∨ ∃ e ∈ E N = n ∧ e = N
dfsclnbgr6.s ⊢ S = n ∈ V | ∃ e ∈ E N n ⊆ e
Assertion dfsclnbgr6 ⊢ N ∈ V → S = U ∪ n ∈ N | ∃ e ∈ E n ∈ e

Proof

Step Hyp Ref Expression
1 dfvopnbgr2.v ⊢ V = Vtx ⁡ G
2 dfvopnbgr2.e ⊢ E = Edg ⁡ G
3 dfvopnbgr2.u ⊢ U = n ∈ V | n ∈ G NeighbVtx N ∨ ∃ e ∈ E N = n ∧ e = N
4 dfsclnbgr6.s ⊢ S = n ∈ V | ∃ e ∈ E N n ⊆ e
5 simpr ⊢ N ∈ e ∧ n ∈ e → n ∈ e
6 5 anim1i ⊢ N ∈ e ∧ n ∈ e ∧ n = N → n ∈ e ∧ n = N
7 6 olcd ⊢ N ∈ e ∧ n ∈ e ∧ n = N → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N
8 7 expcom ⊢ n = N → N ∈ e ∧ n ∈ e → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N
9 3anass ⊢ n ≠ N ∧ N ∈ e ∧ n ∈ e ↔ n ≠ N ∧ N ∈ e ∧ n ∈ e
10 9 biimpri ⊢ n ≠ N ∧ N ∈ e ∧ n ∈ e → n ≠ N ∧ N ∈ e ∧ n ∈ e
11 10 orcd ⊢ n ≠ N ∧ N ∈ e ∧ n ∈ e → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
12 11 orcd ⊢ n ≠ N ∧ N ∈ e ∧ n ∈ e → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N
13 12 ex ⊢ n ≠ N → N ∈ e ∧ n ∈ e → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N
14 8 13 pm2.61ine ⊢ N ∈ e ∧ n ∈ e → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N
15 3simpc ⊢ n ≠ N ∧ N ∈ e ∧ n ∈ e → N ∈ e ∧ n ∈ e
16 15 a1i ⊢ N ∈ V → n ≠ N ∧ N ∈ e ∧ n ∈ e → N ∈ e ∧ n ∈ e
17 vsnid ⊢ n ∈ n
18 17 a1i ⊢ e = n → n ∈ n
19 eleq2 ⊢ e = n → n ∈ e ↔ n ∈ n
20 18 19 mpbird ⊢ e = n → n ∈ e
21 20 adantl ⊢ n = N ∧ e = n → n ∈ e
22 eleq1 ⊢ n = N → n ∈ e ↔ N ∈ e
23 22 bicomd ⊢ n = N → N ∈ e ↔ n ∈ e
24 23 adantr ⊢ n = N ∧ e = n → N ∈ e ↔ n ∈ e
25 21 24 mpbird ⊢ n = N ∧ e = n → N ∈ e
26 25 adantl ⊢ N ∈ V ∧ n = N ∧ e = n → N ∈ e
27 21 adantl ⊢ N ∈ V ∧ n = N ∧ e = n → n ∈ e
28 26 27 jca ⊢ N ∈ V ∧ n = N ∧ e = n → N ∈ e ∧ n ∈ e
29 28 ex ⊢ N ∈ V → n = N ∧ e = n → N ∈ e ∧ n ∈ e
30 16 29 jaod ⊢ N ∈ V → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n → N ∈ e ∧ n ∈ e
31 22 biimpac ⊢ n ∈ e ∧ n = N → N ∈ e
32 simpl ⊢ n ∈ e ∧ n = N → n ∈ e
33 31 32 jca ⊢ n ∈ e ∧ n = N → N ∈ e ∧ n ∈ e
34 33 a1i ⊢ N ∈ V → n ∈ e ∧ n = N → N ∈ e ∧ n ∈ e
35 30 34 jaod ⊢ N ∈ V → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N → N ∈ e ∧ n ∈ e
36 14 35 impbid2 ⊢ N ∈ V → N ∈ e ∧ n ∈ e ↔ n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N
37 36 rexbidv ⊢ N ∈ V → ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N
38 r19.43 ⊢ ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N ↔ ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ ∃ e ∈ E n ∈ e ∧ n = N
39 38 a1i ⊢ N ∈ V → ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n ∈ e ∧ n = N ↔ ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ ∃ e ∈ E n ∈ e ∧ n = N
40 r19.41v ⊢ ∃ e ∈ E n ∈ e ∧ n = N ↔ ∃ e ∈ E n ∈ e ∧ n = N
41 40 biancomi ⊢ ∃ e ∈ E n ∈ e ∧ n = N ↔ n = N ∧ ∃ e ∈ E n ∈ e
42 41 a1i ⊢ N ∈ V → ∃ e ∈ E n ∈ e ∧ n = N ↔ n = N ∧ ∃ e ∈ E n ∈ e
43 42 orbi2d ⊢ N ∈ V → ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ ∃ e ∈ E n ∈ e ∧ n = N ↔ ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n = N ∧ ∃ e ∈ E n ∈ e
44 37 39 43 3bitrd ⊢ N ∈ V → ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n = N ∧ ∃ e ∈ E n ∈ e
45 44 rabbidv ⊢ N ∈ V → n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n = N ∧ ∃ e ∈ E n ∈ e
46 unrab ⊢ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∪ n ∈ V | n = N ∧ ∃ e ∈ E n ∈ e = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n = N ∧ ∃ e ∈ E n ∈ e
47 rabsneq ⊢ N ∈ V → n ∈ N | ∃ e ∈ E n ∈ e = n ∈ V | n = N ∧ ∃ e ∈ E n ∈ e
48 47 eqcomd ⊢ N ∈ V → n ∈ V | n = N ∧ ∃ e ∈ E n ∈ e = n ∈ N | ∃ e ∈ E n ∈ e
49 48 uneq2d ⊢ N ∈ V → n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∪ n ∈ V | n = N ∧ ∃ e ∈ E n ∈ e = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∪ n ∈ N | ∃ e ∈ E n ∈ e
50 46 49 eqtr3id ⊢ N ∈ V → n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∨ n = N ∧ ∃ e ∈ E n ∈ e = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∪ n ∈ N | ∃ e ∈ E n ∈ e
51 45 50 eqtrd ⊢ N ∈ V → n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∪ n ∈ N | ∃ e ∈ E n ∈ e
52 1 4 2 dfsclnbgr2 ⊢ N ∈ V → S = n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e
53 1 2 3 dfvopnbgr2 ⊢ N ∈ V → U = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
54 53 uneq1d ⊢ N ∈ V → U ∪ n ∈ N | ∃ e ∈ E n ∈ e = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∪ n ∈ N | ∃ e ∈ E n ∈ e
55 51 52 54 3eqtr4d ⊢ N ∈ V → S = U ∪ n ∈ N | ∃ e ∈ E n ∈ e