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

Proof

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