Definition df-fusgr

Description: Define the class of all finite undirected simple graphs without loops (called "finite simple graphs" in the following). A finite simple graph is an undirected simple graph of finite order, i.e. with a finite set of vertices. (Contributed by AV, 3-Jan-2020) (Revised by AV, 21-Oct-2020)

	Ref	Expression
Assertion	df-fusgr	⊢ FinUSGraph = { 𝑔 ∈ USGraph ∣ ( Vtx ‘ 𝑔 ) ∈ Fin }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfusgr	⊢ FinUSGraph
1		vg	⊢ 𝑔
2		cusgr	⊢ USGraph
3		cvtx	⊢ Vtx
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( Vtx ‘ 𝑔 )
6		cfn	⊢ Fin
7	5 6	wcel	⊢ ( Vtx ‘ 𝑔 ) ∈ Fin
8	7 1 2	crab	⊢ { 𝑔 ∈ USGraph ∣ ( Vtx ‘ 𝑔 ) ∈ Fin }
9	0 8	wceq	⊢ FinUSGraph = { 𝑔 ∈ USGraph ∣ ( Vtx ‘ 𝑔 ) ∈ Fin }