Metamath Proof Explorer


Theorem nbuhgr

Description: The set of neighbors of a vertex in a hypergraph. This version of nbgrval (with N being an arbitrary set instead of being a vertex) only holds for classes whose edges are subsets of the set of vertices (hypergraphs!). (Contributed by AV, 26-Oct-2020) (Proof shortened by AV, 15-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v 𝑉 = ( Vtx ‘ 𝐺 )
nbuhgr.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbuhgr ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )

Proof

Step Hyp Ref Expression
1 nbuhgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 nbuhgr.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 nbgrval ( 𝑁𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )
4 3 a1d ( 𝑁𝑉 → ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
5 df-nel ( 𝑁𝑉 ↔ ¬ 𝑁𝑉 )
6 1 nbgrnvtx0 ( 𝑁𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
7 5 6 sylbir ( ¬ 𝑁𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
8 7 adantr ( ( ¬ 𝑁𝑉 ∧ ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
9 simpl ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) → 𝐺 ∈ UHGraph )
10 9 adantr ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝐺 ∈ UHGraph )
11 2 eleq2i ( 𝑒𝐸𝑒 ∈ ( Edg ‘ 𝐺 ) )
12 11 biimpi ( 𝑒𝐸𝑒 ∈ ( Edg ‘ 𝐺 ) )
13 edguhgr ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
14 10 12 13 syl2an ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒𝐸 ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
15 velpw ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ 𝑒 ⊆ ( Vtx ‘ 𝐺 ) )
16 1 eqcomi ( Vtx ‘ 𝐺 ) = 𝑉
17 16 sseq2i ( 𝑒 ⊆ ( Vtx ‘ 𝐺 ) ↔ 𝑒𝑉 )
18 15 17 bitri ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ 𝑒𝑉 )
19 sstr ( ( { 𝑁 , 𝑛 } ⊆ 𝑒𝑒𝑉 ) → { 𝑁 , 𝑛 } ⊆ 𝑉 )
20 prssg ( ( 𝑁𝑋𝑛 ∈ V ) → ( ( 𝑁𝑉𝑛𝑉 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑉 ) )
21 20 bicomd ( ( 𝑁𝑋𝑛 ∈ V ) → ( { 𝑁 , 𝑛 } ⊆ 𝑉 ↔ ( 𝑁𝑉𝑛𝑉 ) ) )
22 21 elvd ( 𝑁𝑋 → ( { 𝑁 , 𝑛 } ⊆ 𝑉 ↔ ( 𝑁𝑉𝑛𝑉 ) ) )
23 simpl ( ( 𝑁𝑉𝑛𝑉 ) → 𝑁𝑉 )
24 22 23 syl6bi ( 𝑁𝑋 → ( { 𝑁 , 𝑛 } ⊆ 𝑉𝑁𝑉 ) )
25 19 24 syl5com ( ( { 𝑁 , 𝑛 } ⊆ 𝑒𝑒𝑉 ) → ( 𝑁𝑋𝑁𝑉 ) )
26 25 ex ( { 𝑁 , 𝑛 } ⊆ 𝑒 → ( 𝑒𝑉 → ( 𝑁𝑋𝑁𝑉 ) ) )
27 26 com13 ( 𝑁𝑋 → ( 𝑒𝑉 → ( { 𝑁 , 𝑛 } ⊆ 𝑒𝑁𝑉 ) ) )
28 27 ad3antlr ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒𝐸 ) → ( 𝑒𝑉 → ( { 𝑁 , 𝑛 } ⊆ 𝑒𝑁𝑉 ) ) )
29 18 28 syl5bi ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒𝐸 ) → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒𝑁𝑉 ) ) )
30 14 29 mpd ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒𝐸 ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒𝑁𝑉 ) )
31 30 rexlimdva ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒𝑁𝑉 ) )
32 31 con3rr3 ( ¬ 𝑁𝑉 → ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ¬ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
33 32 expdimp ( ( ¬ 𝑁𝑉 ∧ ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ) → ( 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
34 33 ralrimiv ( ( ¬ 𝑁𝑉 ∧ ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ) → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ¬ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 )
35 rabeq0 ( { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } = ∅ ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ¬ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 )
36 34 35 sylibr ( ( ¬ 𝑁𝑉 ∧ ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ) → { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } = ∅ )
37 8 36 eqtr4d ( ( ¬ 𝑁𝑉 ∧ ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )
38 37 ex ( ¬ 𝑁𝑉 → ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
39 4 38 pm2.61i ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑋 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )