Theorem fusgrvtxfi

Description: A finite simple graph has a finite set of vertices. (Contributed by AV, 16-Dec-2020)

	Ref	Expression
Hypothesis	isfusgr.v	|- V = ( Vtx ` G )
Assertion	fusgrvtxfi	|- ( G e. FinUSGraph -> V e. Fin )

Proof

Step	Hyp	Ref	Expression
1		isfusgr.v	|- V = ( Vtx ` G )
2	1	isfusgr	|- ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
3	2	simprbi	|- ( G e. FinUSGraph -> V e. Fin )