Metamath Proof Explorer

Theorem konigsbergssiedgw

Description: Each subset of 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 = 0 … 3
konigsberg.e ⊢ E = ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 2 3 ”⟩
konigsberg.g ⊢ G = V E
Assertion konigsbergssiedgw ⊢ A ∈ Word V ∧ B ∈ Word V ∧ E = A ++ B → A ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2

Proof

Step Hyp Ref Expression
1 konigsberg.v ⊢ V = 0 … 3
2 konigsberg.e ⊢ E = ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 2 3 ”⟩
3 konigsberg.g ⊢ G = V E
4 1 2 3 konigsbergssiedgwpr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ E = A ++ B → A ∈ Word x ∈ 𝒫 V | x = 2
5 wrdf ⊢ A ∈ Word x ∈ 𝒫 V | x = 2 → A : 0 ..^ A ⟶ x ∈ 𝒫 V | x = 2
6 prprrab ⊢ x ∈ 𝒫 V ∖ ∅ | x = 2 = x ∈ 𝒫 V | x = 2
7 2re ⊢ 2 ∈ ℝ
8 7 eqlei2 ⊢ x = 2 → x ≤ 2
9 8 a1i ⊢ x ∈ 𝒫 V ∖ ∅ → x = 2 → x ≤ 2
10 9 ss2rabi ⊢ x ∈ 𝒫 V ∖ ∅ | x = 2 ⊆ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
11 6 10 eqsstrri ⊢ x ∈ 𝒫 V | x = 2 ⊆ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
12 fss ⊢ A : 0 ..^ A ⟶ x ∈ 𝒫 V | x = 2 ∧ x ∈ 𝒫 V | x = 2 ⊆ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 → A : 0 ..^ A ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
13 11 12 mpan2 ⊢ A : 0 ..^ A ⟶ x ∈ 𝒫 V | x = 2 → A : 0 ..^ A ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
14 iswrdb ⊢ A ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2 ↔ A : 0 ..^ A ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
15 13 14 sylibr ⊢ A : 0 ..^ A ⟶ x ∈ 𝒫 V | x = 2 → A ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2
16 4 5 15 3syl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ E = A ++ B → A ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2