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=⟨“01020312122323”⟩
konigsberg.g ⊢G=VE
Assertion konigsberglem5 ⊢2<x∈V|¬2∥VtxDeg⁡G⁡x

Proof

Step Hyp Ref Expression
1 konigsberg.v ⊢V=0…3
2 konigsberg.e ⊢E=⟨“01020312122323”⟩
3 konigsberg.g ⊢G=VE
4 1 2 3 konigsberglem4 ⊢013⊆x∈V|¬2∥VtxDeg⁡G⁡x
5 1 ovexi ⊢V∈V
6 5 rabex ⊢x∈V|¬2∥VtxDeg⁡G⁡x∈V
7 hashss ⊢x∈V|¬2∥VtxDeg⁡G⁡x∈V∧013⊆x∈V|¬2∥VtxDeg⁡G⁡x→013≤x∈V|¬2∥VtxDeg⁡G⁡x
8 6 7 mpan ⊢013⊆x∈V|¬2∥VtxDeg⁡G⁡x→013≤x∈V|¬2∥VtxDeg⁡G⁡x
9 0ne1 ⊢0≠1
10 1re ⊢1∈ℝ
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∈V
16 1ex ⊢1∈V
17 3ex ⊢3∈V
18 hashtpg ⊢0∈V∧1∈V∧3∈V→0≠1∧1≠3∧3≠0↔013=3
19 15 16 17 18 mp3an ⊢0≠1∧1≠3∧3≠0↔013=3
20 14 19 mpbi ⊢013=3
21 20 breq1i ⊢013≤x∈V|¬2∥VtxDeg⁡G⁡x↔3≤x∈V|¬2∥VtxDeg⁡G⁡x
22 df-3 ⊢3=2+1
23 22 breq1i ⊢3≤x∈V|¬2∥VtxDeg⁡G⁡x↔2+1≤x∈V|¬2∥VtxDeg⁡G⁡x
24 2z ⊢2∈ℤ
25 fzfi ⊢0…3∈Fin
26 1 25 eqeltri ⊢V∈Fin
27 rabfi ⊢V∈Fin→x∈V|¬2∥VtxDeg⁡G⁡x∈Fin
28 hashcl ⊢x∈V|¬2∥VtxDeg⁡G⁡x∈Fin→x∈V|¬2∥VtxDeg⁡G⁡x∈ℕ0
29 26 27 28 mp2b ⊢x∈V|¬2∥VtxDeg⁡G⁡x∈ℕ0
30 29 nn0zi ⊢x∈V|¬2∥VtxDeg⁡G⁡x∈ℤ
31 zltp1le ⊢2∈ℤ∧x∈V|¬2∥VtxDeg⁡G⁡x∈ℤ→2<x∈V|¬2∥VtxDeg⁡G⁡x↔2+1≤x∈V|¬2∥VtxDeg⁡G⁡x
32 24 30 31 mp2an ⊢2<x∈V|¬2∥VtxDeg⁡G⁡x↔2+1≤x∈V|¬2∥VtxDeg⁡G⁡x
33 23 32 sylbb2 ⊢3≤x∈V|¬2∥VtxDeg⁡G⁡x→2<x∈V|¬2∥VtxDeg⁡G⁡x
34 21 33 sylbi ⊢013≤x∈V|¬2∥VtxDeg⁡G⁡x→2<x∈V|¬2∥VtxDeg⁡G⁡x
35 4 8 34 mp2b ⊢2<x∈V|¬2∥VtxDeg⁡G⁡x