Metamath Proof Explorer

Definition df-isubgr

Description: Define the function mapping graphs and subsets of their vertices to their induced subgraphs. Asubgraph induced by a subset of vertices of a graph is a subgraph of the graph which contains all edges of the graph that join vertices of the subgraph (see section I.1 in Bollobas p. 2 or section 1.1 in Diestel p. 4). Although a graph may be given in any meaningful representation, its induced subgraphs are always ordered pairs of vertices and edges. (Contributed by AV, 27-Apr-2025)

Ref Expression
Assertion df-isubgr ⊢ ISubGr = g ∈ V , v ∈ 𝒫 Vtx ⁡ g ⟼ v ⦋ iEdg ⁡ g / e⦌ e ↾ x ∈ dom ⁡ e | e ⁡ x ⊆ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cisubgr class ISubGr
1 vg setvar g
2 cvv class V
3 vv setvar v
4 cvtx class Vtx
5 1 cv setvar g
6 5 4 cfv class Vtx ⁡ g
7 6 cpw class 𝒫 Vtx ⁡ g
8 3 cv setvar v
9 ciedg class iEdg
10 5 9 cfv class iEdg ⁡ g
11 ve setvar e
12 11 cv setvar e
13 vx setvar x
14 12 cdm class dom ⁡ e
15 13 cv setvar x
16 15 12 cfv class e ⁡ x
17 16 8 wss wff e ⁡ x ⊆ v
18 17 13 14 crab class x ∈ dom ⁡ e | e ⁡ x ⊆ v
19 12 18 cres class e ↾ x ∈ dom ⁡ e | e ⁡ x ⊆ v
20 11 10 19 csb class ⦋ iEdg ⁡ g / e⦌ e ↾ x ∈ dom ⁡ e | e ⁡ x ⊆ v
21 8 20 cop class v ⦋ iEdg ⁡ g / e⦌ e ↾ x ∈ dom ⁡ e | e ⁡ x ⊆ v
22 1 3 2 7 21 cmpo class g ∈ V , v ∈ 𝒫 Vtx ⁡ g ⟼ v ⦋ iEdg ⁡ g / e⦌ e ↾ x ∈ dom ⁡ e | e ⁡ x ⊆ v
23 0 22 wceq wff ISubGr = g ∈ V , v ∈ 𝒫 Vtx ⁡ g ⟼ v ⦋ iEdg ⁡ g / e⦌ e ↾ x ∈ dom ⁡ e | e ⁡ x ⊆ v