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 e. Word _V /\ B e. Word _V /\ E = ( A ++ B ) ) -> A e. Word { x e. ( ~P 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 e. Word _V /\ B e. Word _V /\ E = ( A ++ B ) ) -> A e. Word { x e. ~P V | ( # ` x ) = 2 } )
5 wrdf 
 |-  ( A e. Word { x e. ~P V | ( # ` x ) = 2 } -> A : ( 0 ..^ ( # ` A ) ) --> { x e. ~P V | ( # ` x ) = 2 } )
6 prprrab 
 |-  { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } = { x e. ~P V | ( # ` x ) = 2 }
7 2re 
 |-  2 e. RR
8 7 eqlei2 
 |-  ( ( # ` x ) = 2 -> ( # ` x ) <_ 2 )
9 8 a1i 
 |-  ( x e. ( ~P V \ { (/) } ) -> ( ( # ` x ) = 2 -> ( # ` x ) <_ 2 ) )
10 9 ss2rabi 
 |-  { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } C_ { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 }
11 6 10 eqsstrri 
 |-  { x e. ~P V | ( # ` x ) = 2 } C_ { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 }
12 fss 
 |-  ( ( A : ( 0 ..^ ( # ` A ) ) --> { x e. ~P V | ( # ` x ) = 2 } /\ { x e. ~P V | ( # ` x ) = 2 } C_ { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) -> A : ( 0 ..^ ( # ` A ) ) --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
13 11 12 mpan2 
 |-  ( A : ( 0 ..^ ( # ` A ) ) --> { x e. ~P V | ( # ` x ) = 2 } -> A : ( 0 ..^ ( # ` A ) ) --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
14 iswrdb 
 |-  ( A e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } <-> A : ( 0 ..^ ( # ` A ) ) --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
15 13 14 sylibr 
 |-  ( A : ( 0 ..^ ( # ` A ) ) --> { x e. ~P V | ( # ` x ) = 2 } -> A e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
16 4 5 15 3syl 
 |-  ( ( A e. Word _V /\ B e. Word _V /\ E = ( A ++ B ) ) -> A e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )