This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }