This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )