Definition df-isubgr 47733

Description: Define the function mapping graphs and subsets of their vertices to their induced subgraphs. A subgraph 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.)

Assertion

Ref	Expression
df-isubgr	⊢ ISubGr = (𝑔 ∈ V, 𝑣 ∈ 𝒫 (Vtx‘𝑔) ↦ ⟨𝑣, ⦋(iEdg‘𝑔) / 𝑒⦌(𝑒 ↾ {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) ⊆ 𝑣})⟩)

Distinct variable group:   𝑒,𝑔,𝑣,𝑥

Detailed syntax breakdown of Definition df-isubgr

Step	Hyp	Ref	Expression
1		cisubgr 47732	. 2 class ISubGr
2		vg	. . 3 setvar 𝑔
3		vv	. . 3 setvar 𝑣
4		cvv 3488	. . 3 class V
5	2	cv 1536	. . . . 5 class 𝑔
6		cvtx 29031	. . . . 5 class Vtx
7	5, 6	cfv 6573	. . . 4 class (Vtx‘𝑔)
8	7	cpw 4622	. . 3 class 𝒫 (Vtx‘𝑔)
9	3	cv 1536	. . . 4 class 𝑣
10		ve	. . . . 5 setvar 𝑒
11		ciedg 29032	. . . . . 6 class iEdg
12	5, 11	cfv 6573	. . . . 5 class (iEdg‘𝑔)
13	10	cv 1536	. . . . . 6 class 𝑒
14		vx	. . . . . . . . . 10 setvar 𝑥
15	14	cv 1536	. . . . . . . . 9 class 𝑥
16	15, 13	cfv 6573	. . . . . . . 8 class (𝑒‘𝑥)
17	16, 9	wss 3976	. . . . . . 7 wff (𝑒‘𝑥) ⊆ 𝑣
18	13	cdm 5700	. . . . . . 7 class dom 𝑒
19	17, 14, 18	crab 3443	. . . . . 6 class {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) ⊆ 𝑣}
20	13, 19	cres 5702	. . . . 5 class (𝑒 ↾ {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) ⊆ 𝑣})
21	10, 12, 20	csb 3921	. . . 4 class ⦋(iEdg‘𝑔) / 𝑒⦌(𝑒 ↾ {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) ⊆ 𝑣})
22	9, 21	cop 4654	. . 3 class ⟨𝑣, ⦋(iEdg‘𝑔) / 𝑒⦌(𝑒 ↾ {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) ⊆ 𝑣})⟩
23	2, 3, 4, 8, 22	cmpo 7450	. 2 class (𝑔 ∈ V, 𝑣 ∈ 𝒫 (Vtx‘𝑔) ↦ ⟨𝑣, ⦋(iEdg‘𝑔) / 𝑒⦌(𝑒 ↾ {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) ⊆ 𝑣})⟩)
24	1, 23	wceq 1537	1 wff ISubGr = (𝑔 ∈ V, 𝑣 ∈ 𝒫 (Vtx‘𝑔) ↦ ⟨𝑣, ⦋(iEdg‘𝑔) / 𝑒⦌(𝑒 ↾ {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) ⊆ 𝑣})⟩)

This definition is referenced by:  isisubgr  47734