Theorem konigsbergiedgw

Description: The indexed edges of the Königsberg graph G is a word over the pairs of vertices. (Contributed by AV, 28-Feb-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	konigsbergiedgw	$$⊢E\in \mathrm{Word}\left\{x\in 𝒫V|\left|x\right|=2\right\}$$

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		3nn0	$$⊢3\in {\mathbb{N}}_0$$
5		0elfz	$$⊢3\in {\mathbb{N}}_0\to 0\in \left(0\dots 3\right)$$
6	4 5	ax-mp	$$⊢0\in \left(0\dots 3\right)$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		1le3	$$⊢1\le 3$$
9		elfz2nn0	$$⊢1\in \left(0\dots 3\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\wedge 1\le 3\right)$$
10	7 4 8 9	mpbir3an	$$⊢1\in \left(0\dots 3\right)$$
11		0ne1	$$⊢0\ne 1$$
12	6 10 11	umgrbi	$$⊢\left\{0,1\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
13	12	a1i	$$⊢\top \to \left\{0,1\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
14		2nn0	$$⊢2\in {\mathbb{N}}_0$$
15		2re	$$⊢2\in ℝ$$
16		3re	$$⊢3\in ℝ$$
17		2lt3	$$⊢2<3$$
18	15 16 17	ltleii	$$⊢2\le 3$$
19		elfz2nn0	$$⊢2\in \left(0\dots 3\right)\leftrightarrow \left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\wedge 2\le 3\right)$$
20	14 4 18 19	mpbir3an	$$⊢2\in \left(0\dots 3\right)$$
21		0ne2	$$⊢0\ne 2$$
22	6 20 21	umgrbi	$$⊢\left\{0,2\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
23	22	a1i	$$⊢\top \to \left\{0,2\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
24		nn0fz0	$$⊢3\in {\mathbb{N}}_0\leftrightarrow 3\in \left(0\dots 3\right)$$
25	4 24	mpbi	$$⊢3\in \left(0\dots 3\right)$$
26		3ne0	$$⊢3\ne 0$$
27	26	necomi	$$⊢0\ne 3$$
28	6 25 27	umgrbi	$$⊢\left\{0,3\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
29	28	a1i	$$⊢\top \to \left\{0,3\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
30		1ne2	$$⊢1\ne 2$$
31	10 20 30	umgrbi	$$⊢\left\{1,2\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
32	31	a1i	$$⊢\top \to \left\{1,2\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
33	15 17	ltneii	$$⊢2\ne 3$$
34	20 25 33	umgrbi	$$⊢\left\{2,3\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
35	34	a1i	$$⊢\top \to \left\{2,3\right\}\in \left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
36	13 23 29 32 32 35 35	s7cld	$$⊢\top \to ⟨“\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}\left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
37	36	mptru	$$⊢⟨“\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}\left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
38	1	pweqi	$$⊢𝒫V=𝒫\left(0\dots 3\right)$$
39	38	rabeqi	$$⊢\left\{x\in 𝒫V|\left|x\right|=2\right\}=\left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
40	39	wrdeqi	$$⊢\mathrm{Word}\left\{x\in 𝒫V|\left|x\right|=2\right\}=\mathrm{Word}\left\{x\in 𝒫\left(0\dots 3\right)|\left|x\right|=2\right\}$$
41	37 2 40	3eltr4i	$$⊢E\in \mathrm{Word}\left\{x\in 𝒫V|\left|x\right|=2\right\}$$