MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-subgr Structured version   Visualization version   GIF version

Definition df-subgr 26977
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
StepHypRef Expression
1 csubgr 26976 . 2 class SubGraph
2 vs . . . . . . 7 setvar 𝑠
32cv 1527 . . . . . 6 class 𝑠
4 cvtx 26708 . . . . . 6 class Vtx
53, 4cfv 6348 . . . . 5 class (Vtx‘𝑠)
6 vg . . . . . . 7 setvar 𝑔
76cv 1527 . . . . . 6 class 𝑔
87, 4cfv 6348 . . . . 5 class (Vtx‘𝑔)
95, 8wss 3933 . . . 4 wff (Vtx‘𝑠) ⊆ (Vtx‘𝑔)
10 ciedg 26709 . . . . . 6 class iEdg
113, 10cfv 6348 . . . . 5 class (iEdg‘𝑠)
127, 10cfv 6348 . . . . . 6 class (iEdg‘𝑔)
1311cdm 5548 . . . . . 6 class dom (iEdg‘𝑠)
1412, 13cres 5550 . . . . 5 class ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠))
1511, 14wceq 1528 . . . 4 wff (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠))
16 cedg 26759 . . . . . 6 class Edg
173, 16cfv 6348 . . . . 5 class (Edg‘𝑠)
185cpw 4535 . . . . 5 class 𝒫 (Vtx‘𝑠)
1917, 18wss 3933 . . . 4 wff (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠)
209, 15, 19w3a 1079 . . 3 wff ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))
2120, 2, 6copab 5119 . 2 class {⟨𝑠, 𝑔⟩ ∣ ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))}
221, 21wceq 1528 1 wff SubGraph = {⟨𝑠, 𝑔⟩ ∣ ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))}
Colors of variables: wff setvar class
This definition is referenced by:  relsubgr  26978  issubgr  26980
  Copyright terms: Public domain W3C validator