Theorem dfnbgr3

Description: Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval ). (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 25-Oct-2020) (Revised by AV, 21-Mar-2021)

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

Proof

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