Definition df-subgr 29285

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

Assertion

Ref	Expression
df-subgr	⊢ SubGraph = {⟨𝑠, 𝑔⟩ ∣ ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))}

Distinct variable group:   𝑔,𝑠

Detailed syntax breakdown of Definition df-subgr

Step	Hyp	Ref	Expression
1		csubgr 29284	. 2 class SubGraph
2		vs	. . . . . . 7 setvar 𝑠
3	2	cv 1539	. . . . . 6 class 𝑠
4		cvtx 29013	. . . . . 6 class Vtx
5	3, 4	cfv 6561	. . . . 5 class (Vtx‘𝑠)
6		vg	. . . . . . 7 setvar 𝑔
7	6	cv 1539	. . . . . 6 class 𝑔
8	7, 4	cfv 6561	. . . . 5 class (Vtx‘𝑔)
9	5, 8	wss 3951	. . . 4 wff (Vtx‘𝑠) ⊆ (Vtx‘𝑔)
10		ciedg 29014	. . . . . 6 class iEdg
11	3, 10	cfv 6561	. . . . 5 class (iEdg‘𝑠)
12	7, 10	cfv 6561	. . . . . 6 class (iEdg‘𝑔)
13	11	cdm 5685	. . . . . 6 class dom (iEdg‘𝑠)
14	12, 13	cres 5687	. . . . 5 class ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠))
15	11, 14	wceq 1540	. . . 4 wff (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠))
16		cedg 29064	. . . . . 6 class Edg
17	3, 16	cfv 6561	. . . . 5 class (Edg‘𝑠)
18	5	cpw 4600	. . . . 5 class 𝒫 (Vtx‘𝑠)
19	17, 18	wss 3951	. . . 4 wff (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠)
20	9, 15, 19	w3a 1087	. . 3 wff ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))
21	20, 2, 6	copab 5205	. 2 class {⟨𝑠, 𝑔⟩ ∣ ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))}
22	1, 21	wceq 1540	1 wff SubGraph = {⟨𝑠, 𝑔⟩ ∣ ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))}

This definition is referenced by:  relsubgr  29286  issubgr  29288