Theorem nbusgrfi

Description: The class of neighbors of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 28-Oct-2020)

	Ref	Expression
Hypotheses	nbusgrf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	nbusgrf1o.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	nbusgrfi	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		nbusgrf1o.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		rabfi	⊢ ( 𝐸 ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin )
4	3	3ad2ant2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin )
5	1 2	edgusgrnbfin	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
6	5	3adant2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
7	4 6	mpbird	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin )