Theorem upgrss

Description: An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 29-Nov-2020)

	Ref	Expression
Hypotheses	isupgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	isupgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
Assertion	upgrss	$$⊢\left(G\in \mathrm{UPGraph}\wedge F\in \mathrm{dom}E\right)\to E\left(F\right)\subseteq V$$

Proof

Step	Hyp	Ref	Expression
1		isupgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isupgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
3		ssrab2	$$⊢\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\subseteq 𝒫V\setminus \left\{\varnothing \right\}$$
4		difss	$$⊢𝒫V\setminus \left\{\varnothing \right\}\subseteq 𝒫V$$
5	3 4	sstri	$$⊢\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\subseteq 𝒫V$$
6	1 2	upgrf	$$⊢G\in \mathrm{UPGraph}\to E:\mathrm{dom}E⟶\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
7	6	ffvelcdmda	$$⊢\left(G\in \mathrm{UPGraph}\wedge F\in \mathrm{dom}E\right)\to E\left(F\right)\in \left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
8	5 7	sselid	$$⊢\left(G\in \mathrm{UPGraph}\wedge F\in \mathrm{dom}E\right)\to E\left(F\right)\in 𝒫V$$
9	8	elpwid	$$⊢\left(G\in \mathrm{UPGraph}\wedge F\in \mathrm{dom}E\right)\to E\left(F\right)\subseteq V$$