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 ⊆ Vtx ⁡ g ∧ iEdg ⁡ s = iEdg ⁡ g ↾ dom ⁡ iEdg ⁡ s ∧ Edg ⁡ s ⊆ 𝒫 Vtx ⁡ s

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubgr class SubGraph
1 vs setvar s
2 vg setvar g
3 cvtx class Vtx
4 1 cv setvar s
5 4 3 cfv class Vtx ⁡ s
6 2 cv setvar g
7 6 3 cfv class Vtx ⁡ g
8 5 7 wss wff Vtx ⁡ s ⊆ Vtx ⁡ g
9 ciedg class iEdg
10 4 9 cfv class iEdg ⁡ s
11 6 9 cfv class iEdg ⁡ g
12 10 cdm class dom ⁡ iEdg ⁡ s
13 11 12 cres class iEdg ⁡ g ↾ dom ⁡ iEdg ⁡ s
14 10 13 wceq wff iEdg ⁡ s = iEdg ⁡ g ↾ dom ⁡ iEdg ⁡ s
15 cedg class Edg
16 4 15 cfv class Edg ⁡ s
17 5 cpw class 𝒫 Vtx ⁡ s
18 16 17 wss wff Edg ⁡ s ⊆ 𝒫 Vtx ⁡ s
19 8 14 18 w3a wff Vtx ⁡ s ⊆ Vtx ⁡ g ∧ iEdg ⁡ s = iEdg ⁡ g ↾ dom ⁡ iEdg ⁡ s ∧ Edg ⁡ s ⊆ 𝒫 Vtx ⁡ s
20 19 1 2 copab class s g | Vtx ⁡ s ⊆ Vtx ⁡ g ∧ iEdg ⁡ s = iEdg ⁡ g ↾ dom ⁡ iEdg ⁡ s ∧ Edg ⁡ s ⊆ 𝒫 Vtx ⁡ s
21 0 20 wceq wff SubGraph = s g | Vtx ⁡ s ⊆ Vtx ⁡ g ∧ iEdg ⁡ s = iEdg ⁡ g ↾ dom ⁡ iEdg ⁡ s ∧ Edg ⁡ s ⊆ 𝒫 Vtx ⁡ s