Theorem umgredgnlp

Description: An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020) (Revised by AV, 8-Jun-2021)

	Ref	Expression
Hypothesis	umgredgnlp.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	umgredgnlp	$$⊢\left(G\in \mathrm{UMGraph}\wedge C\in E\right)\to \neg \exists vC=\left\{v\right\}$$

Proof

Step	Hyp	Ref	Expression
1		umgredgnlp.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
2		vex	$$⊢v\in \mathrm{V}$$
3		hashsng	$$⊢v\in \mathrm{V}\to \left|\left\{v\right\}\right|=1$$
4		1ne2	$$⊢1\ne 2$$
5	4	neii	$$⊢\neg 1=2$$
6		eqeq1	$$⊢\left|\left\{v\right\}\right|=1\to \left(\left|\left\{v\right\}\right|=2\leftrightarrow 1=2\right)$$
7	5 6	mtbiri	$$⊢\left|\left\{v\right\}\right|=1\to \neg \left|\left\{v\right\}\right|=2$$
8	2 3 7	mp2b	$$⊢\neg \left|\left\{v\right\}\right|=2$$
9		fveqeq2	$$⊢C=\left\{v\right\}\to \left(\left|C\right|=2\leftrightarrow \left|\left\{v\right\}\right|=2\right)$$
10	8 9	mtbiri	$$⊢C=\left\{v\right\}\to \neg \left|C\right|=2$$
11	10	intnand	$$⊢C=\left\{v\right\}\to \neg \left(C\in 𝒫\mathrm{Vtx}\left(G\right)\wedge \left|C\right|=2\right)$$
12	1	eleq2i	$$⊢C\in E\leftrightarrow C\in \mathrm{Edg}\left(G\right)$$
13		edgumgr	$$⊢\left(G\in \mathrm{UMGraph}\wedge C\in \mathrm{Edg}\left(G\right)\right)\to \left(C\in 𝒫\mathrm{Vtx}\left(G\right)\wedge \left|C\right|=2\right)$$
14	12 13	sylan2b	$$⊢\left(G\in \mathrm{UMGraph}\wedge C\in E\right)\to \left(C\in 𝒫\mathrm{Vtx}\left(G\right)\wedge \left|C\right|=2\right)$$
15	11 14	nsyl3	$$⊢\left(G\in \mathrm{UMGraph}\wedge C\in E\right)\to \neg C=\left\{v\right\}$$
16	15	nexdv	$$⊢\left(G\in \mathrm{UMGraph}\wedge C\in E\right)\to \neg \exists vC=\left\{v\right\}$$