Theorem edgusgrnbfin

Description: The number of neighbors of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 28-Oct-2020)

	Ref	Expression
Hypotheses	nbusgrf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	nbusgrf1o.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	edgusgrnbfin	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		nbusgrf1o.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	nbusgrf1o	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )
4		f1ofo	⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )
5		fofi	⊢ ( ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ∧ 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin )
6	5	expcom	⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
7	4 6	syl	⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
8	7	exlimiv	⊢ ( ∃ 𝑓 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
9	3 8	syl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
10		f1of1	⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )
11		f1fi	⊢ ( ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ∧ 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin )
12	11	expcom	⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) )
13	10 12	syl	⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) )
14	13	exlimiv	⊢ ( ∃ 𝑓 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) )
15	3 14	syl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) )
16	9 15	impbid	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )