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	$$⊢\mathrm{SubGraph}=\left\{⟨s,g⟩|\left(\mathrm{Vtx}\left(s\right)\subseteq \mathrm{Vtx}\left(g\right)\wedge \mathrm{iEdg}\left(s\right)={\mathrm{iEdg}\left(g\right)\upharpoonright }_{\mathrm{dom}\mathrm{iEdg}\left(s\right)}\wedge \mathrm{Edg}\left(s\right)\subseteq 𝒫\mathrm{Vtx}\left(s\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubgr	$$class\mathrm{SubGraph}$$
1		vs	$$setvars$$
2		vg	$$setvarg$$
3		cvtx	$$class\mathrm{Vtx}$$
4	1	cv	$$setvars$$
5	4 3	cfv	$$class\mathrm{Vtx}\left(s\right)$$
6	2	cv	$$setvarg$$
7	6 3	cfv	$$class\mathrm{Vtx}\left(g\right)$$
8	5 7	wss	$$wff\mathrm{Vtx}\left(s\right)\subseteq \mathrm{Vtx}\left(g\right)$$
9		ciedg	$$class\mathrm{iEdg}$$
10	4 9	cfv	$$class\mathrm{iEdg}\left(s\right)$$
11	6 9	cfv	$$class\mathrm{iEdg}\left(g\right)$$
12	10	cdm	$$class\mathrm{dom}\mathrm{iEdg}\left(s\right)$$
13	11 12	cres	$$class\left({\mathrm{iEdg}\left(g\right)\upharpoonright }_{\mathrm{dom}\mathrm{iEdg}\left(s\right)}\right)$$
14	10 13	wceq	$$wff\mathrm{iEdg}\left(s\right)={\mathrm{iEdg}\left(g\right)\upharpoonright }_{\mathrm{dom}\mathrm{iEdg}\left(s\right)}$$
15		cedg	$$class\mathrm{Edg}$$
16	4 15	cfv	$$class\mathrm{Edg}\left(s\right)$$
17	5	cpw	$$class𝒫\mathrm{Vtx}\left(s\right)$$
18	16 17	wss	$$wff\mathrm{Edg}\left(s\right)\subseteq 𝒫\mathrm{Vtx}\left(s\right)$$
19	8 14 18	w3a	$$wff\left(\mathrm{Vtx}\left(s\right)\subseteq \mathrm{Vtx}\left(g\right)\wedge \mathrm{iEdg}\left(s\right)={\mathrm{iEdg}\left(g\right)\upharpoonright }_{\mathrm{dom}\mathrm{iEdg}\left(s\right)}\wedge \mathrm{Edg}\left(s\right)\subseteq 𝒫\mathrm{Vtx}\left(s\right)\right)$$
20	19 1 2	copab	$$class\left\{⟨s,g⟩|\left(\mathrm{Vtx}\left(s\right)\subseteq \mathrm{Vtx}\left(g\right)\wedge \mathrm{iEdg}\left(s\right)={\mathrm{iEdg}\left(g\right)\upharpoonright }_{\mathrm{dom}\mathrm{iEdg}\left(s\right)}\wedge \mathrm{Edg}\left(s\right)\subseteq 𝒫\mathrm{Vtx}\left(s\right)\right)\right\}$$
21	0 20	wceq	$$wff\mathrm{SubGraph}=\left\{⟨s,g⟩|\left(\mathrm{Vtx}\left(s\right)\subseteq \mathrm{Vtx}\left(g\right)\wedge \mathrm{iEdg}\left(s\right)={\mathrm{iEdg}\left(g\right)\upharpoonright }_{\mathrm{dom}\mathrm{iEdg}\left(s\right)}\wedge \mathrm{Edg}\left(s\right)\subseteq 𝒫\mathrm{Vtx}\left(s\right)\right)\right\}$$