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 ⊢ V = Vtx ⁡ G
Assertion finrusgrfusgr ⊢ G RegUSGraph K ∧ V ∈ Fin → G ∈ FinUSGraph

Proof

Step Hyp Ref Expression
1 finrusgrfusgr.v ⊢ V = Vtx ⁡ G
2 rusgrusgr ⊢ G RegUSGraph K → G ∈ USGraph
3 2 anim1i ⊢ G RegUSGraph K ∧ V ∈ Fin → G ∈ USGraph ∧ V ∈ Fin
4 1 isfusgr ⊢ G ∈ FinUSGraph ↔ G ∈ USGraph ∧ V ∈ Fin
5 3 4 sylibr ⊢ G RegUSGraph K ∧ V ∈ Fin → G ∈ FinUSGraph