Theorem fusgrvtxfi

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

	Ref	Expression
Hypothesis	isfusgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	fusgrvtxfi	⊢ ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		isfusgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	isfusgr	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
3	2	simprbi	⊢ ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin )