Theorem usgrss

Description: An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 15-Oct-2020)

	Ref	Expression
Hypotheses	usgrf1o.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
	usgrss.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	usgrss	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in \mathrm{dom}E\right)\to E\left(X\right)\subseteq V$$

Proof

Step	Hyp	Ref	Expression
1		usgrf1o.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
2		usgrss.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
3		ssrab2	$$⊢\left\{x\in 𝒫V|\left|x\right|=2\right\}\subseteq 𝒫V$$
4	2 1	usgrfs	$$⊢G\in \mathrm{USGraph}\to E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
5		f1f	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}\to E:\mathrm{dom}E⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
6	4 5	syl	$$⊢G\in \mathrm{USGraph}\to E:\mathrm{dom}E⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
7	6	ffvelcdmda	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in \mathrm{dom}E\right)\to E\left(X\right)\in \left\{x\in 𝒫V|\left|x\right|=2\right\}$$
8	3 7	sselid	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in \mathrm{dom}E\right)\to E\left(X\right)\in 𝒫V$$
9	8	elpwid	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in \mathrm{dom}E\right)\to E\left(X\right)\subseteq V$$