Metamath Proof Explorer

Theorem uhgrnbgr0nb

Description: A vertex which is not endpoint of an edge has no neighbor in a hypergraph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Assertion uhgrnbgr0nb ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 nbuhgr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑁 ∈ V ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } )
4 3 adantlr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) ∧ 𝑁 ∈ V ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } )
5 df-nel ⊢ ( 𝑁 ∉ 𝑒 ↔ ¬ 𝑁 ∈ 𝑒 )
6 prssg ⊢ ( ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) → ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
7 simpl ⊢ ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) → 𝑁 ∈ 𝑒 )
8 6 7 syl6bir ⊢ ( ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 → 𝑁 ∈ 𝑒 ) )
9 8 ad2antlr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 → 𝑁 ∈ 𝑒 ) )
10 9 con3d ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( ¬ 𝑁 ∈ 𝑒 → ¬ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
11 5 10 syl5bi ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑁 ∉ 𝑒 → ¬ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
12 11 ralimdva ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) ) → ( ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 → ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ¬ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
13 12 imp ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) → ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ¬ { 𝑁 , 𝑛 } ⊆ 𝑒 )
14 ralnex ⊢ ( ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ¬ { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 )
15 13 14 sylib ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) → ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 )
16 15 expcom ⊢ ( ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 → ( ( 𝐺 ∈ UHGraph ∧ ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) ) → ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
17 16 expd ⊢ ( ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 → ( 𝐺 ∈ UHGraph → ( ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) → ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) )
18 17 impcom ⊢ ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) → ( ( 𝑁 ∈ V ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ) → ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
19 18 expdimp ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) ∧ 𝑁 ∈ V ) → ( 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) → ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
20 19 ralrimiv ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) ∧ 𝑁 ∈ V ) → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 )
21 rabeq0 ⊢ ( { 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } = ∅ ↔ ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 )
22 20 21 sylibr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) ∧ 𝑁 ∈ V ) → { 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } = ∅ )
23 4 22 eqtrd ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) ∧ 𝑁 ∈ V ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
24 23 expcom ⊢ ( 𝑁 ∈ V → ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ ) )
25 id ⊢ ( ¬ 𝑁 ∈ V → ¬ 𝑁 ∈ V )
26 25 intnand ⊢ ( ¬ 𝑁 ∈ V → ¬ ( 𝐺 ∈ V ∧ 𝑁 ∈ V ) )
27 nbgrprc0 ⊢ ( ¬ ( 𝐺 ∈ V ∧ 𝑁 ∈ V ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
28 26 27 syl ⊢ ( ¬ 𝑁 ∈ V → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )
29 28 a1d ⊢ ( ¬ 𝑁 ∈ V → ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ ) )
30 24 29 pm2.61i ⊢ ( ( 𝐺 ∈ UHGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝑁 ∉ 𝑒 ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )