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 e. _V , v e. ~P ( Vtx ` g ) |-> <. v , [_ ( iEdg ` g ) / e ]_ ( e |` { x e. dom e | ( e ` x ) C_ v } ) >. )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cisubgr	|- ISubGr
1		vg	|- g
2		cvv	|- _V
3		vv	|- v
4		cvtx	|- Vtx
5	1	cv	|- g
6	5 4	cfv	|- ( Vtx ` g )
7	6	cpw	|- ~P ( Vtx ` g )
8	3	cv	|- v
9		ciedg	|- iEdg
10	5 9	cfv	|- ( iEdg ` g )
11		ve	|- e
12	11	cv	|- e
13		vx	|- x
14	12	cdm	|- dom e
15	13	cv	|- x
16	15 12	cfv	|- ( e ` x )
17	16 8	wss	|- ( e ` x ) C_ v
18	17 13 14	crab	|- { x e. dom e | ( e ` x ) C_ v }
19	12 18	cres	|- ( e |` { x e. dom e | ( e ` x ) C_ v } )
20	11 10 19	csb	|- [_ ( iEdg ` g ) / e ]_ ( e |` { x e. dom e | ( e ` x ) C_ v } )
21	8 20	cop	|- <. v , [_ ( iEdg ` g ) / e ]_ ( e |` { x e. dom e | ( e ` x ) C_ v } ) >.
22	1 3 2 7 21	cmpo	|- ( g e. _V , v e. ~P ( Vtx ` g ) |-> <. v , [_ ( iEdg ` g ) / e ]_ ( e |` { x e. dom e | ( e ` x ) C_ v } ) >. )
23	0 22	wceq	|- ISubGr = ( g e. _V , v e. ~P ( Vtx ` g ) |-> <. v , [_ ( iEdg ` g ) / e ]_ ( e |` { x e. dom e | ( e ` x ) C_ v } ) >. )