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 e. Fin ) -> G e. FinUSGraph )

Proof

Step	Hyp	Ref	Expression
1		finrusgrfusgr.v	|- V = ( Vtx ` G )
2		rusgrusgr	|- ( G RegUSGraph K -> G e. USGraph )
3	2	anim1i	|- ( ( G RegUSGraph K /\ V e. Fin ) -> ( G e. USGraph /\ V e. Fin ) )
4	1	isfusgr	|- ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
5	3 4	sylibr	|- ( ( G RegUSGraph K /\ V e. Fin ) -> G e. FinUSGraph )