Metamath Proof Explorer

Theorem konigsberglem4

Description: Lemma 4 for konigsberg : Vertices 0 , 1 , 3 are vertices of odd degree. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised 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 konigsberglem4 
|- { 0 , 1 , 3 } C_ { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) }

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 6 1 eleqtrri 
 |-  0 e. V
8 n2dvds3 
 |-  -. 2 || 3
9 1 2 3 konigsberglem1 
 |-  ( ( VtxDeg ` G ) ` 0 ) = 3
10 9 breq2i 
 |-  ( 2 || ( ( VtxDeg ` G ) ` 0 ) <-> 2 || 3 )
11 8 10 mtbir 
 |-  -. 2 || ( ( VtxDeg ` G ) ` 0 )
12 fveq2 
 |-  ( x = 0 -> ( ( VtxDeg ` G ) ` x ) = ( ( VtxDeg ` G ) ` 0 ) )
13 12 breq2d 
 |-  ( x = 0 -> ( 2 || ( ( VtxDeg ` G ) ` x ) <-> 2 || ( ( VtxDeg ` G ) ` 0 ) ) )
14 13 notbid 
 |-  ( x = 0 -> ( -. 2 || ( ( VtxDeg ` G ) ` x ) <-> -. 2 || ( ( VtxDeg ` G ) ` 0 ) ) )
15 14 elrab 
 |-  ( 0 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } <-> ( 0 e. V /\ -. 2 || ( ( VtxDeg ` G ) ` 0 ) ) )
16 7 11 15 mpbir2an 
 |-  0 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) }
17 1nn0 
 |-  1 e. NN0
18 1le3 
 |-  1 <_ 3
19 elfz2nn0 
 |-  ( 1 e. ( 0 ... 3 ) <-> ( 1 e. NN0 /\ 3 e. NN0 /\ 1 <_ 3 ) )
20 17 4 18 19 mpbir3an 
 |-  1 e. ( 0 ... 3 )
21 20 1 eleqtrri 
 |-  1 e. V
22 1 2 3 konigsberglem2 
 |-  ( ( VtxDeg ` G ) ` 1 ) = 3
23 22 breq2i 
 |-  ( 2 || ( ( VtxDeg ` G ) ` 1 ) <-> 2 || 3 )
24 8 23 mtbir 
 |-  -. 2 || ( ( VtxDeg ` G ) ` 1 )
25 fveq2 
 |-  ( x = 1 -> ( ( VtxDeg ` G ) ` x ) = ( ( VtxDeg ` G ) ` 1 ) )
26 25 breq2d 
 |-  ( x = 1 -> ( 2 || ( ( VtxDeg ` G ) ` x ) <-> 2 || ( ( VtxDeg ` G ) ` 1 ) ) )
27 26 notbid 
 |-  ( x = 1 -> ( -. 2 || ( ( VtxDeg ` G ) ` x ) <-> -. 2 || ( ( VtxDeg ` G ) ` 1 ) ) )
28 27 elrab 
 |-  ( 1 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } <-> ( 1 e. V /\ -. 2 || ( ( VtxDeg ` G ) ` 1 ) ) )
29 21 24 28 mpbir2an 
 |-  1 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) }
30 3re 
 |-  3 e. RR
31 30 leidi 
 |-  3 <_ 3
32 elfz2nn0 
 |-  ( 3 e. ( 0 ... 3 ) <-> ( 3 e. NN0 /\ 3 e. NN0 /\ 3 <_ 3 ) )
33 4 4 31 32 mpbir3an 
 |-  3 e. ( 0 ... 3 )
34 33 1 eleqtrri 
 |-  3 e. V
35 1 2 3 konigsberglem3 
 |-  ( ( VtxDeg ` G ) ` 3 ) = 3
36 35 breq2i 
 |-  ( 2 || ( ( VtxDeg ` G ) ` 3 ) <-> 2 || 3 )
37 8 36 mtbir 
 |-  -. 2 || ( ( VtxDeg ` G ) ` 3 )
38 fveq2 
 |-  ( x = 3 -> ( ( VtxDeg ` G ) ` x ) = ( ( VtxDeg ` G ) ` 3 ) )
39 38 breq2d 
 |-  ( x = 3 -> ( 2 || ( ( VtxDeg ` G ) ` x ) <-> 2 || ( ( VtxDeg ` G ) ` 3 ) ) )
40 39 notbid 
 |-  ( x = 3 -> ( -. 2 || ( ( VtxDeg ` G ) ` x ) <-> -. 2 || ( ( VtxDeg ` G ) ` 3 ) ) )
41 40 elrab 
 |-  ( 3 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } <-> ( 3 e. V /\ -. 2 || ( ( VtxDeg ` G ) ` 3 ) ) )
42 34 37 41 mpbir2an 
 |-  3 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) }
43 16 29 42 3pm3.2i 
 |-  ( 0 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } /\ 1 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } /\ 3 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } )
44 c0ex 
 |-  0 e. _V
45 1ex 
 |-  1 e. _V
46 3ex 
 |-  3 e. _V
47 44 45 46 tpss 
 |-  ( ( 0 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } /\ 1 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } /\ 3 e. { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) <-> { 0 , 1 , 3 } C_ { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } )
48 43 47 mpbi 
 |-  { 0 , 1 , 3 } C_ { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) }