Theorem dfclnbgr3

Description: Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval ). (Contributed by AV, 8-May-2025)

	Ref	Expression
Hypotheses	dfclnbgr3.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	dfclnbgr3.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	dfclnbgr3	⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		dfclnbgr3.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfclnbgr3.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4	3	eqcomi	⊢ ran ( iEdg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
5	1 4	clnbgrval	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
6	5	adantr	⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
7	2	eqcomi	⊢ ( iEdg ‘ 𝐺 ) = 𝐼
8	7	rneqi	⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼
9	8	rexeqi	⊢ ( ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ran 𝐼 { 𝑁 , 𝑛 } ⊆ 𝑒 )
10		funfn	⊢ ( Fun 𝐼 ↔ 𝐼 Fn dom 𝐼 )
11	10	biimpi	⊢ ( Fun 𝐼 → 𝐼 Fn dom 𝐼 )
12	11	adantl	⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → 𝐼 Fn dom 𝐼 )
13		sseq2	⊢ ( 𝑒 = ( 𝐼 ‘ 𝑖 ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) ) )
14	13	rexrn	⊢ ( 𝐼 Fn dom 𝐼 → ( ∃ 𝑒 ∈ ran 𝐼 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) ) )
15	12 14	syl	⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( ∃ 𝑒 ∈ ran 𝐼 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) ) )
16	9 15	bitrid	⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) ) )
17	16	rabbidv	⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) } )
18	17	uneq2d	⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) } ) )
19	6 18	eqtrd	⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) } ) )