MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fusgr Structured version   Visualization version   GIF version

Definition df-fusgr 27026
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.)
Assertion
Ref Expression
df-fusgr FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}

Detailed syntax breakdown of Definition df-fusgr
StepHypRef Expression
1 cfusgr 27025 . 2 class FinUSGraph
2 vg . . . . . 6 setvar 𝑔
32cv 1527 . . . . 5 class 𝑔
4 cvtx 26708 . . . . 5 class Vtx
53, 4cfv 6348 . . . 4 class (Vtx‘𝑔)
6 cfn 8497 . . . 4 class Fin
75, 6wcel 2105 . . 3 wff (Vtx‘𝑔) ∈ Fin
8 cusgr 26861 . . 3 class USGraph
97, 2, 8crab 3139 . 2 class {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
101, 9wceq 1528 1 wff FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
Colors of variables: wff setvar class
This definition is referenced by:  isfusgr  27027
  Copyright terms: Public domain W3C validator