Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eupth2lem3lem4 Structured version   Visualization version   GIF version

Theorem eupth2lem3lem4 41394
Description: Lemma for eupth2lem3 41399, formerly part of proof of eupath2lem3 26272: If an edge (not a loop) is added to a trail, the degree of the end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.)
Hypotheses
Ref Expression
trlsegvdeg.v 𝑉 = (Vtx‘𝐺)
trlsegvdeg.i 𝐼 = (iEdg‘𝐺)
trlsegvdeg.f (𝜑 → Fun 𝐼)
trlsegvdeg.n (𝜑𝑁 ∈ (0..^(#‘𝐹)))
trlsegvdeg.u (𝜑𝑈𝑉)
trlsegvdeg.w (𝜑𝐹(TrailS‘𝐺)𝑃)
trlsegvdeg.vx (𝜑 → (Vtx‘𝑋) = 𝑉)
trlsegvdeg.vy (𝜑 → (Vtx‘𝑌) = 𝑉)
trlsegvdeg.vz (𝜑 → (Vtx‘𝑍) = 𝑉)
trlsegvdeg.ix (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
trlsegvdeg.iy (𝜑 → (iEdg‘𝑌) = {⟨(𝐹𝑁), (𝐼‘(𝐹𝑁))⟩})
trlsegvdeg.iz (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))
eupth2lem3.o (𝜑 → {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}))
eupth2lem3lem3.e (𝜑 → if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
eupth2lem3lem4.i (𝜑 → (𝐼‘(𝐹𝑁)) ∈ 𝒫 𝑉)
Assertion
Ref Expression
eupth2lem3lem4 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
Distinct variable groups:   𝑥,𝑈   𝑥,𝑉   𝑥,𝑋
Allowed substitution hints:   𝜑(𝑥)   𝑃(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝐼(𝑥)   𝑁(𝑥)   𝑌(𝑥)   𝑍(𝑥)

Proof of Theorem eupth2lem3lem4
StepHypRef Expression
1 fvex 6098 . . . . . . . . . . . 12 (𝐹𝑁) ∈ V
21a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝐹𝑁) ∈ V)
3 trlsegvdeg.u . . . . . . . . . . . 12 (𝜑𝑈𝑉)
43ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈𝑉)
5 trlsegvdeg.v . . . . . . . . . . . . . 14 𝑉 = (Vtx‘𝐺)
6 trlsegvdeg.i . . . . . . . . . . . . . 14 𝐼 = (iEdg‘𝐺)
7 trlsegvdeg.f . . . . . . . . . . . . . 14 (𝜑 → Fun 𝐼)
8 trlsegvdeg.n . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (0..^(#‘𝐹)))
9 trlsegvdeg.w . . . . . . . . . . . . . 14 (𝜑𝐹(TrailS‘𝐺)𝑃)
105, 6, 7, 8, 3, 9trlsegvdeglem1 41383 . . . . . . . . . . . . 13 (𝜑 → ((𝑃𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉))
1110simprd 477 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
1211ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
13 neeq1 2843 . . . . . . . . . . . . . 14 ((𝑃𝑁) = 𝑈 → ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1))))
1413biimpcd 237 . . . . . . . . . . . . 13 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) → ((𝑃𝑁) = 𝑈𝑈 ≠ (𝑃‘(𝑁 + 1))))
1514adantl 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃𝑁) = 𝑈𝑈 ≠ (𝑃‘(𝑁 + 1))))
1615imp 443 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈 ≠ (𝑃‘(𝑁 + 1)))
17 eupth2lem3lem4.i . . . . . . . . . . . 12 (𝜑 → (𝐼‘(𝐹𝑁)) ∈ 𝒫 𝑉)
1817ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝐼‘(𝐹𝑁)) ∈ 𝒫 𝑉)
19 trlsegvdeg.iy . . . . . . . . . . . 12 (𝜑 → (iEdg‘𝑌) = {⟨(𝐹𝑁), (𝐼‘(𝐹𝑁))⟩})
2019ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (iEdg‘𝑌) = {⟨(𝐹𝑁), (𝐼‘(𝐹𝑁))⟩})
21 eupth2lem3lem3.e . . . . . . . . . . . . . 14 (𝜑 → if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
2221adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
23 df-ne 2781 . . . . . . . . . . . . . . . 16 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ ¬ (𝑃𝑁) = (𝑃‘(𝑁 + 1)))
24 ifpfal 1017 . . . . . . . . . . . . . . . 16 (¬ (𝑃𝑁) = (𝑃‘(𝑁 + 1)) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) ↔ {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
2523, 24sylbi 205 . . . . . . . . . . . . . . 15 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) ↔ {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
2625adantl 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) ↔ {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
27 preq1 4211 . . . . . . . . . . . . . . . 16 ((𝑃𝑁) = 𝑈 → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, (𝑃‘(𝑁 + 1))})
2827sseq1d 3594 . . . . . . . . . . . . . . 15 ((𝑃𝑁) = 𝑈 → ({(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)) ↔ {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
2928biimpcd 237 . . . . . . . . . . . . . 14 ({(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)) → ((𝑃𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
3026, 29syl6bi 241 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) → ((𝑃𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)))))
3122, 30mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
3231imp 443 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)))
33 trlsegvdeg.vy . . . . . . . . . . . 12 (𝜑 → (Vtx‘𝑌) = 𝑉)
3433ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (Vtx‘𝑌) = 𝑉)
352, 4, 12, 16, 18, 20, 32, 341hegrvtxdg1 40718 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1)
3635oveq2d 6543 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1))
3736breq2d 4589 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
3837notbid 306 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
39 trlsegvdeg.vx . . . . . . . . . . . . . . 15 (𝜑 → (Vtx‘𝑋) = 𝑉)
40 trlsegvdeg.vz . . . . . . . . . . . . . . 15 (𝜑 → (Vtx‘𝑍) = 𝑉)
41 trlsegvdeg.ix . . . . . . . . . . . . . . 15 (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
42 trlsegvdeg.iz . . . . . . . . . . . . . . 15 (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))
435, 6, 7, 8, 3, 9, 39, 33, 40, 41, 19, 42eupth2lem3lem1 41391 . . . . . . . . . . . . . 14 (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ0)
4443nn0zd 11312 . . . . . . . . . . . . 13 (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ)
45 2nn 11032 . . . . . . . . . . . . . 14 2 ∈ ℕ
4645a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℕ)
47 1lt2 11041 . . . . . . . . . . . . . 14 1 < 2
4847a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 < 2)
49 ndvdsp1 14919 . . . . . . . . . . . . 13 ((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
5044, 46, 48, 49syl3anc 1317 . . . . . . . . . . . 12 (𝜑 → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
5150con2d 127 . . . . . . . . . . 11 (𝜑 → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) → ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
52 1z 11240 . . . . . . . . . . . . . 14 1 ∈ ℤ
53 n2dvds1 14888 . . . . . . . . . . . . . 14 ¬ 2 ∥ 1
54 opoe 14871 . . . . . . . . . . . . . 14 (((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))
5552, 53, 54mpanr12 716 . . . . . . . . . . . . 13 ((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))
5655ex 448 . . . . . . . . . . . 12 (((VtxDeg‘𝑋)‘𝑈) ∈ ℤ → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
5744, 56syl 17 . . . . . . . . . . 11 (𝜑 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
5851, 57impbid 200 . . . . . . . . . 10 (𝜑 → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
59 fveq2 6088 . . . . . . . . . . . . . 14 (𝑥 = 𝑈 → ((VtxDeg‘𝑋)‘𝑥) = ((VtxDeg‘𝑋)‘𝑈))
6059breq2d 4589 . . . . . . . . . . . . 13 (𝑥 = 𝑈 → (2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
6160notbid 306 . . . . . . . . . . . 12 (𝑥 = 𝑈 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
6261elrab3 3331 . . . . . . . . . . 11 (𝑈𝑉 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
633, 62syl 17 . . . . . . . . . 10 (𝜑 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
64 eupth2lem3.o . . . . . . . . . . 11 (𝜑 → {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}))
6564eleq2d 2672 . . . . . . . . . 10 (𝜑 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
6658, 63, 653bitr2d 294 . . . . . . . . 9 (𝜑 → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
6766notbid 306 . . . . . . . 8 (𝜑 → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
6867ad2antrr 757 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
69 fvex 6098 . . . . . . . . 9 (𝑃𝑁) ∈ V
7069eupath2lem2 26271 . . . . . . . 8 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
7170adantll 745 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
7238, 68, 713bitrd 292 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
7372expcom 449 . . . . 5 ((𝑃𝑁) = 𝑈 → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
7473eqcoms 2617 . . . 4 (𝑈 = (𝑃𝑁) → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
751a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐹𝑁) ∈ V)
7610simpld 473 . . . . . . . . . . . 12 (𝜑 → (𝑃𝑁) ∈ 𝑉)
7776ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ∈ 𝑉)
783ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑈𝑉)
79 neeq2 2844 . . . . . . . . . . . . . 14 ((𝑃‘(𝑁 + 1)) = 𝑈 → ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃𝑁) ≠ 𝑈))
8079biimpcd 237 . . . . . . . . . . . . 13 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) → ((𝑃‘(𝑁 + 1)) = 𝑈 → (𝑃𝑁) ≠ 𝑈))
8180adantl 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → (𝑃𝑁) ≠ 𝑈))
8281imp 443 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ≠ 𝑈)
8317ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐼‘(𝐹𝑁)) ∈ 𝒫 𝑉)
8419ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (iEdg‘𝑌) = {⟨(𝐹𝑁), (𝐼‘(𝐹𝑁))⟩})
85 preq2 4212 . . . . . . . . . . . . . . . 16 ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {(𝑃𝑁), 𝑈})
8685sseq1d 3594 . . . . . . . . . . . . . . 15 ((𝑃‘(𝑁 + 1)) = 𝑈 → ({(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)) ↔ {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁))))
8786biimpcd 237 . . . . . . . . . . . . . 14 ({(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁))))
8826, 87syl6bi 241 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁)))))
8922, 88mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁))))
9089imp 443 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁)))
9133ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (Vtx‘𝑌) = 𝑉)
9275, 77, 78, 82, 83, 84, 90, 911hegrvtxdg1r 40719 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1)
9392oveq2d 6543 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1))
9493breq2d 4589 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
9594notbid 306 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
9667ad2antrr 757 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
97 necom 2834 . . . . . . . . . 10 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘(𝑁 + 1)) ≠ (𝑃𝑁))
98 fvex 6098 . . . . . . . . . . 11 (𝑃‘(𝑁 + 1)) ∈ V
9998eupath2lem2 26271 . . . . . . . . . 10 (((𝑃‘(𝑁 + 1)) ≠ (𝑃𝑁) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
10097, 99sylanb 487 . . . . . . . . 9 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
101100con1bid 343 . . . . . . . 8 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
102101adantll 745 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
10395, 96, 1023bitrd 292 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
104103expcom 449 . . . . 5 ((𝑃‘(𝑁 + 1)) = 𝑈 → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
105104eqcoms 2617 . . . 4 (𝑈 = (𝑃‘(𝑁 + 1)) → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
10674, 105jaoi 392 . . 3 ((𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1))) → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
107106com12 32 . 2 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
1081073impia 1252 1 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  if-wif 1005  w3a 1030   = wceq 1474  wcel 1976  wne 2779  {crab 2899  Vcvv 3172  wss 3539  c0 3873  ifcif 4035  𝒫 cpw 4107  {csn 4124  {cpr 4126  cop 4130   class class class wbr 4577  cres 5030  cima 5031  Fun wfun 5784  cfv 5790  (class class class)co 6527  0cc0 9792  1c1 9793   + caddc 9795   < clt 9930  cn 10867  2c2 10917  cz 11210  ...cfz 12152  ..^cfzo 12289  #chash 12934  cdvds 14767  Vtxcvtx 40224  iEdgciedg 40225  VtxDegcvtxdg 40676  TrailSctrls 40894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ifp 1006  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-sup 8208  df-inf 8209  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-n0 11140  df-z 11211  df-uz 11520  df-rp 11665  df-xadd 11779  df-fz 12153  df-fzo 12290  df-seq 12619  df-exp 12678  df-hash 12935  df-word 13100  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-dvds 14768  df-xnn0 40193  df-vtxdg 40677  df-1wlks 40795  df-trls 40896
This theorem is referenced by:  eupth2lem3lem7  41397
  Copyright terms: Public domain W3C validator