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 ⊢ 𝑉 = ( 0 ... 3 )
konigsberg.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
konigsberg.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion konigsberglem4 { 0 , 1 , 3 } ⊆ { 𝑥 ∈ 𝑉 ∣ ¬ 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 3nn0 ⊢ 3 ∈ ℕ0
5 0elfz ⊢ ( 3 ∈ ℕ0 → 0 ∈ ( 0 ... 3 ) )
6 4 5 ax-mp ⊢ 0 ∈ ( 0 ... 3 )
7 6 1 eleqtrri ⊢ 0 ∈ 𝑉
8 n2dvds3 ⊢ ¬ 2 ∥ 3
9 1 2 3 konigsberglem1 ⊢ ( ( VtxDeg ‘ 𝐺 ) ‘ 0 ) = 3
10 9 breq2i ⊢ ( 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 0 ) ↔ 2 ∥ 3 )
11 8 10 mtbir ⊢ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 0 )
12 fveq2 ⊢ ( 𝑥 = 0 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 0 ) )
13 12 breq2d ⊢ ( 𝑥 = 0 → ( 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 0 ) ) )
14 13 notbid ⊢ ( 𝑥 = 0 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 0 ) ) )
15 14 elrab ⊢ ( 0 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ↔ ( 0 ∈ 𝑉 ∧ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 0 ) ) )
16 7 11 15 mpbir2an ⊢ 0 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) }
17 1nn0 ⊢ 1 ∈ ℕ0
18 1le3 ⊢ 1 ≤ 3
19 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 3 ) ↔ ( 1 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 1 ≤ 3 ) )
20 17 4 18 19 mpbir3an ⊢ 1 ∈ ( 0 ... 3 )
21 20 1 eleqtrri ⊢ 1 ∈ 𝑉
22 1 2 3 konigsberglem2 ⊢ ( ( VtxDeg ‘ 𝐺 ) ‘ 1 ) = 3
23 22 breq2i ⊢ ( 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 1 ) ↔ 2 ∥ 3 )
24 8 23 mtbir ⊢ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 1 )
25 fveq2 ⊢ ( 𝑥 = 1 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 1 ) )
26 25 breq2d ⊢ ( 𝑥 = 1 → ( 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 1 ) ) )
27 26 notbid ⊢ ( 𝑥 = 1 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 1 ) ) )
28 27 elrab ⊢ ( 1 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ↔ ( 1 ∈ 𝑉 ∧ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 1 ) ) )
29 21 24 28 mpbir2an ⊢ 1 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) }
30 3re ⊢ 3 ∈ ℝ
31 30 leidi ⊢ 3 ≤ 3
32 elfz2nn0 ⊢ ( 3 ∈ ( 0 ... 3 ) ↔ ( 3 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 ≤ 3 ) )
33 4 4 31 32 mpbir3an ⊢ 3 ∈ ( 0 ... 3 )
34 33 1 eleqtrri ⊢ 3 ∈ 𝑉
35 1 2 3 konigsberglem3 ⊢ ( ( VtxDeg ‘ 𝐺 ) ‘ 3 ) = 3
36 35 breq2i ⊢ ( 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 3 ) ↔ 2 ∥ 3 )
37 8 36 mtbir ⊢ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 3 )
38 fveq2 ⊢ ( 𝑥 = 3 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 3 ) )
39 38 breq2d ⊢ ( 𝑥 = 3 → ( 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 3 ) ) )
40 39 notbid ⊢ ( 𝑥 = 3 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 3 ) ) )
41 40 elrab ⊢ ( 3 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ↔ ( 3 ∈ 𝑉 ∧ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 3 ) ) )
42 34 37 41 mpbir2an ⊢ 3 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) }
43 16 29 42 3pm3.2i ⊢ ( 0 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ∧ 1 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ∧ 3 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } )
44 c0ex ⊢ 0 ∈ V
45 1ex ⊢ 1 ∈ V
46 3ex ⊢ 3 ∈ V
47 44 45 46 tpss ⊢ ( ( 0 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ∧ 1 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ∧ 3 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ↔ { 0 , 1 , 3 } ⊆ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } )
48 43 47 mpbi ⊢ { 0 , 1 , 3 } ⊆ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) }