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

Metamath Proof Explorer

Theorem dfclnbgr2

Description: Alternate definition of the closed neighborhood of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 7-May-2025)

		Ref	Expression
	Hypotheses	clnbgrval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
		clnbgrval.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	Assertion	dfclnbgr2	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		clnbgrval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clnbgrval.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	clnbgrval	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
4		prssg	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ) → ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
5	4	elvd	⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
6	5	bicomd	⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) )
7	6	rexbidv	⊢ ( 𝑁 ∈ 𝑉 → ( ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) )
8	7	rabbidv	⊢ ( 𝑁 ∈ 𝑉 → { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
9	8	uneq2d	⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) )
10	3 9	eqtrd	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) )