Step | Hyp | Ref
| Expression |
1 | | clwwlkn1 29034 |
. 2
⊢ (𝑊 ∈ (1 ClWWalksN 𝐺) ↔ ((♯‘𝑊) = 1 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0)} ∈ (Edg‘𝐺))) |
2 | | wrdl1exs1 14510 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 1) → ∃𝑣 ∈ (Vtx‘𝐺)𝑊 = ⟨“𝑣”⟩) |
3 | | fveq1 6845 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 = ⟨“𝑣”⟩ → (𝑊‘0) = (⟨“𝑣”⟩‘0)) |
4 | | s1fv 14507 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ (Vtx‘𝐺) → (⟨“𝑣”⟩‘0) = 𝑣) |
5 | 3, 4 | sylan9eq 2793 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 = ⟨“𝑣”⟩ ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝑊‘0) = 𝑣) |
6 | 5 | sneqd 4602 |
. . . . . . . . . . . . 13
⊢ ((𝑊 = ⟨“𝑣”⟩ ∧ 𝑣 ∈ (Vtx‘𝐺)) → {(𝑊‘0)} = {𝑣}) |
7 | 6 | eleq1d 2819 |
. . . . . . . . . . . 12
⊢ ((𝑊 = ⟨“𝑣”⟩ ∧ 𝑣 ∈ (Vtx‘𝐺)) → ({(𝑊‘0)} ∈ (Edg‘𝐺) ↔ {𝑣} ∈ (Edg‘𝐺))) |
8 | 7 | biimpd 228 |
. . . . . . . . . . 11
⊢ ((𝑊 = ⟨“𝑣”⟩ ∧ 𝑣 ∈ (Vtx‘𝐺)) → ({(𝑊‘0)} ∈ (Edg‘𝐺) → {𝑣} ∈ (Edg‘𝐺))) |
9 | 8 | ex 414 |
. . . . . . . . . 10
⊢ (𝑊 = ⟨“𝑣”⟩ → (𝑣 ∈ (Vtx‘𝐺) → ({(𝑊‘0)} ∈ (Edg‘𝐺) → {𝑣} ∈ (Edg‘𝐺)))) |
10 | 9 | com13 88 |
. . . . . . . . 9
⊢ ({(𝑊‘0)} ∈
(Edg‘𝐺) → (𝑣 ∈ (Vtx‘𝐺) → (𝑊 = ⟨“𝑣”⟩ → {𝑣} ∈ (Edg‘𝐺)))) |
11 | 10 | imp 408 |
. . . . . . . 8
⊢ (({(𝑊‘0)} ∈
(Edg‘𝐺) ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝑊 = ⟨“𝑣”⟩ → {𝑣} ∈ (Edg‘𝐺))) |
12 | 11 | ancld 552 |
. . . . . . 7
⊢ (({(𝑊‘0)} ∈
(Edg‘𝐺) ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝑊 = ⟨“𝑣”⟩ → (𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺)))) |
13 | 12 | reximdva 3162 |
. . . . . 6
⊢ ({(𝑊‘0)} ∈
(Edg‘𝐺) →
(∃𝑣 ∈
(Vtx‘𝐺)𝑊 = ⟨“𝑣”⟩ →
∃𝑣 ∈
(Vtx‘𝐺)(𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺)))) |
14 | 2, 13 | syl5com 31 |
. . . . 5
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 1) → ({(𝑊‘0)} ∈
(Edg‘𝐺) →
∃𝑣 ∈
(Vtx‘𝐺)(𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺)))) |
15 | 14 | expcom 415 |
. . . 4
⊢
((♯‘𝑊) =
1 → (𝑊 ∈ Word
(Vtx‘𝐺) →
({(𝑊‘0)} ∈
(Edg‘𝐺) →
∃𝑣 ∈
(Vtx‘𝐺)(𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺))))) |
16 | 15 | 3imp 1112 |
. . 3
⊢
(((♯‘𝑊)
= 1 ∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧ {(𝑊‘0)} ∈
(Edg‘𝐺)) →
∃𝑣 ∈
(Vtx‘𝐺)(𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺))) |
17 | | s1len 14503 |
. . . . . . . 8
⊢
(♯‘⟨“𝑣”⟩) = 1 |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ ((𝑣 ∈ (Vtx‘𝐺) ∧ {𝑣} ∈ (Edg‘𝐺)) → (♯‘⟨“𝑣”⟩) =
1) |
19 | | s1cl 14499 |
. . . . . . . 8
⊢ (𝑣 ∈ (Vtx‘𝐺) → ⟨“𝑣”⟩ ∈ Word
(Vtx‘𝐺)) |
20 | 19 | adantr 482 |
. . . . . . 7
⊢ ((𝑣 ∈ (Vtx‘𝐺) ∧ {𝑣} ∈ (Edg‘𝐺)) → ⟨“𝑣”⟩ ∈ Word (Vtx‘𝐺)) |
21 | 4 | eqcomd 2739 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ (Vtx‘𝐺) → 𝑣 = (⟨“𝑣”⟩‘0)) |
22 | 21 | sneqd 4602 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (Vtx‘𝐺) → {𝑣} = {(⟨“𝑣”⟩‘0)}) |
23 | 22 | eleq1d 2819 |
. . . . . . . . 9
⊢ (𝑣 ∈ (Vtx‘𝐺) → ({𝑣} ∈ (Edg‘𝐺) ↔ {(⟨“𝑣”⟩‘0)} ∈
(Edg‘𝐺))) |
24 | 23 | biimpd 228 |
. . . . . . . 8
⊢ (𝑣 ∈ (Vtx‘𝐺) → ({𝑣} ∈ (Edg‘𝐺) → {(⟨“𝑣”⟩‘0)} ∈
(Edg‘𝐺))) |
25 | 24 | imp 408 |
. . . . . . 7
⊢ ((𝑣 ∈ (Vtx‘𝐺) ∧ {𝑣} ∈ (Edg‘𝐺)) → {(⟨“𝑣”⟩‘0)} ∈
(Edg‘𝐺)) |
26 | 18, 20, 25 | 3jca 1129 |
. . . . . 6
⊢ ((𝑣 ∈ (Vtx‘𝐺) ∧ {𝑣} ∈ (Edg‘𝐺)) → ((♯‘⟨“𝑣”⟩) = 1 ∧
⟨“𝑣”⟩
∈ Word (Vtx‘𝐺)
∧ {(⟨“𝑣”⟩‘0)} ∈
(Edg‘𝐺))) |
27 | 26 | adantrl 715 |
. . . . 5
⊢ ((𝑣 ∈ (Vtx‘𝐺) ∧ (𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺))) →
((♯‘⟨“𝑣”⟩) = 1 ∧ ⟨“𝑣”⟩ ∈ Word
(Vtx‘𝐺) ∧
{(⟨“𝑣”⟩‘0)} ∈
(Edg‘𝐺))) |
28 | | fveqeq2 6855 |
. . . . . . 7
⊢ (𝑊 = ⟨“𝑣”⟩ →
((♯‘𝑊) = 1
↔ (♯‘⟨“𝑣”⟩) = 1)) |
29 | | eleq1 2822 |
. . . . . . 7
⊢ (𝑊 = ⟨“𝑣”⟩ → (𝑊 ∈ Word (Vtx‘𝐺) ↔ ⟨“𝑣”⟩ ∈ Word
(Vtx‘𝐺))) |
30 | 3 | sneqd 4602 |
. . . . . . . 8
⊢ (𝑊 = ⟨“𝑣”⟩ → {(𝑊‘0)} =
{(⟨“𝑣”⟩‘0)}) |
31 | 30 | eleq1d 2819 |
. . . . . . 7
⊢ (𝑊 = ⟨“𝑣”⟩ → ({(𝑊‘0)} ∈
(Edg‘𝐺) ↔
{(⟨“𝑣”⟩‘0)} ∈
(Edg‘𝐺))) |
32 | 28, 29, 31 | 3anbi123d 1437 |
. . . . . 6
⊢ (𝑊 = ⟨“𝑣”⟩ →
(((♯‘𝑊) = 1
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧ {(𝑊‘0)} ∈
(Edg‘𝐺)) ↔
((♯‘⟨“𝑣”⟩) = 1 ∧ ⟨“𝑣”⟩ ∈ Word
(Vtx‘𝐺) ∧
{(⟨“𝑣”⟩‘0)} ∈
(Edg‘𝐺)))) |
33 | 32 | ad2antrl 727 |
. . . . 5
⊢ ((𝑣 ∈ (Vtx‘𝐺) ∧ (𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺))) → (((♯‘𝑊) = 1 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0)} ∈ (Edg‘𝐺)) ↔
((♯‘⟨“𝑣”⟩) = 1 ∧ ⟨“𝑣”⟩ ∈ Word
(Vtx‘𝐺) ∧
{(⟨“𝑣”⟩‘0)} ∈
(Edg‘𝐺)))) |
34 | 27, 33 | mpbird 257 |
. . . 4
⊢ ((𝑣 ∈ (Vtx‘𝐺) ∧ (𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺))) → ((♯‘𝑊) = 1 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0)} ∈ (Edg‘𝐺))) |
35 | 34 | rexlimiva 3141 |
. . 3
⊢
(∃𝑣 ∈
(Vtx‘𝐺)(𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺)) → ((♯‘𝑊) = 1 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0)} ∈ (Edg‘𝐺))) |
36 | 16, 35 | impbii 208 |
. 2
⊢
(((♯‘𝑊)
= 1 ∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧ {(𝑊‘0)} ∈
(Edg‘𝐺)) ↔
∃𝑣 ∈
(Vtx‘𝐺)(𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺))) |
37 | 1, 36 | bitri 275 |
1
⊢ (𝑊 ∈ (1 ClWWalksN 𝐺) ↔ ∃𝑣 ∈ (Vtx‘𝐺)(𝑊 = ⟨“𝑣”⟩ ∧ {𝑣} ∈ (Edg‘𝐺))) |