MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eupth2lem3lem4 Structured version   Visualization version   GIF version

Theorem eupth2lem3lem4 30250
Description: Lemma for eupth2lem3 30255, formerly part of proof of eupth2lem3 30255: 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 fvexd 6921 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝐹𝑁) ∈ V)
2 trlsegvdeg.u . . . . . . . . . . . 12 (𝜑𝑈𝑉)
32ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈𝑉)
4 trlsegvdeg.v . . . . . . . . . . . . . 14 𝑉 = (Vtx‘𝐺)
5 trlsegvdeg.i . . . . . . . . . . . . . 14 𝐼 = (iEdg‘𝐺)
6 trlsegvdeg.f . . . . . . . . . . . . . 14 (𝜑 → Fun 𝐼)
7 trlsegvdeg.n . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (0..^(♯‘𝐹)))
8 trlsegvdeg.w . . . . . . . . . . . . . 14 (𝜑𝐹(Trails‘𝐺)𝑃)
94, 5, 6, 7, 2, 8trlsegvdeglem1 30239 . . . . . . . . . . . . 13 (𝜑 → ((𝑃𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉))
109simprd 495 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
1110ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
12 neeq1 3003 . . . . . . . . . . . . . 14 ((𝑃𝑁) = 𝑈 → ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1))))
1312biimpcd 249 . . . . . . . . . . . . 13 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) → ((𝑃𝑁) = 𝑈𝑈 ≠ (𝑃‘(𝑁 + 1))))
1413adantl 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃𝑁) = 𝑈𝑈 ≠ (𝑃‘(𝑁 + 1))))
1514imp 406 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈 ≠ (𝑃‘(𝑁 + 1)))
16 eupth2lem3lem4.i . . . . . . . . . . . 12 (𝜑 → (𝐼‘(𝐹𝑁)) ∈ 𝒫 𝑉)
1716ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝐼‘(𝐹𝑁)) ∈ 𝒫 𝑉)
18 trlsegvdeg.iy . . . . . . . . . . . 12 (𝜑 → (iEdg‘𝑌) = {⟨(𝐹𝑁), (𝐼‘(𝐹𝑁))⟩})
1918ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (iEdg‘𝑌) = {⟨(𝐹𝑁), (𝐼‘(𝐹𝑁))⟩})
20 eupth2lem3lem3.e . . . . . . . . . . . . . 14 (𝜑 → if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
2120adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
22 df-ne 2941 . . . . . . . . . . . . . . . 16 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ ¬ (𝑃𝑁) = (𝑃‘(𝑁 + 1)))
23 ifpfal 1076 . . . . . . . . . . . . . . . 16 (¬ (𝑃𝑁) = (𝑃‘(𝑁 + 1)) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) ↔ {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
2422, 23sylbi 217 . . . . . . . . . . . . . . 15 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) ↔ {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
2524adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) ↔ {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
26 preq1 4733 . . . . . . . . . . . . . . . 16 ((𝑃𝑁) = 𝑈 → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, (𝑃‘(𝑁 + 1))})
2726sseq1d 4015 . . . . . . . . . . . . . . 15 ((𝑃𝑁) = 𝑈 → ({(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)) ↔ {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
2827biimpcd 249 . . . . . . . . . . . . . 14 ({(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)) → ((𝑃𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
2925, 28biimtrdi 253 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) → ((𝑃𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)))))
3021, 29mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))))
3130imp 406 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)))
32 trlsegvdeg.vy . . . . . . . . . . . 12 (𝜑 → (Vtx‘𝑌) = 𝑉)
3332ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (Vtx‘𝑌) = 𝑉)
341, 3, 11, 15, 17, 19, 31, 331hegrvtxdg1 29525 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1)
3534oveq2d 7447 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1))
3635breq2d 5155 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
3736notbid 318 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
38 trlsegvdeg.vx . . . . . . . . . . . . . . 15 (𝜑 → (Vtx‘𝑋) = 𝑉)
39 trlsegvdeg.vz . . . . . . . . . . . . . . 15 (𝜑 → (Vtx‘𝑍) = 𝑉)
40 trlsegvdeg.ix . . . . . . . . . . . . . . 15 (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
41 trlsegvdeg.iz . . . . . . . . . . . . . . 15 (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))
424, 5, 6, 7, 2, 8, 38, 32, 39, 40, 18, 41eupth2lem3lem1 30247 . . . . . . . . . . . . . 14 (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ0)
4342nn0zd 12639 . . . . . . . . . . . . 13 (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ)
44 2nn 12339 . . . . . . . . . . . . . 14 2 ∈ ℕ
4544a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℕ)
46 1lt2 12437 . . . . . . . . . . . . . 14 1 < 2
4746a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 < 2)
48 ndvdsp1 16448 . . . . . . . . . . . . 13 ((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
4943, 45, 47, 48syl3anc 1373 . . . . . . . . . . . 12 (𝜑 → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
5049con2d 134 . . . . . . . . . . 11 (𝜑 → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) → ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
51 1z 12647 . . . . . . . . . . . . . 14 1 ∈ ℤ
52 n2dvds1 16405 . . . . . . . . . . . . . 14 ¬ 2 ∥ 1
53 opoe 16400 . . . . . . . . . . . . . 14 (((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))
5451, 52, 53mpanr12 705 . . . . . . . . . . . . 13 ((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))
5554ex 412 . . . . . . . . . . . 12 (((VtxDeg‘𝑋)‘𝑈) ∈ ℤ → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
5643, 55syl 17 . . . . . . . . . . 11 (𝜑 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
5750, 56impbid 212 . . . . . . . . . 10 (𝜑 → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
58 fveq2 6906 . . . . . . . . . . . . . 14 (𝑥 = 𝑈 → ((VtxDeg‘𝑋)‘𝑥) = ((VtxDeg‘𝑋)‘𝑈))
5958breq2d 5155 . . . . . . . . . . . . 13 (𝑥 = 𝑈 → (2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
6059notbid 318 . . . . . . . . . . . 12 (𝑥 = 𝑈 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
6160elrab3 3693 . . . . . . . . . . 11 (𝑈𝑉 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
622, 61syl 17 . . . . . . . . . 10 (𝜑 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
63 eupth2lem3.o . . . . . . . . . . 11 (𝜑 → {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}))
6463eleq2d 2827 . . . . . . . . . 10 (𝜑 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
6557, 62, 643bitr2d 307 . . . . . . . . 9 (𝜑 → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
6665notbid 318 . . . . . . . 8 (𝜑 → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
6766ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
68 fvex 6919 . . . . . . . . 9 (𝑃𝑁) ∈ V
6968eupth2lem2 30238 . . . . . . . 8 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
7069adantll 714 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
7137, 67, 703bitrd 305 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
7271expcom 413 . . . . 5 ((𝑃𝑁) = 𝑈 → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
7372eqcoms 2745 . . . 4 (𝑈 = (𝑃𝑁) → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
74 fvexd 6921 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐹𝑁) ∈ V)
759simpld 494 . . . . . . . . . . . 12 (𝜑 → (𝑃𝑁) ∈ 𝑉)
7675ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ∈ 𝑉)
772ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑈𝑉)
78 neeq2 3004 . . . . . . . . . . . . . 14 ((𝑃‘(𝑁 + 1)) = 𝑈 → ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃𝑁) ≠ 𝑈))
7978biimpcd 249 . . . . . . . . . . . . 13 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) → ((𝑃‘(𝑁 + 1)) = 𝑈 → (𝑃𝑁) ≠ 𝑈))
8079adantl 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → (𝑃𝑁) ≠ 𝑈))
8180imp 406 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ≠ 𝑈)
8216ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐼‘(𝐹𝑁)) ∈ 𝒫 𝑉)
8318ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (iEdg‘𝑌) = {⟨(𝐹𝑁), (𝐼‘(𝐹𝑁))⟩})
84 preq2 4734 . . . . . . . . . . . . . . . 16 ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {(𝑃𝑁), 𝑈})
8584sseq1d 4015 . . . . . . . . . . . . . . 15 ((𝑃‘(𝑁 + 1)) = 𝑈 → ({(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)) ↔ {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁))))
8685biimpcd 249 . . . . . . . . . . . . . 14 ({(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁)) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁))))
8725, 86biimtrdi 253 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹𝑁)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹𝑁))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁)))))
8821, 87mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁))))
8988imp 406 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {(𝑃𝑁), 𝑈} ⊆ (𝐼‘(𝐹𝑁)))
9032ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (Vtx‘𝑌) = 𝑉)
9174, 76, 77, 81, 82, 83, 89, 901hegrvtxdg1r 29526 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1)
9291oveq2d 7447 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1))
9392breq2d 5155 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
9493notbid 318 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
9566ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
96 necom 2994 . . . . . . . . . 10 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘(𝑁 + 1)) ≠ (𝑃𝑁))
97 fvex 6919 . . . . . . . . . . 11 (𝑃‘(𝑁 + 1)) ∈ V
9897eupth2lem2 30238 . . . . . . . . . 10 (((𝑃‘(𝑁 + 1)) ≠ (𝑃𝑁) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
9996, 98sylanb 581 . . . . . . . . 9 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
10099con1bid 355 . . . . . . . 8 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
101100adantll 714 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
10294, 95, 1013bitrd 305 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
103102expcom 413 . . . . 5 ((𝑃‘(𝑁 + 1)) = 𝑈 → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
104103eqcoms 2745 . . . 4 (𝑈 = (𝑃‘(𝑁 + 1)) → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
10573, 104jaoi 858 . . 3 ((𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1))) → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
106105com12 32 . 2 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
1071063impia 1118 1 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  if-wif 1063  w3a 1087   = wceq 1540  wcel 2108  wne 2940  {crab 3436  Vcvv 3480  wss 3951  c0 4333  ifcif 4525  𝒫 cpw 4600  {csn 4626  {cpr 4628  cop 4632   class class class wbr 5143  cres 5687  cima 5688  Fun wfun 6555  cfv 6561  (class class class)co 7431  0cc0 11155  1c1 11156   + caddc 11158   < clt 11295  cn 12266  2c2 12321  cz 12613  ...cfz 13547  ..^cfzo 13694  chash 14369  cdvds 16290  Vtxcvtx 29013  iEdgciedg 29014  VtxDegcvtxdg 29483  Trailsctrls 29708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ifp 1064  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-rp 13035  df-xadd 13155  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-word 14553  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-dvds 16291  df-vtxdg 29484  df-wlks 29617  df-trls 29710
This theorem is referenced by:  eupth2lem3lem7  30253
  Copyright terms: Public domain W3C validator