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

Metamath Proof Explorer

Definition df-subgr

Description: Define the class of the subgraph relation. A class s is a subgraph of a class g (thesupergraph of s ) if its vertices are also vertices of g , and its edges are also edges of g , connecting vertices of s only (see section I.1 in Bollobas p. 2 or section 1.1 in Diestel p. 4). The second condition is ensured by the requirement that the edge function of s is a restriction of the edge function of g having only vertices of s in its range. Note that the domains of the edge functions of the subgraph and the supergraph should be compatible. (Contributed by AV, 16-Nov-2020)

Ref Expression
Assertion df-subgr SubGraph = { ⟨ 𝑠 , 𝑔 ⟩ ∣ ( ( Vtx ‘ 𝑠 ) ⊆ ( Vtx ‘ 𝑔 ) ∧ ( iEdg ‘ 𝑠 ) = ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) ) ∧ ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubgr ⊢ SubGraph
1 vs ⊢ 𝑠
2 vg ⊢ 𝑔
3 cvtx ⊢ Vtx
4 1 cv ⊢ 𝑠
5 4 3 cfv ⊢ ( Vtx ‘ 𝑠 )
6 2 cv ⊢ 𝑔
7 6 3 cfv ⊢ ( Vtx ‘ 𝑔 )
8 5 7 wss ⊢ ( Vtx ‘ 𝑠 ) ⊆ ( Vtx ‘ 𝑔 )
9 ciedg ⊢ iEdg
10 4 9 cfv ⊢ ( iEdg ‘ 𝑠 )
11 6 9 cfv ⊢ ( iEdg ‘ 𝑔 )
12 10 cdm ⊢ dom ( iEdg ‘ 𝑠 )
13 11 12 cres ⊢ ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) )
14 10 13 wceq ⊢ ( iEdg ‘ 𝑠 ) = ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) )
15 cedg ⊢ Edg
16 4 15 cfv ⊢ ( Edg ‘ 𝑠 )
17 5 cpw ⊢ 𝒫 ( Vtx ‘ 𝑠 )
18 16 17 wss ⊢ ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 )
19 8 14 18 w3a ⊢ ( ( Vtx ‘ 𝑠 ) ⊆ ( Vtx ‘ 𝑔 ) ∧ ( iEdg ‘ 𝑠 ) = ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) ) ∧ ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 ) )
20 19 1 2 copab ⊢ { ⟨ 𝑠 , 𝑔 ⟩ ∣ ( ( Vtx ‘ 𝑠 ) ⊆ ( Vtx ‘ 𝑔 ) ∧ ( iEdg ‘ 𝑠 ) = ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) ) ∧ ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 ) ) }
21 0 20 wceq ⊢ SubGraph = { ⟨ 𝑠 , 𝑔 ⟩ ∣ ( ( Vtx ‘ 𝑠 ) ⊆ ( Vtx ‘ 𝑔 ) ∧ ( iEdg ‘ 𝑠 ) = ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) ) ∧ ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 ) ) }