Metamath Proof Explorer

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 
|- 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 konigsbergiedgw 
|- E 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 3nn0 
 |-  3 e. NN0
5 0elfz 
 |-  ( 3 e. NN0 -> 0 e. ( 0 ... 3 ) )
6 4 5 ax-mp 
 |-  0 e. ( 0 ... 3 )
7 1nn0 
 |-  1 e. NN0
8 1le3 
 |-  1 <_ 3
9 elfz2nn0 
 |-  ( 1 e. ( 0 ... 3 ) <-> ( 1 e. NN0 /\ 3 e. NN0 /\ 1 <_ 3 ) )
10 7 4 8 9 mpbir3an 
 |-  1 e. ( 0 ... 3 )
11 0ne1 
 |-  0 =/= 1
12 6 10 11 umgrbi 
 |-  { 0 , 1 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 }
13 12 a1i 
 |-  ( T. -> { 0 , 1 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 } )
14 2nn0 
 |-  2 e. NN0
15 2re 
 |-  2 e. RR
16 3re 
 |-  3 e. RR
17 2lt3 
 |-  2 < 3
18 15 16 17 ltleii 
 |-  2 <_ 3
19 elfz2nn0 
 |-  ( 2 e. ( 0 ... 3 ) <-> ( 2 e. NN0 /\ 3 e. NN0 /\ 2 <_ 3 ) )
20 14 4 18 19 mpbir3an 
 |-  2 e. ( 0 ... 3 )
21 0ne2 
 |-  0 =/= 2
22 6 20 21 umgrbi 
 |-  { 0 , 2 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 }
23 22 a1i 
 |-  ( T. -> { 0 , 2 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 } )
24 nn0fz0 
 |-  ( 3 e. NN0 <-> 3 e. ( 0 ... 3 ) )
25 4 24 mpbi 
 |-  3 e. ( 0 ... 3 )
26 3ne0 
 |-  3 =/= 0
27 26 necomi 
 |-  0 =/= 3
28 6 25 27 umgrbi 
 |-  { 0 , 3 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 }
29 28 a1i 
 |-  ( T. -> { 0 , 3 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 } )
30 1ne2 
 |-  1 =/= 2
31 10 20 30 umgrbi 
 |-  { 1 , 2 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 }
32 31 a1i 
 |-  ( T. -> { 1 , 2 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 } )
33 15 17 ltneii 
 |-  2 =/= 3
34 20 25 33 umgrbi 
 |-  { 2 , 3 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 }
35 34 a1i 
 |-  ( T. -> { 2 , 3 } e. { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 } )
36 13 23 29 32 32 35 35 s7cld 
 |-  ( T. -> <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. Word { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 } )
37 36 mptru 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. Word { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 }
38 1 pweqi 
 |-  ~P V = ~P ( 0 ... 3 )
39 38 rabeqi 
 |-  { x e. ~P V | ( # ` x ) = 2 } = { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 }
40 39 wrdeqi 
 |-  Word { x e. ~P V | ( # ` x ) = 2 } = Word { x e. ~P ( 0 ... 3 ) | ( # ` x ) = 2 }
41 37 2 40 3eltr4i 
 |-  E e. Word { x e. ~P V | ( # ` x ) = 2 }