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 )