Proof of Theorem eupth2lem3lem4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fvexd 6921 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝐹‘𝑁) ∈ V) | 
| 2 |  | trlsegvdeg.u | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ 𝑉) | 
| 3 | 2 | ad2antrr 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‘𝐺)𝑃) | 
| 9 | 4, 5, 6, 7, 2, 8 | trlsegvdeglem1 30239 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉)) | 
| 10 | 9 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘(𝑁 + 1)) ∈ 𝑉) | 
| 11 | 10 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉) | 
| 12 |  | neeq1 3003 | . . . . . . . . . . . . . 14
⊢ ((𝑃‘𝑁) = 𝑈 → ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1)))) | 
| 13 | 12 | biimpcd 249 | . . . . . . . . . . . . 13
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) → ((𝑃‘𝑁) = 𝑈 → 𝑈 ≠ (𝑃‘(𝑁 + 1)))) | 
| 14 | 13 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘𝑁) = 𝑈 → 𝑈 ≠ (𝑃‘(𝑁 + 1)))) | 
| 15 | 14 | imp 406 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → 𝑈 ≠ (𝑃‘(𝑁 + 1))) | 
| 16 |  | eupth2lem3lem4.i | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉) | 
| 17 | 16 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉) | 
| 18 |  | trlsegvdeg.iy | . . . . . . . . . . . 12
⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) | 
| 19 | 18 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) | 
| 20 |  | eupth2lem3lem3.e | . . . . . . . . . . . . . 14
⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 22 |  | df-ne 2941 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ ¬ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) | 
| 23 |  | ifpfal 1076 | . . . . . . . . . . . . . . . 16
⊢ (¬
(𝑃‘𝑁) = (𝑃‘(𝑁 + 1)) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 24 | 22, 23 | sylbi 217 | . . . . . . . . . . . . . . 15
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 25 | 24 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 26 |  | preq1 4733 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃‘𝑁) = 𝑈 → {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, (𝑃‘(𝑁 + 1))}) | 
| 27 | 26 | sseq1d 4015 | . . . . . . . . . . . . . . 15
⊢ ((𝑃‘𝑁) = 𝑈 → ({(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)) ↔ {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 28 | 27 | biimpcd 249 | . . . . . . . . . . . . . 14
⊢ ({(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)) → ((𝑃‘𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 29 | 25, 28 | biimtrdi 253 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) → ((𝑃‘𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))))) | 
| 30 | 21, 29 | mpd 15 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 31 | 30 | imp 406 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) | 
| 32 |  | trlsegvdeg.vy | . . . . . . . . . . . 12
⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) | 
| 33 | 32 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (Vtx‘𝑌) = 𝑉) | 
| 34 | 1, 3, 11, 15, 17, 19, 31, 33 | 1hegrvtxdg1 29525 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1) | 
| 35 | 34 | oveq2d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1)) | 
| 36 | 35 | breq2d 5155 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))) | 
| 37 | 36 | notbid 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...𝑁)))) | 
| 42 | 4, 5, 6, 7, 2, 8, 38, 32, 39, 40, 18, 41 | eupth2lem3lem1 30247 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈
ℕ0) | 
| 43 | 42 | nn0zd 12639 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ) | 
| 44 |  | 2nn 12339 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ | 
| 45 | 44 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℕ) | 
| 46 |  | 1lt2 12437 | . . . . . . . . . . . . . 14
⊢ 1 <
2 | 
| 47 | 46 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 < 2) | 
| 48 |  | ndvdsp1 16448 | . . . . . . . . . . . . 13
⊢
((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ 2 ∈ ℕ
∧ 1 < 2) → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1))) | 
| 49 | 43, 45, 47, 48 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (𝜑 → (2 ∥
((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1))) | 
| 50 | 49 | con2d 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)) | 
| 54 | 51, 52, 53 | mpanr12 705 | . . . . . . . . . . . . 13
⊢
((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈)) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)) | 
| 55 | 54 | ex 412 | . . . . . . . . . . . 12
⊢
(((VtxDeg‘𝑋)‘𝑈) ∈ ℤ → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))) | 
| 56 | 43, 55 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))) | 
| 57 | 50, 56 | impbid 212 | . . . . . . . . . 10
⊢ (𝜑 → (2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈))) | 
| 58 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑈 → ((VtxDeg‘𝑋)‘𝑥) = ((VtxDeg‘𝑋)‘𝑈)) | 
| 59 | 58 | breq2d 5155 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑈 → (2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝑋)‘𝑈))) | 
| 60 | 59 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑈 → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈))) | 
| 61 | 60 | elrab3 3693 | . . . . . . . . . . 11
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈))) | 
| 62 | 2, 61 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈))) | 
| 63 |  | eupth2lem3.o | . . . . . . . . . . 11
⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) | 
| 64 | 63 | eleq2d 2827 | . . . . . . . . . 10
⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) | 
| 65 | 57, 62, 64 | 3bitr2d 307 | . . . . . . . . 9
⊢ (𝜑 → (2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) | 
| 66 | 65 | notbid 318 | . . . . . . . 8
⊢ (𝜑 → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) | 
| 67 | 66 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) | 
| 68 |  | fvex 6919 | . . . . . . . . 9
⊢ (𝑃‘𝑁) ∈ V | 
| 69 | 68 | eupth2lem2 30238 | . . . . . . . 8
⊢ (((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | 
| 70 | 69 | adantll 714 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | 
| 71 | 37, 67, 70 | 3bitrd 305 | . . . . . 6
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | 
| 72 | 71 | expcom 413 | . . . . 5
⊢ ((𝑃‘𝑁) = 𝑈 → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) | 
| 73 | 72 | eqcoms 2745 | . . . 4
⊢ (𝑈 = (𝑃‘𝑁) → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) | 
| 74 |  | fvexd 6921 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐹‘𝑁) ∈ V) | 
| 75 | 9 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘𝑁) ∈ 𝑉) | 
| 76 | 75 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘𝑁) ∈ 𝑉) | 
| 77 | 2 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑈 ∈ 𝑉) | 
| 78 |  | neeq2 3004 | . . . . . . . . . . . . . 14
⊢ ((𝑃‘(𝑁 + 1)) = 𝑈 → ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘𝑁) ≠ 𝑈)) | 
| 79 | 78 | biimpcd 249 | . . . . . . . . . . . . 13
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) → ((𝑃‘(𝑁 + 1)) = 𝑈 → (𝑃‘𝑁) ≠ 𝑈)) | 
| 80 | 79 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → (𝑃‘𝑁) ≠ 𝑈)) | 
| 81 | 80 | imp 406 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘𝑁) ≠ 𝑈) | 
| 82 | 16 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉) | 
| 83 | 18 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) | 
| 84 |  | preq2 4734 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} = {(𝑃‘𝑁), 𝑈}) | 
| 85 | 84 | sseq1d 4015 | . . . . . . . . . . . . . . 15
⊢ ((𝑃‘(𝑁 + 1)) = 𝑈 → ({(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)) ↔ {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 86 | 85 | biimpcd 249 | . . . . . . . . . . . . . 14
⊢ ({(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 87 | 25, 86 | biimtrdi 253 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁))))) | 
| 88 | 21, 87 | mpd 15 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁)))) | 
| 89 | 88 | imp 406 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁))) | 
| 90 | 32 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (Vtx‘𝑌) = 𝑉) | 
| 91 | 74, 76, 77, 81, 82, 83, 89, 90 | 1hegrvtxdg1r 29526 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1) | 
| 92 | 91 | oveq2d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1)) | 
| 93 | 92 | breq2d 5155 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))) | 
| 94 | 93 | notbid 318 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ ¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1))) | 
| 95 | 66 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) | 
| 96 |  | necom 2994 | . . . . . . . . . 10
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘(𝑁 + 1)) ≠ (𝑃‘𝑁)) | 
| 97 |  | fvex 6919 | . . . . . . . . . . 11
⊢ (𝑃‘(𝑁 + 1)) ∈ V | 
| 98 | 97 | eupth2lem2 30238 | . . . . . . . . . 10
⊢ (((𝑃‘(𝑁 + 1)) ≠ (𝑃‘𝑁) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) | 
| 99 | 96, 98 | sylanb 581 | . . . . . . . . 9
⊢ (((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) | 
| 100 | 99 | con1bid 355 | . . . . . . . 8
⊢ (((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | 
| 101 | 100 | adantll 714 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | 
| 102 | 94, 95, 101 | 3bitrd 305 | . . . . . 6
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | 
| 103 | 102 | expcom 413 | . . . . 5
⊢ ((𝑃‘(𝑁 + 1)) = 𝑈 → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) | 
| 104 | 103 | eqcoms 2745 | . . . 4
⊢ (𝑈 = (𝑃‘(𝑁 + 1)) → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) | 
| 105 | 73, 104 | jaoi 858 | . . 3
⊢ ((𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1))) → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) | 
| 106 | 105 | com12 32 | . 2
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) | 
| 107 | 106 | 3impia 1118 | 1
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |