| Step | Hyp | Ref
| Expression |
| 1 | | n0 4353 |
. . 3
⊢ ((𝑋(𝑁 WSPathsNOn 𝐺)𝑌) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌)) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 3 | 2 | wspthnonp 29879 |
. . . . 5
⊢ (𝑝 ∈ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) → ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺)) ∧ (𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) ∧ ∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝))) |
| 4 | | wwlknon 29877 |
. . . . . . . 8
⊢ (𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) ↔ (𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘𝑁) = 𝑌)) |
| 5 | | iswwlksn 29858 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑝 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑝 ∈ (WWalks‘𝐺) ∧ (♯‘𝑝) = (𝑁 + 1)))) |
| 6 | | spthonisspth 29770 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → 𝑓(SPaths‘𝐺)𝑝) |
| 7 | | spthispth 29744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑓(Paths‘𝐺)𝑝) |
| 8 | | pthiswlk 29745 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(Paths‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝) |
| 9 | | wlklenvm1 29640 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑓) = ((♯‘𝑝) − 1)) |
| 10 | 6, 7, 8, 9 | 4syl 19 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (♯‘𝑓) = ((♯‘𝑝) − 1)) |
| 11 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑝) =
(𝑁 + 1) →
((♯‘𝑝) −
1) = ((𝑁 + 1) −
1)) |
| 12 | 11 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑝) =
(𝑁 + 1) →
((♯‘𝑓) =
((♯‘𝑝) −
1) ↔ (♯‘𝑓)
= ((𝑁 + 1) −
1))) |
| 13 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧
(♯‘𝑓) = ((𝑁 + 1) − 1)) →
(♯‘𝑓) = ((𝑁 + 1) −
1)) |
| 14 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 15 | | pncan1 11687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧
(♯‘𝑓) = ((𝑁 + 1) − 1)) → ((𝑁 + 1) − 1) = 𝑁) |
| 18 | 13, 17 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧
(♯‘𝑓) = ((𝑁 + 1) − 1)) →
(♯‘𝑓) = 𝑁) |
| 19 | | nnne0 12300 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧
(♯‘𝑓) = ((𝑁 + 1) − 1)) → 𝑁 ≠ 0) |
| 21 | 18, 20 | eqnetrd 3008 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧
(♯‘𝑓) = ((𝑁 + 1) − 1)) →
(♯‘𝑓) ≠
0) |
| 22 | | spthonepeq 29772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑋 = 𝑌 ↔ (♯‘𝑓) = 0)) |
| 23 | 22 | necon3bid 2985 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑋 ≠ 𝑌 ↔ (♯‘𝑓) ≠ 0)) |
| 24 | 21, 23 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧
(♯‘𝑓) = ((𝑁 + 1) − 1)) → (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → 𝑋 ≠ 𝑌)) |
| 25 | 24 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑓) =
((𝑁 + 1) − 1) →
(𝑁 ∈ ℕ →
(𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → 𝑋 ≠ 𝑌))) |
| 26 | 25 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑓) =
((𝑁 + 1) − 1) →
(𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
| 27 | 12, 26 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑝) =
(𝑁 + 1) →
((♯‘𝑓) =
((♯‘𝑝) −
1) → (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
| 28 | 27 | com13 88 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → ((♯‘𝑓) = ((♯‘𝑝) − 1) → ((♯‘𝑝) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
| 29 | 10, 28 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → ((♯‘𝑝) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
| 30 | 29 | exlimiv 1930 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → ((♯‘𝑝) = (𝑁 + 1) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
| 31 | 30 | com12 32 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑝) =
(𝑁 + 1) →
(∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
| 32 | 31 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ (WWalks‘𝐺) ∧ (♯‘𝑝) = (𝑁 + 1)) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
| 33 | 5, 32 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑝 ∈ (𝑁 WWalksN 𝐺) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
(𝑝 ∈ (𝑁 WWalksN 𝐺) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → (𝑝 ∈ (𝑁 WWalksN 𝐺) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
| 36 | 35 | com12 32 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (𝑁 WWalksN 𝐺) → (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
| 37 | 36 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘𝑁) = 𝑌) → (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
| 38 | 37 | com12 32 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → ((𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘𝑁) = 𝑌) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
| 39 | 4, 38 | biimtrid 242 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → (𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) → (∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝 → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)))) |
| 40 | 39 | impd 410 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺))) → ((𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) ∧ ∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌))) |
| 41 | 40 | 3impia 1118 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
(𝑋 ∈ (Vtx‘𝐺) ∧ 𝑌 ∈ (Vtx‘𝐺)) ∧ (𝑝 ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑌) ∧ ∃𝑓 𝑓(𝑋(SPathsOn‘𝐺)𝑌)𝑝)) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)) |
| 42 | 3, 41 | syl 17 |
. . . 4
⊢ (𝑝 ∈ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)) |
| 43 | 42 | exlimiv 1930 |
. . 3
⊢
(∃𝑝 𝑝 ∈ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)) |
| 44 | 1, 43 | sylbi 217 |
. 2
⊢ ((𝑋(𝑁 WSPathsNOn 𝐺)𝑌) ≠ ∅ → (𝑁 ∈ ℕ → 𝑋 ≠ 𝑌)) |
| 45 | 44 | impcom 407 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) ≠ ∅) → 𝑋 ≠ 𝑌) |