Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-cplgr | Structured version Visualization version GIF version |
Description: Define the class of all complete "graphs". A class/graph is called complete if every pair of distinct vertices is connected by an edge, i.e., each vertex has all other vertices as neighbors or, in other words, each vertex is a universal vertex. (Contributed by AV, 24-Oct-2020.) (Revised by TA, 15-Feb-2022.) |
Ref | Expression |
---|---|
df-cplgr | ⊢ ComplGraph = {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccplgr 27118 | . 2 class ComplGraph | |
2 | vg | . . . . . 6 setvar 𝑔 | |
3 | 2 | cv 1527 | . . . . 5 class 𝑔 |
4 | cuvtx 27094 | . . . . 5 class UnivVtx | |
5 | 3, 4 | cfv 6348 | . . . 4 class (UnivVtx‘𝑔) |
6 | cvtx 26708 | . . . . 5 class Vtx | |
7 | 3, 6 | cfv 6348 | . . . 4 class (Vtx‘𝑔) |
8 | 5, 7 | wceq 1528 | . . 3 wff (UnivVtx‘𝑔) = (Vtx‘𝑔) |
9 | 8, 2 | cab 2796 | . 2 class {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)} |
10 | 1, 9 | wceq 1528 | 1 wff ComplGraph = {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)} |
Colors of variables: wff setvar class |
This definition is referenced by: cplgruvtxb 27122 |
Copyright terms: Public domain | W3C validator |