Theorem konigsbergssiedgwpr

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	⊢ 𝑉 = ( 0 ... 3 )
	konigsberg.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
	konigsberg.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion	konigsbergssiedgwpr	⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ∧ 𝐸 = ( 𝐴 ++ 𝐵 ) ) → 𝐴 ∈ 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	1 2 3	konigsbergiedgw	⊢ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
5	4	jctr	⊢ ( 𝐸 = ( 𝐴 ++ 𝐵 ) → ( 𝐸 = ( 𝐴 ++ 𝐵 ) ∧ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
6		ccatrcl1	⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ∧ ( 𝐸 = ( 𝐴 ++ 𝐵 ) ∧ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) → 𝐴 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
7	5 6	syl3an3	⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ∧ 𝐸 = ( 𝐴 ++ 𝐵 ) ) → 𝐴 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )