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 = ( 𝑔 ∈ 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 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) ⟩ )