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=\mathrm{Vtx}\left(G\right)$$
Assertion	fusgrvtxfi	$$⊢G\in \mathrm{FinUSGraph}\to V\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		isfusgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	isfusgr	$$⊢G\in \mathrm{FinUSGraph}\leftrightarrow \left(G\in \mathrm{USGraph}\wedge V\in \mathrm{Fin}\right)$$
3	2	simprbi	$$⊢G\in \mathrm{FinUSGraph}\to V\in \mathrm{Fin}$$