Theorem konigsbergumgr

Description: The Königsberg graph G is a multigraph. (Contributed by AV, 28-Feb-2021) (Revised by AV, 9-Mar-2021)

	Ref	Expression
Hypotheses	konigsberg.v	$$⊢V=\left(0\dots 3\right)$$
	konigsberg.e	$$⊢E=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$
	konigsberg.g	$$⊢G=⟨V,E⟩$$
Assertion	konigsbergumgr	$$⊢G\in \mathrm{UMGraph}$$

Proof

Step	Hyp	Ref	Expression
1		konigsberg.v	$$⊢V=\left(0\dots 3\right)$$
2		konigsberg.e	$$⊢E=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$
3		konigsberg.g	$$⊢G=⟨V,E⟩$$
4	1 2 3	konigsbergiedgw	$$⊢E\in \mathrm{Word}\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
5		opex	$$⊢⟨V,E⟩\in \mathrm{V}$$
6	3 5	eqeltri	$$⊢G\in \mathrm{V}$$
7		s7cli	$$⊢⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩\in \mathrm{Word}\mathrm{V}$$
8	2 7	eqeltri	$$⊢E\in \mathrm{Word}\mathrm{V}$$
9	1 2 3	konigsbergvtx	$$⊢\mathrm{Vtx}\left(G\right)=\left(0\dots 3\right)$$
10	1 9	eqtr4i	$$⊢V=\mathrm{Vtx}\left(G\right)$$
11	1 2 3	konigsbergiedg	$$⊢\mathrm{iEdg}\left(G\right)=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$
12	2 11	eqtr4i	$$⊢E=\mathrm{iEdg}\left(G\right)$$
13	10 12	wrdumgr	$$⊢\left(G\in \mathrm{V}\wedge E\in \mathrm{Word}\mathrm{V}\right)\to \left(G\in \mathrm{UMGraph}\leftrightarrow E\in \mathrm{Word}\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$
14	6 8 13	mp2an	$$⊢G\in \mathrm{UMGraph}\leftrightarrow E\in \mathrm{Word}\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
15	4 14	mpbir	$$⊢G\in \mathrm{UMGraph}$$