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 = ( 𝑔 ∈ V , 𝑣 ∈ 𝒫 ( Vtx ‘ 𝑔 ) ↦ ⟨ 𝑣 , ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cisubgr	⊢ ISubGr
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vv	⊢ 𝑣
4		cvtx	⊢ Vtx
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Vtx ‘ 𝑔 )
7	6	cpw	⊢ 𝒫 ( Vtx ‘ 𝑔 )
8	3	cv	⊢ 𝑣
9		ciedg	⊢ iEdg
10	5 9	cfv	⊢ ( iEdg ‘ 𝑔 )
11		ve	⊢ 𝑒
12	11	cv	⊢ 𝑒
13		vx	⊢ 𝑥
14	12	cdm	⊢ dom 𝑒
15	13	cv	⊢ 𝑥
16	15 12	cfv	⊢ ( 𝑒 ‘ 𝑥 )
17	16 8	wss	⊢ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣
18	17 13 14	crab	⊢ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 }
19	12 18	cres	⊢ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } )
20	11 10 19	csb	⊢ ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } )
21	8 20	cop	⊢ ⟨ 𝑣 , ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) ⟩
22	1 3 2 7 21	cmpo	⊢ ( 𝑔 ∈ V , 𝑣 ∈ 𝒫 ( Vtx ‘ 𝑔 ) ↦ ⟨ 𝑣 , ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) ⟩ )
23	0 22	wceq	⊢ ISubGr = ( 𝑔 ∈ V , 𝑣 ∈ 𝒫 ( Vtx ‘ 𝑔 ) ↦ ⟨ 𝑣 , ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) ⟩ )