This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 } ) >. )