Metamath Proof Explorer


Definition df-subgr

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 ) ) }

Detailed syntax breakdown

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 ) ) }