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	⊢ 𝑉 = ( 0 ... 3 )
	konigsberg.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
	konigsberg.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion	konigsbergiedgw	⊢ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }

Proof

Step	Hyp	Ref	Expression
1		konigsberg.v	⊢ 𝑉 = ( 0 ... 3 )
2		konigsberg.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
3		konigsberg.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4		3nn0	⊢ 3 ∈ ℕ0
5		0elfz	⊢ ( 3 ∈ ℕ0 → 0 ∈ ( 0 ... 3 ) )
6	4 5	ax-mp	⊢ 0 ∈ ( 0 ... 3 )
7		1nn0	⊢ 1 ∈ ℕ0
8		1le3	⊢ 1 ≤ 3
9		elfz2nn0	⊢ ( 1 ∈ ( 0 ... 3 ) ↔ ( 1 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 1 ≤ 3 ) )
10	7 4 8 9	mpbir3an	⊢ 1 ∈ ( 0 ... 3 )
11		0ne1	⊢ 0 ≠ 1
12	6 10 11	umgrbi	⊢ { 0 , 1 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
13	12	a1i	⊢ ( ⊤ → { 0 , 1 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
14		2nn0	⊢ 2 ∈ ℕ0
15		2re	⊢ 2 ∈ ℝ
16		3re	⊢ 3 ∈ ℝ
17		2lt3	⊢ 2 < 3
18	15 16 17	ltleii	⊢ 2 ≤ 3
19		elfz2nn0	⊢ ( 2 ∈ ( 0 ... 3 ) ↔ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 2 ≤ 3 ) )
20	14 4 18 19	mpbir3an	⊢ 2 ∈ ( 0 ... 3 )
21		0ne2	⊢ 0 ≠ 2
22	6 20 21	umgrbi	⊢ { 0 , 2 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
23	22	a1i	⊢ ( ⊤ → { 0 , 2 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
24		nn0fz0	⊢ ( 3 ∈ ℕ0 ↔ 3 ∈ ( 0 ... 3 ) )
25	4 24	mpbi	⊢ 3 ∈ ( 0 ... 3 )
26		3ne0	⊢ 3 ≠ 0
27	26	necomi	⊢ 0 ≠ 3
28	6 25 27	umgrbi	⊢ { 0 , 3 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
29	28	a1i	⊢ ( ⊤ → { 0 , 3 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
30		1ne2	⊢ 1 ≠ 2
31	10 20 30	umgrbi	⊢ { 1 , 2 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
32	31	a1i	⊢ ( ⊤ → { 1 , 2 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
33	15 17	ltneii	⊢ 2 ≠ 3
34	20 25 33	umgrbi	⊢ { 2 , 3 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
35	34	a1i	⊢ ( ⊤ → { 2 , 3 } ∈ { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
36	13 23 29 32 32 35 35	s7cld	⊢ ( ⊤ → ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
37	36	mptru	⊢ ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
38	1	pweqi	⊢ 𝒫 𝑉 = 𝒫 ( 0 ... 3 )
39	38	rabeqi	⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
40	39	wrdeqi	⊢ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } = Word { 𝑥 ∈ 𝒫 ( 0 ... 3 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
41	37 2 40	3eltr4i	⊢ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }