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

Theorem eupth2lem3lem4 30260
Description: Lemma for eupth2lem3 30265, formerly part of proof of eupth2lem3 30265: 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 6922 . . . . . . . . . . 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 30249 . . . . . . . . . . . . 13 (𝜑 → ((𝑃𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉))
109simprd 495 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
1110ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
12 neeq1 3001 . . . . . . . . . . . . . 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 2939 . . . . . . . . . . . . . . . 16 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ ¬ (𝑃𝑁) = (𝑃‘(𝑁 + 1)))
23 ifpfal 1075 . . . . . . . . . . . . . . . 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 4738 . . . . . . . . . . . . . . . 16 ((𝑃𝑁) = 𝑈 → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, (𝑃‘(𝑁 + 1))})
2726sseq1d 4027 . . . . . . . . . . . . . . 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 29540 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1)
3534oveq2d 7447 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1))
3635breq2d 5160 . . . . . . . 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 30257 . . . . . . . . . . . . . 14 (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ0)
4342nn0zd 12637 . . . . . . . . . . . . 13 (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ)
44 2nn 12337 . . . . . . . . . . . . . 14 2 ∈ ℕ
4544a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℕ)
46 1lt2 12435 . . . . . . . . . . . . . 14 1 < 2
4746a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 < 2)
48 ndvdsp1 16445 . . . . . . . . . . . . 13 ((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
4943, 45, 47, 48syl3anc 1370 . . . . . . . . . . . 12 (𝜑 → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)))
5049con2d 134 . . . . . . . . . . 11 (𝜑 → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1) → ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
51 1z 12645 . . . . . . . . . . . . . 14 1 ∈ ℤ
52 n2dvds1 16402 . . . . . . . . . . . . . 14 ¬ 2 ∥ 1
53 opoe 16397 . . . . . . . . . . . . . 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 6907 . . . . . . . . . . . . . 14 (𝑥 = 𝑈 → ((VtxDeg‘𝑋)‘𝑥) = ((VtxDeg‘𝑋)‘𝑈))
5958breq2d 5160 . . . . . . . . . . . . 13 (𝑥 = 𝑈 → (2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
6059notbid 318 . . . . . . . . . . . 12 (𝑥 = 𝑈 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
6160elrab3 3696 . . . . . . . . . . 11 (𝑈𝑉 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
622, 61syl 17 . . . . . . . . . 10 (𝜑 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
63 eupth2lem3.o . . . . . . . . . . 11 (𝜑 → {𝑥𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}))
6463eleq2d 2825 . . . . . . . . . 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 6920 . . . . . . . . 9 (𝑃𝑁) ∈ V
6968eupth2lem2 30248 . . . . . . . 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 2743 . . . 4 (𝑈 = (𝑃𝑁) → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
74 fvexd 6922 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐹𝑁) ∈ V)
759simpld 494 . . . . . . . . . . . 12 (𝜑 → (𝑃𝑁) ∈ 𝑉)
7675ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ∈ 𝑉)
772ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑈𝑉)
78 neeq2 3002 . . . . . . . . . . . . . 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 4739 . . . . . . . . . . . . . . . 16 ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {(𝑃𝑁), 𝑈})
8584sseq1d 4027 . . . . . . . . . . . . . . 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 29541 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1)
9291oveq2d 7447 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1))
9392breq2d 5160 . . . . . . . 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 2992 . . . . . . . . . 10 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘(𝑁 + 1)) ≠ (𝑃𝑁))
97 fvex 6920 . . . . . . . . . . 11 (𝑃‘(𝑁 + 1)) ∈ V
9897eupth2lem2 30248 . . . . . . . . . 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 2743 . . . 4 (𝑈 = (𝑃‘(𝑁 + 1)) → ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))))
10573, 104jaoi 857 . . 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 1116 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 847  if-wif 1062  w3a 1086   = wceq 1537  wcel 2106  wne 2938  {crab 3433  Vcvv 3478  wss 3963  c0 4339  ifcif 4531  𝒫 cpw 4605  {csn 4631  {cpr 4633  cop 4637   class class class wbr 5148  cres 5691  cima 5692  Fun wfun 6557  cfv 6563  (class class class)co 7431  0cc0 11153  1c1 11154   + caddc 11156   < clt 11293  cn 12264  2c2 12319  cz 12611  ...cfz 13544  ..^cfzo 13691  chash 14366  cdvds 16287  Vtxcvtx 29028  iEdgciedg 29029  VtxDegcvtxdg 29498  Trailsctrls 29723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ifp 1063  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-oadd 8509  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-sup 9480  df-inf 9481  df-dju 9939  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-xnn0 12598  df-z 12612  df-uz 12877  df-rp 13033  df-xadd 13153  df-fz 13545  df-fzo 13692  df-seq 14040  df-exp 14100  df-hash 14367  df-word 14550  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-dvds 16288  df-vtxdg 29499  df-wlks 29632  df-trls 29725
This theorem is referenced by:  eupth2lem3lem7  30263
  Copyright terms: Public domain W3C validator