Step | Hyp | Ref
| Expression |
1 | | n0 3931 |
. . 3
⊢ ((𝑋(𝑁 WSPathsNOn 𝐺)𝑌) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌)) |
2 | | eqid 2622 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | 2 | wspthnonp 26744 |
. . . . 5
⊢ (𝑝 ∈ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) → ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺)) ∧ (𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) ∧ ∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝))) |
4 | 2 | wwlknon 26742 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺)) → (𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) ↔ (𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘𝑁) = 𝑌))) |
5 | 4 | adantl 482 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → (𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) ↔ (𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘𝑁) = 𝑌))) |
6 | | iswwlksn 26730 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑝 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑝 ∈ (WWalks‘𝐺) ∧ (#‘𝑝) = (𝑁 + 1)))) |
7 | | spthonisspth 26646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → 𝑓(SPaths‘𝐺)𝑝) |
8 | | spthispth 26622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑓(Paths‘𝐺)𝑝) |
9 | | pthiswlk 26623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(Paths‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝) |
10 | | wlklenvm1 26517 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(Walks‘𝐺)𝑝 → (#‘𝑓) = ((#‘𝑝) − 1)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(Paths‘𝐺)𝑝 → (#‘𝑓) = ((#‘𝑝) − 1)) |
12 | 7, 8, 11 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (#‘𝑓) = ((#‘𝑝) − 1)) |
13 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) =
(𝑁 + 1) →
((#‘𝑝) − 1) =
((𝑁 + 1) −
1)) |
14 | 13 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑝) =
(𝑁 + 1) →
((#‘𝑓) =
((#‘𝑝) − 1)
↔ (#‘𝑓) =
((𝑁 + 1) −
1))) |
15 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑓) = ((𝑁 + 1) − 1)) →
(#‘𝑓) = ((𝑁 + 1) −
1)) |
16 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
17 | | pncan1 10454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑓) = ((𝑁 + 1) − 1)) → ((𝑁 + 1) − 1) = 𝑁) |
20 | 15, 19 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑓) = ((𝑁 + 1) − 1)) →
(#‘𝑓) = 𝑁) |
21 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑓) = ((𝑁 + 1) − 1)) → 𝑁 ≠ 0) |
23 | 20, 22 | eqnetrd 2861 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑓) = ((𝑁 + 1) − 1)) →
(#‘𝑓) ≠
0) |
24 | | spthonepeq 26648 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑋 = 𝑌 ↔ (#‘𝑓) = 0)) |
25 | 24 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑋 ≠ 𝑌 ↔ (#‘𝑓) ≠ 0)) |
26 | 23, 25 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑓) = ((𝑁 + 1) − 1)) → (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → 𝑋 ≠ 𝑌)) |
27 | 26 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑓) =
((𝑁 + 1) − 1) →
(𝑁 ∈ ℕ →
(𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → 𝑋 ≠ 𝑌))) |
28 | 27 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑓) =
((𝑁 + 1) − 1) →
(𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
29 | 14, 28 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑝) =
(𝑁 + 1) →
((#‘𝑓) =
((#‘𝑝) − 1)
→ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
30 | 29 | com13 88 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → ((#‘𝑓) = ((#‘𝑝) − 1) → ((#‘𝑝) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
31 | 12, 30 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → ((#‘𝑝) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
32 | 31 | exlimiv 1858 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → ((#‘𝑝) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
33 | 32 | com12 32 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑝) =
(𝑁 + 1) →
(∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
34 | 33 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ (WWalks‘𝐺) ∧ (#‘𝑝) = (𝑁 + 1)) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
35 | 6, 34 | syl6bi 243 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑝 ∈ (𝑁 WWalksN 𝐺) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
36 | 35 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
(𝑝 ∈ (𝑁 WWalksN 𝐺) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
37 | 36 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → (𝑝 ∈ (𝑁 WWalksN 𝐺) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
38 | 37 | com12 32 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (𝑁 WWalksN 𝐺) → (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
39 | 38 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘𝑁) = 𝑌) → (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
40 | 39 | com12 32 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → ((𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘𝑁) = 𝑌) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
41 | 5, 40 | sylbid 230 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → (𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
42 | 41 | impd 447 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → ((𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) ∧ ∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
43 | 42 | 3impia 1261 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺)) ∧ (𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) ∧ ∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝)) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)) |
44 | 3, 43 | syl 17 |
. . . 4
⊢ (𝑝 ∈ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)) |
45 | 44 | exlimiv 1858 |
. . 3
⊢
(∃𝑝 𝑝 ∈ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)) |
46 | 1, 45 | sylbi 207 |
. 2
⊢ ((𝑋(𝑁 WSPathsNOn 𝐺)𝑌) ≠ ∅ → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)) |
47 | 46 | impcom 446 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) ≠ ∅) → 𝑋 ≠ 𝑌) |