Proof of Theorem umgrclwwlkge2
Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | 1 | clwwlkbp 28328 |
. . . . 5
⊢ (𝑃 ∈ (ClWWalks‘𝐺) → (𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅)) |
3 | 2 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ UMGraph ∧ 𝑃 ∈ (ClWWalks‘𝐺)) → (𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅)) |
4 | | lencl 14217 |
. . . . . . 7
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (♯‘𝑃) ∈
ℕ0) |
5 | 4 | 3ad2ant2 1132 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅) → (♯‘𝑃) ∈
ℕ0) |
6 | 5 | adantl 481 |
. . . . 5
⊢ (((𝐺 ∈ UMGraph ∧ 𝑃 ∈ (ClWWalks‘𝐺)) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅)) → (♯‘𝑃) ∈
ℕ0) |
7 | | hasheq0 14059 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → ((♯‘𝑃) = 0 ↔ 𝑃 = ∅)) |
8 | 7 | bicomd 222 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (𝑃 = ∅ ↔ (♯‘𝑃) = 0)) |
9 | 8 | necon3bid 2989 |
. . . . . . . . 9
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (𝑃 ≠ ∅ ↔ (♯‘𝑃) ≠ 0)) |
10 | 9 | biimpd 228 |
. . . . . . . 8
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (𝑃 ≠ ∅ → (♯‘𝑃) ≠ 0)) |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝐺 ∈ V → (𝑃 ∈ Word (Vtx‘𝐺) → (𝑃 ≠ ∅ → (♯‘𝑃) ≠ 0))) |
12 | 11 | 3imp 1109 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅) → (♯‘𝑃) ≠ 0) |
13 | 12 | adantl 481 |
. . . . 5
⊢ (((𝐺 ∈ UMGraph ∧ 𝑃 ∈ (ClWWalks‘𝐺)) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅)) → (♯‘𝑃) ≠ 0) |
14 | | clwwlk1loop 28331 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ClWWalks‘𝐺) ∧ (♯‘𝑃) = 1) → {(𝑃‘0), (𝑃‘0)} ∈ (Edg‘𝐺)) |
15 | 14 | expcom 413 |
. . . . . . . . 9
⊢
((♯‘𝑃) =
1 → (𝑃 ∈
(ClWWalks‘𝐺) →
{(𝑃‘0), (𝑃‘0)} ∈
(Edg‘𝐺))) |
16 | | eqid 2739 |
. . . . . . . . . . 11
⊢ (𝑃‘0) = (𝑃‘0) |
17 | | eqid 2739 |
. . . . . . . . . . . 12
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
18 | 17 | umgredgne 27496 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ {(𝑃‘0), (𝑃‘0)} ∈ (Edg‘𝐺)) → (𝑃‘0) ≠ (𝑃‘0)) |
19 | | eqneqall 2955 |
. . . . . . . . . . 11
⊢ ((𝑃‘0) = (𝑃‘0) → ((𝑃‘0) ≠ (𝑃‘0) → ((𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅) → (♯‘𝑃) ≠ 1))) |
20 | 16, 18, 19 | mpsyl 68 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ {(𝑃‘0), (𝑃‘0)} ∈ (Edg‘𝐺)) → ((𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅) → (♯‘𝑃) ≠ 1)) |
21 | 20 | expcom 413 |
. . . . . . . . 9
⊢ ({(𝑃‘0), (𝑃‘0)} ∈ (Edg‘𝐺) → (𝐺 ∈ UMGraph → ((𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅) → (♯‘𝑃) ≠ 1))) |
22 | 15, 21 | syl6 35 |
. . . . . . . 8
⊢
((♯‘𝑃) =
1 → (𝑃 ∈
(ClWWalks‘𝐺) →
(𝐺 ∈ UMGraph →
((𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅) → (♯‘𝑃) ≠ 1)))) |
23 | 22 | com23 86 |
. . . . . . 7
⊢
((♯‘𝑃) =
1 → (𝐺 ∈ UMGraph
→ (𝑃 ∈
(ClWWalks‘𝐺) →
((𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅) → (♯‘𝑃) ≠ 1)))) |
24 | 23 | imp4c 423 |
. . . . . 6
⊢
((♯‘𝑃) =
1 → (((𝐺 ∈
UMGraph ∧ 𝑃 ∈
(ClWWalks‘𝐺)) ∧
(𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅)) → (♯‘𝑃) ≠ 1)) |
25 | | neqne 2952 |
. . . . . . 7
⊢ (¬
(♯‘𝑃) = 1
→ (♯‘𝑃)
≠ 1) |
26 | 25 | a1d 25 |
. . . . . 6
⊢ (¬
(♯‘𝑃) = 1
→ (((𝐺 ∈ UMGraph
∧ 𝑃 ∈
(ClWWalks‘𝐺)) ∧
(𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅)) → (♯‘𝑃) ≠ 1)) |
27 | 24, 26 | pm2.61i 182 |
. . . . 5
⊢ (((𝐺 ∈ UMGraph ∧ 𝑃 ∈ (ClWWalks‘𝐺)) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅)) → (♯‘𝑃) ≠ 1) |
28 | 6, 13, 27 | 3jca 1126 |
. . . 4
⊢ (((𝐺 ∈ UMGraph ∧ 𝑃 ∈ (ClWWalks‘𝐺)) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑃 ≠ ∅)) → ((♯‘𝑃) ∈ ℕ0
∧ (♯‘𝑃)
≠ 0 ∧ (♯‘𝑃) ≠ 1)) |
29 | 3, 28 | mpdan 683 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ 𝑃 ∈ (ClWWalks‘𝐺)) → ((♯‘𝑃) ∈ ℕ0
∧ (♯‘𝑃)
≠ 0 ∧ (♯‘𝑃) ≠ 1)) |
30 | | nn0n0n1ge2 12283 |
. . 3
⊢
(((♯‘𝑃)
∈ ℕ0 ∧ (♯‘𝑃) ≠ 0 ∧ (♯‘𝑃) ≠ 1) → 2 ≤
(♯‘𝑃)) |
31 | 29, 30 | syl 17 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ 𝑃 ∈ (ClWWalks‘𝐺)) → 2 ≤
(♯‘𝑃)) |
32 | 31 | ex 412 |
1
⊢ (𝐺 ∈ UMGraph → (𝑃 ∈ (ClWWalks‘𝐺) → 2 ≤
(♯‘𝑃))) |