Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fusgr Structured version   Visualization version   GIF version

Definition df-fusgr 40531
Description: Define the class of all finite undirected simple graphs without loops (called "finite simple graphs" in the following). A finite 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 40530 . 2 class FinUSGraph
2 vg . . . . . 6 setvar 𝑔
32cv 1473 . . . . 5 class 𝑔
4 cvtx 40224 . . . . 5 class Vtx
53, 4cfv 5790 . . . 4 class (Vtx‘𝑔)
6 cfn 7818 . . . 4 class Fin
75, 6wcel 1976 . . 3 wff (Vtx‘𝑔) ∈ Fin
8 cusgr 40374 . . 3 class USGraph
97, 2, 8crab 2899 . 2 class {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
101, 9wceq 1474 1 wff FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
Colors of variables: wff setvar class
This definition is referenced by:  isfusgr  40532
  Copyright terms: Public domain W3C validator