This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( 𝑁 ∈ 𝑋 → ( { 𝑁 , 𝑛 } ⊆ 𝑉 → 𝑁 ∈ 𝑉 ) )
25 19 24 syl5com ⊢ ( ( { 𝑁 , 𝑛 } ⊆ 𝑒 ∧ 𝑒 ⊆ 𝑉 ) → ( 𝑁 ∈ 𝑋 → 𝑁 ∈ 𝑉 ) )
26 25 ex ⊢ ( { 𝑁 , 𝑛 } ⊆ 𝑒 → ( 𝑒 ⊆ 𝑉 → ( 𝑁 ∈ 𝑋 → 𝑁 ∈ 𝑉 ) ) )
27 26 com13 ⊢ ( 𝑁 ∈ 𝑋 → ( 𝑒 ⊆ 𝑉 → ( { 𝑁 , 𝑛 } ⊆ 𝑒 → 𝑁 ∈ 𝑉 ) ) )
28 27 ad3antlr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑒 ⊆ 𝑉 → ( { 𝑁 , 𝑛 } ⊆ 𝑒 → 𝑁 ∈ 𝑉 ) ) )
29 18 28 biimtrid ⊢ ( ( ( ( 𝐺 ∈ 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 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )