Theorem subgrprop2

Description: The properties of a subgraph: If S is a subgraph of G , its vertices are also vertices of G , and its edges are also edges of G , connecting vertices of the subgraph only. (Contributed by AV, 19-Nov-2020)

	Ref	Expression
Hypotheses	issubgr.v	$$⊢V=\mathrm{Vtx}\left(S\right)$$
	issubgr.a	$$⊢A=\mathrm{Vtx}\left(G\right)$$
	issubgr.i	$$⊢I=\mathrm{iEdg}\left(S\right)$$
	issubgr.b	$$⊢B=\mathrm{iEdg}\left(G\right)$$
	issubgr.e	$$⊢E=\mathrm{Edg}\left(S\right)$$
Assertion	subgrprop2	$$⊢S\mathrm{SubGraph}G\to \left(V\subseteq A\wedge I\subseteq B\wedge E\subseteq 𝒫V\right)$$

Proof

Step	Hyp	Ref	Expression
1		issubgr.v	$$⊢V=\mathrm{Vtx}\left(S\right)$$
2		issubgr.a	$$⊢A=\mathrm{Vtx}\left(G\right)$$
3		issubgr.i	$$⊢I=\mathrm{iEdg}\left(S\right)$$
4		issubgr.b	$$⊢B=\mathrm{iEdg}\left(G\right)$$
5		issubgr.e	$$⊢E=\mathrm{Edg}\left(S\right)$$
6	1 2 3 4 5	subgrprop	$$⊢S\mathrm{SubGraph}G\to \left(V\subseteq A\wedge I={B\upharpoonright }_{\mathrm{dom}I}\wedge E\subseteq 𝒫V\right)$$
7		resss	$$⊢{B\upharpoonright }_{\mathrm{dom}I}\subseteq B$$
8		sseq1	$$⊢I={B\upharpoonright }_{\mathrm{dom}I}\to \left(I\subseteq B\leftrightarrow {B\upharpoonright }_{\mathrm{dom}I}\subseteq B\right)$$
9	7 8	mpbiri	$$⊢I={B\upharpoonright }_{\mathrm{dom}I}\to I\subseteq B$$
10	9	3anim2i	$$⊢\left(V\subseteq A\wedge I={B\upharpoonright }_{\mathrm{dom}I}\wedge E\subseteq 𝒫V\right)\to \left(V\subseteq A\wedge I\subseteq B\wedge E\subseteq 𝒫V\right)$$
11	6 10	syl	$$⊢S\mathrm{SubGraph}G\to \left(V\subseteq A\wedge I\subseteq B\wedge E\subseteq 𝒫V\right)$$