Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-subgr | Structured version Visualization version Unicode version |
Description: Define the class of the subgraph relation. A class is a subgraph of a class (the supergraph of ) if its vertices are also vertices of , and its edges are also edges of , connecting vertices of only (see section I.1 in [Bollobas] p. 2 or section 1.1 in [Diestel] p. 4). The second condition is ensured by the requirement that the edge function of is a restriction of the edge function of having only vertices of in its range. Note that the domains of the edge functions of the subgraph and the supergraph should be compatible. (Contributed by AV, 16-Nov-2020.) |
Ref | Expression |
---|---|
df-subgr | SubGraph Vtx Vtx iEdg iEdg iEdg Edg Vtx |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csubgr 26159 | . 2 SubGraph | |
2 | vs | . . . . . . 7 | |
3 | 2 | cv 1482 | . . . . . 6 |
4 | cvtx 25874 | . . . . . 6 Vtx | |
5 | 3, 4 | cfv 5888 | . . . . 5 Vtx |
6 | vg | . . . . . . 7 | |
7 | 6 | cv 1482 | . . . . . 6 |
8 | 7, 4 | cfv 5888 | . . . . 5 Vtx |
9 | 5, 8 | wss 3574 | . . . 4 Vtx Vtx |
10 | ciedg 25875 | . . . . . 6 iEdg | |
11 | 3, 10 | cfv 5888 | . . . . 5 iEdg |
12 | 7, 10 | cfv 5888 | . . . . . 6 iEdg |
13 | 11 | cdm 5114 | . . . . . 6 iEdg |
14 | 12, 13 | cres 5116 | . . . . 5 iEdg iEdg |
15 | 11, 14 | wceq 1483 | . . . 4 iEdg iEdg iEdg |
16 | cedg 25939 | . . . . . 6 Edg | |
17 | 3, 16 | cfv 5888 | . . . . 5 Edg |
18 | 5 | cpw 4158 | . . . . 5 Vtx |
19 | 17, 18 | wss 3574 | . . . 4 Edg Vtx |
20 | 9, 15, 19 | w3a 1037 | . . 3 Vtx Vtx iEdg iEdg iEdg Edg Vtx |
21 | 20, 2, 6 | copab 4712 | . 2 Vtx Vtx iEdg iEdg iEdg Edg Vtx |
22 | 1, 21 | wceq 1483 | 1 SubGraph Vtx Vtx iEdg iEdg iEdg Edg Vtx |
Colors of variables: wff setvar class |
This definition is referenced by: relsubgr 26161 issubgr 26163 |
Copyright terms: Public domain | W3C validator |