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 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )