This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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