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