Metamath Proof Explorer

Theorem konigsberglem5

Description: Lemma 5 for konigsberg : The set of vertices of odd degree is greater than 2. (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 konigsberglem5 
|- 2 < ( # ` { 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 1 2 3 konigsberglem4 
 |-  { 0 , 1 , 3 } C_ { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) }
5 1 ovexi 
 |-  V e. _V
6 5 rabex 
 |-  { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } e. _V
7 hashss 
 |-  ( ( { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } e. _V /\ { 0 , 1 , 3 } C_ { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) -> ( # ` { 0 , 1 , 3 } ) <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
8 6 7 mpan 
 |-  ( { 0 , 1 , 3 } C_ { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } -> ( # ` { 0 , 1 , 3 } ) <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
9 0ne1 
 |-  0 =/= 1
10 1re 
 |-  1 e. RR
11 1lt3 
 |-  1 < 3
12 10 11 ltneii 
 |-  1 =/= 3
13 3ne0 
 |-  3 =/= 0
14 9 12 13 3pm3.2i 
 |-  ( 0 =/= 1 /\ 1 =/= 3 /\ 3 =/= 0 )
15 c0ex 
 |-  0 e. _V
16 1ex 
 |-  1 e. _V
17 3ex 
 |-  3 e. _V
18 hashtpg 
 |-  ( ( 0 e. _V /\ 1 e. _V /\ 3 e. _V ) -> ( ( 0 =/= 1 /\ 1 =/= 3 /\ 3 =/= 0 ) <-> ( # ` { 0 , 1 , 3 } ) = 3 ) )
19 15 16 17 18 mp3an 
 |-  ( ( 0 =/= 1 /\ 1 =/= 3 /\ 3 =/= 0 ) <-> ( # ` { 0 , 1 , 3 } ) = 3 )
20 14 19 mpbi 
 |-  ( # ` { 0 , 1 , 3 } ) = 3
21 20 breq1i 
 |-  ( ( # ` { 0 , 1 , 3 } ) <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) <-> 3 <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
22 df-3 
 |-  3 = ( 2 + 1 )
23 22 breq1i 
 |-  ( 3 <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) <-> ( 2 + 1 ) <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
24 2z 
 |-  2 e. ZZ
25 fzfi 
 |-  ( 0 ... 3 ) e. Fin
26 1 25 eqeltri 
 |-  V e. Fin
27 rabfi 
 |-  ( V e. Fin -> { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } e. Fin )
28 hashcl 
 |-  ( { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } e. Fin -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. NN0 )
29 26 27 28 mp2b 
 |-  ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. NN0
30 29 nn0zi 
 |-  ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. ZZ
31 zltp1le 
 |-  ( ( 2 e. ZZ /\ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. ZZ ) -> ( 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) <-> ( 2 + 1 ) <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) ) )
32 24 30 31 mp2an 
 |-  ( 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) <-> ( 2 + 1 ) <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
33 23 32 sylbb2 
 |-  ( 3 <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) -> 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
34 21 33 sylbi 
 |-  ( ( # ` { 0 , 1 , 3 } ) <_ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) -> 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
35 4 8 34 mp2b 
 |-  2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } )