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 ⊒ 𝑉 = ( 0 ... 3 )
konigsberg.e ⊒ 𝐸 = βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ©
konigsberg.g ⊒ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion konigsbergssiedgw ( ( 𝐴 ∈ 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 konigsbergssiedgwpr ⊒ ( ( 𝐴 ∈ Word V ∧ 𝐡 ∈ Word V ∧ 𝐸 = ( 𝐴 ++ 𝐡 ) ) β†’ 𝐴 ∈ Word { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } )
5 wrdf ⊒ ( 𝐴 ∈ Word { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } β†’ 𝐴 : ( 0 ..^ ( β™― β€˜ 𝐴 ) ) ⟢ { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } )
6 prprrab ⊒ { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) = 2 } = { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 }
7 2re ⊒ 2 ∈ ℝ
8 7 eqlei2 ⊒ ( ( β™― β€˜ π‘₯ ) = 2 β†’ ( β™― β€˜ π‘₯ ) ≀ 2 )
9 8 a1i ⊒ ( π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) β†’ ( ( β™― β€˜ π‘₯ ) = 2 β†’ ( β™― β€˜ π‘₯ ) ≀ 2 ) )
10 9 ss2rabi ⊒ { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) = 2 } βŠ† { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 }
11 6 10 eqsstrri ⊒ { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } βŠ† { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 }
12 fss ⊒ ( ( 𝐴 : ( 0 ..^ ( β™― β€˜ 𝐴 ) ) ⟢ { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } ∧ { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } βŠ† { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 } ) β†’ 𝐴 : ( 0 ..^ ( β™― β€˜ 𝐴 ) ) ⟢ { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 } )
13 11 12 mpan2 ⊒ ( 𝐴 : ( 0 ..^ ( β™― β€˜ 𝐴 ) ) ⟢ { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } β†’ 𝐴 : ( 0 ..^ ( β™― β€˜ 𝐴 ) ) ⟢ { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 } )
14 iswrdb ⊒ ( 𝐴 ∈ Word { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 } ↔ 𝐴 : ( 0 ..^ ( β™― β€˜ 𝐴 ) ) ⟢ { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 } )
15 13 14 sylibr ⊒ ( 𝐴 : ( 0 ..^ ( β™― β€˜ 𝐴 ) ) ⟢ { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } β†’ 𝐴 ∈ Word { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 } )
16 4 5 15 3syl ⊒ ( ( 𝐴 ∈ Word V ∧ 𝐡 ∈ Word V ∧ 𝐸 = ( 𝐴 ++ 𝐡 ) ) β†’ 𝐴 ∈ Word { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 } )