Proof of Theorem eupth2lem3lem4
Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑁) ∈ V |
2 | 1 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝐹‘𝑁) ∈ V) |
3 | | trlsegvdeg.u |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
4 | 3 | ad2antrr 758 |
. . . . . . . . . . 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‘𝐺)𝑃) |
10 | 5, 6, 7, 8, 3, 9 | trlsegvdeglem1 41388 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉)) |
11 | 10 | simprd 478 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘(𝑁 + 1)) ∈ 𝑉) |
12 | 11 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉) |
13 | | neeq1 2844 |
. . . . . . . . . . . . . 14
⊢ ((𝑃‘𝑁) = 𝑈 → ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1)))) |
14 | 13 | biimpcd 238 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) → ((𝑃‘𝑁) = 𝑈 → 𝑈 ≠ (𝑃‘(𝑁 + 1)))) |
15 | 14 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘𝑁) = 𝑈 → 𝑈 ≠ (𝑃‘(𝑁 + 1)))) |
16 | 15 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → 𝑈 ≠ (𝑃‘(𝑁 + 1))) |
17 | | eupth2lem3lem4.i |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉) |
18 | 17 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉) |
19 | | trlsegvdeg.iy |
. . . . . . . . . . . 12
⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) |
20 | 19 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) |
21 | | eupth2lem3lem3.e |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
23 | | df-ne 2782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ ¬ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) |
24 | | ifpfal 1018 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑃‘𝑁) = (𝑃‘(𝑁 + 1)) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
25 | 23, 24 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
27 | | preq1 4212 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃‘𝑁) = 𝑈 → {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, (𝑃‘(𝑁 + 1))}) |
28 | 27 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃‘𝑁) = 𝑈 → ({(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)) ↔ {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
29 | 28 | biimpcd 238 |
. . . . . . . . . . . . . 14
⊢ ({(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)) → ((𝑃‘𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
30 | 26, 29 | syl6bi 242 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) → ((𝑃‘𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))))) |
31 | 22, 30 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘𝑁) = 𝑈 → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) |
32 | 31 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → {𝑈, (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) |
33 | | trlsegvdeg.vy |
. . . . . . . . . . . 12
⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) |
34 | 33 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (Vtx‘𝑌) = 𝑉) |
35 | 2, 4, 12, 16, 18, 20, 32, 34 | 1hegrvtxdg1 40723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1) |
36 | 35 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1)) |
37 | 36 | breq2d 4595 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))) |
38 | 37 | notbid 307 |
. . . . . . 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...𝑁)))) |
43 | 5, 6, 7, 8, 3, 9, 39, 33, 40, 41, 19, 42 | eupth2lem3lem1 41396 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈
ℕ0) |
44 | 43 | nn0zd 11356 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ) |
45 | | 2nn 11062 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
46 | 45 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℕ) |
47 | | 1lt2 11071 |
. . . . . . . . . . . . . 14
⊢ 1 <
2 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < 2) |
49 | | ndvdsp1 14973 |
. . . . . . . . . . . . 13
⊢
((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ 2 ∈ ℕ
∧ 1 < 2) → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1))) |
50 | 44, 46, 48, 49 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 ∥
((VtxDeg‘𝑋)‘𝑈) → ¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1))) |
51 | 50 | con2d 128 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) → ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈))) |
52 | | 1z 11284 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
53 | | n2dvds1 14942 |
. . . . . . . . . . . . . 14
⊢ ¬ 2
∥ 1 |
54 | | opoe 14925 |
. . . . . . . . . . . . . 14
⊢
(((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈)) ∧ (1 ∈ ℤ ∧ ¬ 2
∥ 1)) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)) |
55 | 52, 53, 54 | mpanr12 717 |
. . . . . . . . . . . . 13
⊢
((((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈)) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1)) |
56 | 55 | ex 449 |
. . . . . . . . . . . 12
⊢
(((VtxDeg‘𝑋)‘𝑈) ∈ ℤ → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))) |
57 | 44, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈) → 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))) |
58 | 51, 57 | impbid 201 |
. . . . . . . . . 10
⊢ (𝜑 → (2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈))) |
59 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑈 → ((VtxDeg‘𝑋)‘𝑥) = ((VtxDeg‘𝑋)‘𝑈)) |
60 | 59 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑈 → (2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝑋)‘𝑈))) |
61 | 60 | notbid 307 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑈 → (¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈))) |
62 | 61 | elrab3 3332 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈))) |
63 | 3, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑈))) |
64 | | eupth2lem3.o |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) |
65 | 64 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥
((VtxDeg‘𝑋)‘𝑥)} ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
66 | 58, 63, 65 | 3bitr2d 295 |
. . . . . . . . 9
⊢ (𝜑 → (2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
67 | 66 | notbid 307 |
. . . . . . . 8
⊢ (𝜑 → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
68 | 67 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
69 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝑃‘𝑁) ∈ V |
70 | 69 | eupath2lem2 26505 |
. . . . . . . 8
⊢ (((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |
71 | 70 | adantll 746 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |
72 | 38, 68, 71 | 3bitrd 293 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |
73 | 72 | expcom 450 |
. . . . 5
⊢ ((𝑃‘𝑁) = 𝑈 → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) |
74 | 73 | eqcoms 2618 |
. . . 4
⊢ (𝑈 = (𝑃‘𝑁) → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) |
75 | 1 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐹‘𝑁) ∈ V) |
76 | 10 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘𝑁) ∈ 𝑉) |
77 | 76 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘𝑁) ∈ 𝑉) |
78 | 3 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑈 ∈ 𝑉) |
79 | | neeq2 2845 |
. . . . . . . . . . . . . 14
⊢ ((𝑃‘(𝑁 + 1)) = 𝑈 → ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘𝑁) ≠ 𝑈)) |
80 | 79 | biimpcd 238 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) → ((𝑃‘(𝑁 + 1)) = 𝑈 → (𝑃‘𝑁) ≠ 𝑈)) |
81 | 80 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → (𝑃‘𝑁) ≠ 𝑈)) |
82 | 81 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘𝑁) ≠ 𝑈) |
83 | 17 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉) |
84 | 19 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) |
85 | | preq2 4213 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} = {(𝑃‘𝑁), 𝑈}) |
86 | 85 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃‘(𝑁 + 1)) = 𝑈 → ({(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)) ↔ {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁)))) |
87 | 86 | biimpcd 238 |
. . . . . . . . . . . . . 14
⊢ ({(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁)))) |
88 | 26, 87 | syl6bi 242 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁))))) |
89 | 22, 88 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑃‘(𝑁 + 1)) = 𝑈 → {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁)))) |
90 | 89 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {(𝑃‘𝑁), 𝑈} ⊆ (𝐼‘(𝐹‘𝑁))) |
91 | 33 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (Vtx‘𝑌) = 𝑉) |
92 | 75, 77, 78, 82, 83, 84, 90, 91 | 1hegrvtxdg1r 40724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((VtxDeg‘𝑌)‘𝑈) = 1) |
93 | 92 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + 1)) |
94 | 93 | breq2d 4595 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + 1))) |
95 | 94 | notbid 307 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ ¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1))) |
96 | 67 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
97 | | necom 2835 |
. . . . . . . . . 10
⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘(𝑁 + 1)) ≠ (𝑃‘𝑁)) |
98 | | fvex 6113 |
. . . . . . . . . . 11
⊢ (𝑃‘(𝑁 + 1)) ∈ V |
99 | 98 | eupath2lem2 26505 |
. . . . . . . . . 10
⊢ (((𝑃‘(𝑁 + 1)) ≠ (𝑃‘𝑁) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
100 | 97, 99 | sylanb 488 |
. . . . . . . . 9
⊢ (((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))) |
101 | 100 | con1bid 344 |
. . . . . . . 8
⊢ (((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |
102 | 101 | adantll 746 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |
103 | 95, 96, 102 | 3bitrd 293 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |
104 | 103 | expcom 450 |
. . . . 5
⊢ ((𝑃‘(𝑁 + 1)) = 𝑈 → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) |
105 | 104 | eqcoms 2618 |
. . . 4
⊢ (𝑈 = (𝑃‘(𝑁 + 1)) → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) |
106 | 74, 105 | jaoi 393 |
. . 3
⊢ ((𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1))) → ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) |
107 | 106 | com12 32 |
. 2
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → ((𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))) |
108 | 107 | 3impia 1253 |
1
⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))) → (¬ 2 ∥
(((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) |