Metamath Proof Explorer

Theorem eupth2lem3lem7

Description: Lemma for eupth2lem3 : Combining trlsegvdeg , eupth2lem3lem3 , eupth2lem3lem4 and eupth2lem3lem6 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 27-Feb-2021)

Ref Expression
Hypotheses trlsegvdeg.v ⊢ V = Vtx ⁡ G
trlsegvdeg.i ⊢ I = iEdg ⁡ G
trlsegvdeg.f ⊢ φ → Fun ⁡ I
trlsegvdeg.n ⊢ φ → N ∈ 0 ..^ F
trlsegvdeg.u ⊢ φ → U ∈ V
trlsegvdeg.w ⊢ φ → F Trails ⁡ G P
trlsegvdeg.vx ⊢ φ → Vtx ⁡ X = V
trlsegvdeg.vy ⊢ φ → Vtx ⁡ Y = V
trlsegvdeg.vz ⊢ φ → Vtx ⁡ Z = V
trlsegvdeg.ix ⊢ φ → iEdg ⁡ X = I ↾ F 0 ..^ N
trlsegvdeg.iy ⊢ φ → iEdg ⁡ Y = F ⁡ N I ⁡ F ⁡ N
trlsegvdeg.iz ⊢ φ → iEdg ⁡ Z = I ↾ F 0 … N
eupth2lem3.o ⊢ φ → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ X ⁡ x = if P ⁡ 0 = P ⁡ N ∅ P ⁡ 0 P ⁡ N
eupth2lem3.e ⊢ φ → I ⁡ F ⁡ N = P ⁡ N P ⁡ N + 1
Assertion eupth2lem3lem7 ⊢ φ → ¬ 2 ∥ VtxDeg ⁡ Z ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1

Proof

Step Hyp Ref Expression
1 trlsegvdeg.v ⊢ V = Vtx ⁡ G
2 trlsegvdeg.i ⊢ I = iEdg ⁡ G
3 trlsegvdeg.f ⊢ φ → Fun ⁡ I
4 trlsegvdeg.n ⊢ φ → N ∈ 0 ..^ F
5 trlsegvdeg.u ⊢ φ → U ∈ V
6 trlsegvdeg.w ⊢ φ → F Trails ⁡ G P
7 trlsegvdeg.vx ⊢ φ → Vtx ⁡ X = V
8 trlsegvdeg.vy ⊢ φ → Vtx ⁡ Y = V
9 trlsegvdeg.vz ⊢ φ → Vtx ⁡ Z = V
10 trlsegvdeg.ix ⊢ φ → iEdg ⁡ X = I ↾ F 0 ..^ N
11 trlsegvdeg.iy ⊢ φ → iEdg ⁡ Y = F ⁡ N I ⁡ F ⁡ N
12 trlsegvdeg.iz ⊢ φ → iEdg ⁡ Z = I ↾ F 0 … N
13 eupth2lem3.o ⊢ φ → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ X ⁡ x = if P ⁡ 0 = P ⁡ N ∅ P ⁡ 0 P ⁡ N
14 eupth2lem3.e ⊢ φ → I ⁡ F ⁡ N = P ⁡ N P ⁡ N + 1
15 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeg ⊢ φ → VtxDeg ⁡ Z ⁡ U = VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U
16 15 breq2d ⊢ φ → 2 ∥ VtxDeg ⁡ Z ⁡ U ↔ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U
17 16 notbid ⊢ φ → ¬ 2 ∥ VtxDeg ⁡ Z ⁡ U ↔ ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U
18 ifpprsnss ⊢ I ⁡ F ⁡ N = P ⁡ N P ⁡ N + 1 → if- P ⁡ N = P ⁡ N + 1 I ⁡ F ⁡ N = P ⁡ N P ⁡ N P ⁡ N + 1 ⊆ I ⁡ F ⁡ N
19 14 18 syl ⊢ φ → if- P ⁡ N = P ⁡ N + 1 I ⁡ F ⁡ N = P ⁡ N P ⁡ N P ⁡ N + 1 ⊆ I ⁡ F ⁡ N
20 1 2 3 4 5 6 7 8 9 10 11 12 13 19 eupth2lem3lem3 ⊢ φ ∧ P ⁡ N = P ⁡ N + 1 → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 eupth2lem3lem5 ⊢ φ → I ⁡ F ⁡ N ∈ 𝒫 V
22 1 2 3 4 5 6 7 8 9 10 11 12 13 19 21 eupth2lem3lem4 ⊢ φ ∧ P ⁡ N ≠ P ⁡ N + 1 ∧ U = P ⁡ N ∨ U = P ⁡ N + 1 → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
23 22 3expa ⊢ φ ∧ P ⁡ N ≠ P ⁡ N + 1 ∧ U = P ⁡ N ∨ U = P ⁡ N + 1 → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
24 23 expcom ⊢ U = P ⁡ N ∨ U = P ⁡ N + 1 → φ ∧ P ⁡ N ≠ P ⁡ N + 1 → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
25 neanior ⊢ U ≠ P ⁡ N ∧ U ≠ P ⁡ N + 1 ↔ ¬ U = P ⁡ N ∨ U = P ⁡ N + 1
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 eupth2lem3lem6 ⊢ φ ∧ P ⁡ N ≠ P ⁡ N + 1 ∧ U ≠ P ⁡ N ∧ U ≠ P ⁡ N + 1 → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
27 26 3expa ⊢ φ ∧ P ⁡ N ≠ P ⁡ N + 1 ∧ U ≠ P ⁡ N ∧ U ≠ P ⁡ N + 1 → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
28 27 expcom ⊢ U ≠ P ⁡ N ∧ U ≠ P ⁡ N + 1 → φ ∧ P ⁡ N ≠ P ⁡ N + 1 → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
29 25 28 sylbir ⊢ ¬ U = P ⁡ N ∨ U = P ⁡ N + 1 → φ ∧ P ⁡ N ≠ P ⁡ N + 1 → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
30 24 29 pm2.61i ⊢ φ ∧ P ⁡ N ≠ P ⁡ N + 1 → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
31 20 30 pm2.61dane ⊢ φ → ¬ 2 ∥ VtxDeg ⁡ X ⁡ U + VtxDeg ⁡ Y ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1
32 17 31 bitrd ⊢ φ → ¬ 2 ∥ VtxDeg ⁡ Z ⁡ U ↔ U ∈ if P ⁡ 0 = P ⁡ N + 1 ∅ P ⁡ 0 P ⁡ N + 1