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 ‘ 𝑠 ) ) }