Description: Define the class of the subgraph relation. A class s is a subgraph of a class g (thesupergraph of s ) if its vertices are also vertices of g , and its edges are also edges of g , connecting vertices of s 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 s is a restriction of the edge function of g having only vertices of s 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 | ||
---|---|---|---|
Assertion | df-subgr | |- SubGraph = { <. s , g >. | ( ( Vtx ` s ) C_ ( Vtx ` g ) /\ ( iEdg ` s ) = ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) /\ ( Edg ` s ) C_ ~P ( Vtx ` s ) ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | csubgr | |- SubGraph |
|
1 | vs | |- s |
|
2 | vg | |- g |
|
3 | cvtx | |- Vtx |
|
4 | 1 | cv | |- s |
5 | 4 3 | cfv | |- ( Vtx ` s ) |
6 | 2 | cv | |- g |
7 | 6 3 | cfv | |- ( Vtx ` g ) |
8 | 5 7 | wss | |- ( Vtx ` s ) C_ ( Vtx ` g ) |
9 | ciedg | |- iEdg |
|
10 | 4 9 | cfv | |- ( iEdg ` s ) |
11 | 6 9 | cfv | |- ( iEdg ` g ) |
12 | 10 | cdm | |- dom ( iEdg ` s ) |
13 | 11 12 | cres | |- ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) |
14 | 10 13 | wceq | |- ( iEdg ` s ) = ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) |
15 | cedg | |- Edg |
|
16 | 4 15 | cfv | |- ( Edg ` s ) |
17 | 5 | cpw | |- ~P ( Vtx ` s ) |
18 | 16 17 | wss | |- ( Edg ` s ) C_ ~P ( Vtx ` s ) |
19 | 8 14 18 | w3a | |- ( ( Vtx ` s ) C_ ( Vtx ` g ) /\ ( iEdg ` s ) = ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) /\ ( Edg ` s ) C_ ~P ( Vtx ` s ) ) |
20 | 19 1 2 | copab | |- { <. s , g >. | ( ( Vtx ` s ) C_ ( Vtx ` g ) /\ ( iEdg ` s ) = ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) /\ ( Edg ` s ) C_ ~P ( Vtx ` s ) ) } |
21 | 0 20 | wceq | |- SubGraph = { <. s , g >. | ( ( Vtx ` s ) C_ ( Vtx ` g ) /\ ( iEdg ` s ) = ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) /\ ( Edg ` s ) C_ ~P ( Vtx ` s ) ) } |