Theorem isfusgr

Description: The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020) (Revised by AV, 21-Oct-2020)

	Ref	Expression
Hypothesis	isfusgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	isfusgr	$$⊢G\in \mathrm{FinUSGraph}\leftrightarrow \left(G\in \mathrm{USGraph}\wedge V\in \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfusgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		fveq2	$$⊢g=G\to \mathrm{Vtx}\left(g\right)=\mathrm{Vtx}\left(G\right)$$
3	2 1	eqtr4di	$$⊢g=G\to \mathrm{Vtx}\left(g\right)=V$$
4	3	eleq1d	$$⊢g=G\to \left(\mathrm{Vtx}\left(g\right)\in \mathrm{Fin}\leftrightarrow V\in \mathrm{Fin}\right)$$
5		df-fusgr	$$⊢\mathrm{FinUSGraph}=\left\{g\in \mathrm{USGraph}|\mathrm{Vtx}\left(g\right)\in \mathrm{Fin}\right\}$$
6	4 5	elrab2	$$⊢G\in \mathrm{FinUSGraph}\leftrightarrow \left(G\in \mathrm{USGraph}\wedge V\in \mathrm{Fin}\right)$$