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 ‘ 𝐺 ) ‘ 𝑥 ) } )