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 26254
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 26253 . 2 class FinUSGraph
2 vg . . . . . 6 setvar 𝑔
32cv 1522 . . . . 5 class 𝑔
4 cvtx 25919 . . . . 5 class Vtx
53, 4cfv 5926 . . . 4 class (Vtx‘𝑔)
6 cfn 7997 . . . 4 class Fin
75, 6wcel 2030 . . 3 wff (Vtx‘𝑔) ∈ Fin
8 cusgr 26089 . . 3 class USGraph
97, 2, 8crab 2945 . 2 class {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
101, 9wceq 1523 1 wff FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
Colors of variables: wff setvar class
This definition is referenced by:  isfusgr  26255
  Copyright terms: Public domain W3C validator