Metamath Proof Explorer


Theorem finrusgrfusgr

Description: A finite regular simple graph is a finite simple graph. (Contributed by AV, 3-Jun-2021)

Ref Expression
Hypothesis finrusgrfusgr.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion finrusgrfusgr ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph )

Proof

Step Hyp Ref Expression
1 finrusgrfusgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 rusgrusgr ( 𝐺 RegUSGraph 𝐾𝐺 ∈ USGraph )
3 2 anim1i ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
4 1 isfusgr ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
5 3 4 sylibr ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph )