Theorem fusgredgfi

Description: In a finite simple graph the number of edges which contain a given vertex is also finite. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 21-Oct-2020)

	Ref	Expression
Hypotheses	fusgredgfi.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	fusgredgfi.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	fusgredgfi	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fusgredgfi.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fusgredgfi.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	2	fvexi	⊢ 𝐸 ∈ V
4		rabexg	⊢ ( 𝐸 ∈ V → { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∈ V )
5	3 4	mp1i	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∈ V )
6	1	isfusgr	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
7		hashcl	⊢ ( 𝑉 ∈ Fin → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
8	6 7	simplbiim	⊢ ( 𝐺 ∈ FinUSGraph → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
9	8	adantr	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
10		fusgrusgr	⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
11	1 2	usgredgleord	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ≤ ( ♯ ‘ 𝑉 ) )
12	10 11	sylan	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ≤ ( ♯ ‘ 𝑉 ) )
13		hashbnd	⊢ ( ( { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∈ V ∧ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ≤ ( ♯ ‘ 𝑉 ) ) → { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∈ Fin )
14	5 9 12 13	syl3anc	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∈ Fin )