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 ⊒ 𝑉 = ( 0 ... 3 )
konigsberg.e ⊒ 𝐸 = βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ©
konigsberg.g ⊒ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion konigsberglem5 2 < ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } )

Proof

Step Hyp Ref Expression
1 konigsberg.v ⊒ 𝑉 = ( 0 ... 3 )
2 konigsberg.e ⊒ 𝐸 = βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ©
3 konigsberg.g ⊒ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 1 2 3 konigsberglem4 ⊒ { 0 , 1 , 3 } βŠ† { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) }
5 1 ovexi ⊒ 𝑉 ∈ V
6 5 rabex ⊒ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ∈ V
7 hashss ⊒ ( ( { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ∈ V ∧ { 0 , 1 , 3 } βŠ† { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) β†’ ( β™― β€˜ { 0 , 1 , 3 } ) ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) )
8 6 7 mpan ⊒ ( { 0 , 1 , 3 } βŠ† { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } β†’ ( β™― β€˜ { 0 , 1 , 3 } ) ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) )
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 ) ↔ ( β™― β€˜ { 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 } ) ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) ↔ 3 ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) )
22 df-3 ⊒ 3 = ( 2 + 1 )
23 22 breq1i ⊒ ( 3 ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) ↔ ( 2 + 1 ) ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) )
24 2z ⊒ 2 ∈ β„€
25 fzfi ⊒ ( 0 ... 3 ) ∈ Fin
26 1 25 eqeltri ⊒ 𝑉 ∈ Fin
27 rabfi ⊒ ( 𝑉 ∈ Fin β†’ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ∈ Fin )
28 hashcl ⊒ ( { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ∈ Fin β†’ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) ∈ β„•0 )
29 26 27 28 mp2b ⊒ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) ∈ β„•0
30 29 nn0zi ⊒ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) ∈ β„€
31 zltp1le ⊒ ( ( 2 ∈ β„€ ∧ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) ∈ β„€ ) β†’ ( 2 < ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) ↔ ( 2 + 1 ) ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) ) )
32 24 30 31 mp2an ⊒ ( 2 < ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) ↔ ( 2 + 1 ) ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) )
33 23 32 sylbb2 ⊒ ( 3 ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) β†’ 2 < ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) )
34 21 33 sylbi ⊒ ( ( β™― β€˜ { 0 , 1 , 3 } ) ≀ ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) β†’ 2 < ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } ) )
35 4 8 34 mp2b ⊒ 2 < ( β™― β€˜ { π‘₯ ∈ 𝑉 ∣ Β¬ 2 βˆ₯ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘₯ ) } )