Definition df-subgr 16104

Description: Define the class of the subgraph relation. A class s is a subgraph of a class g (the supergraph 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.)

Assertion

Ref	Expression
df-subgr	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }

Distinct variable group:   g, s

Detailed syntax breakdown of Definition df-subgr

Step	Hyp	Ref	Expression
1		csubgr 16103	. 2 class SubGraph
2		vs	. . . . . . 7 setvar s
3	2	cv 1396	. . . . . 6 class s
4		cvtx 15862	. . . . . 6 class Vtx
5	3, 4	cfv 5326	. . . . 5 class (Vtx ` s )
6		vg	. . . . . . 7 setvar g
7	6	cv 1396	. . . . . 6 class g
8	7, 4	cfv 5326	. . . . 5 class (Vtx ` g )
9	5, 8	wss 3200	. . . 4 wff (Vtx ` s ) C_ (Vtx ` g )
10		ciedg 15863	. . . . . 6 class iEdg
11	3, 10	cfv 5326	. . . . 5 class (iEdg ` s )
12	7, 10	cfv 5326	. . . . . 6 class (iEdg ` g )
13	11	cdm 4725	. . . . . 6 class dom (iEdg ` s )
14	12, 13	cres 4727	. . . . 5 class ( (iEdg ` g ) |` dom (iEdg ` s ) )
15	11, 14	wceq 1397	. . . 4 wff (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) )
16		cedg 15907	. . . . . 6 class Edg
17	3, 16	cfv 5326	. . . . 5 class (Edg ` s )
18	5	cpw 3652	. . . . 5 class ~P (Vtx ` s )
19	17, 18	wss 3200	. . . 4 wff (Edg ` s ) C_ ~P (Vtx ` s )
20	9, 15, 19	w3a 1004	. . 3 wff ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) )
21	20, 2, 6	copab 4149	. 2 class { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
22	1, 21	wceq 1397	1 wff SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }

This definition is referenced by:  relsubgr  16105  issubgr  16107