Theorem upgrle

Description: An edge of an undirected pseudograph has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

	Ref	Expression
Hypotheses	isupgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	isupgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
Assertion	upgrle	$$⊢\left(G\in \mathrm{UPGraph}\wedge EFnA\wedge F\in A\right)\to \left|E\left(F\right)\right|\le 2$$

Proof

Step	Hyp	Ref	Expression
1		isupgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isupgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
3	1 2	upgrfn	$$⊢\left(G\in \mathrm{UPGraph}\wedge EFnA\right)\to E:A⟶\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
4	3	ffvelcdmda	$$⊢\left(\left(G\in \mathrm{UPGraph}\wedge EFnA\right)\wedge F\in A\right)\to E\left(F\right)\in \left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
5	4	3impa	$$⊢\left(G\in \mathrm{UPGraph}\wedge EFnA\wedge F\in A\right)\to E\left(F\right)\in \left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
6		fveq2	$$⊢x=E\left(F\right)\to \left|x\right|=\left|E\left(F\right)\right|$$
7	6	breq1d	$$⊢x=E\left(F\right)\to \left(\left|x\right|\le 2\leftrightarrow \left|E\left(F\right)\right|\le 2\right)$$
8	7	elrab	$$⊢E\left(F\right)\in \left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\leftrightarrow \left(E\left(F\right)\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)\wedge \left|E\left(F\right)\right|\le 2\right)$$
9	8	simprbi	$$⊢E\left(F\right)\in \left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\to \left|E\left(F\right)\right|\le 2$$
10	5 9	syl	$$⊢\left(G\in \mathrm{UPGraph}\wedge EFnA\wedge F\in A\right)\to \left|E\left(F\right)\right|\le 2$$