Proof of Theorem clwwlknon1
| Step | Hyp | Ref
| Expression |
| 1 | | clwwlknon1.c |
. . . 4
⊢ 𝐶 = (ClWWalksNOn‘𝐺) |
| 2 | 1 | oveqi 7444 |
. . 3
⊢ (𝑋𝐶1) = (𝑋(ClWWalksNOn‘𝐺)1) |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝑋 ∈ 𝑉 → (𝑋𝐶1) = (𝑋(ClWWalksNOn‘𝐺)1)) |
| 4 | | clwwlknon 30109 |
. . 3
⊢ (𝑋(ClWWalksNOn‘𝐺)1) = {𝑤 ∈ (1 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} |
| 5 | 4 | a1i 11 |
. 2
⊢ (𝑋 ∈ 𝑉 → (𝑋(ClWWalksNOn‘𝐺)1) = {𝑤 ∈ (1 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
| 6 | | clwwlkn1 30060 |
. . . . 5
⊢ (𝑤 ∈ (1 ClWWalksN 𝐺) ↔ ((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺))) |
| 7 | 6 | anbi1i 624 |
. . . 4
⊢ ((𝑤 ∈ (1 ClWWalksN 𝐺) ∧ (𝑤‘0) = 𝑋) ↔ (((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋)) |
| 8 | | clwwlknon1.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Vtx‘𝐺) |
| 9 | 8 | eqcomi 2746 |
. . . . . . . . . . 11
⊢
(Vtx‘𝐺) =
𝑉 |
| 10 | 9 | wrdeqi 14575 |
. . . . . . . . . 10
⊢ Word
(Vtx‘𝐺) = Word 𝑉 |
| 11 | 10 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑤 ∈ Word (Vtx‘𝐺) ↔ 𝑤 ∈ Word 𝑉) |
| 12 | 11 | biimpi 216 |
. . . . . . . 8
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → 𝑤 ∈ Word 𝑉) |
| 13 | 12 | 3ad2ant2 1135 |
. . . . . . 7
⊢
(((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0)} ∈
(Edg‘𝐺)) → 𝑤 ∈ Word 𝑉) |
| 14 | 13 | ad2antrl 728 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋)) → 𝑤 ∈ Word 𝑉) |
| 15 | 13 | adantr 480 |
. . . . . . . . 9
⊢
((((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0)} ∈
(Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋) → 𝑤 ∈ Word 𝑉) |
| 16 | | simpl1 1192 |
. . . . . . . . 9
⊢
((((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0)} ∈
(Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋) → (♯‘𝑤) = 1) |
| 17 | | simpr 484 |
. . . . . . . . 9
⊢
((((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0)} ∈
(Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋) → (𝑤‘0) = 𝑋) |
| 18 | 15, 16, 17 | 3jca 1129 |
. . . . . . . 8
⊢
((((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0)} ∈
(Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋) → (𝑤 ∈ Word 𝑉 ∧ (♯‘𝑤) = 1 ∧ (𝑤‘0) = 𝑋)) |
| 19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ (((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋)) → (𝑤 ∈ Word 𝑉 ∧ (♯‘𝑤) = 1 ∧ (𝑤‘0) = 𝑋)) |
| 20 | | wrdl1s1 14652 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑤 = 〈“𝑋”〉 ↔ (𝑤 ∈ Word 𝑉 ∧ (♯‘𝑤) = 1 ∧ (𝑤‘0) = 𝑋))) |
| 21 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ (((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋)) → (𝑤 = 〈“𝑋”〉 ↔ (𝑤 ∈ Word 𝑉 ∧ (♯‘𝑤) = 1 ∧ (𝑤‘0) = 𝑋))) |
| 22 | 19, 21 | mpbird 257 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋)) → 𝑤 = 〈“𝑋”〉) |
| 23 | | sneq 4636 |
. . . . . . . . . . . . 13
⊢ ((𝑤‘0) = 𝑋 → {(𝑤‘0)} = {𝑋}) |
| 24 | | clwwlknon1.e |
. . . . . . . . . . . . . . 15
⊢ 𝐸 = (Edg‘𝐺) |
| 25 | 24 | eqcomi 2746 |
. . . . . . . . . . . . . 14
⊢
(Edg‘𝐺) =
𝐸 |
| 26 | 25 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑤‘0) = 𝑋 → (Edg‘𝐺) = 𝐸) |
| 27 | 23, 26 | eleq12d 2835 |
. . . . . . . . . . . 12
⊢ ((𝑤‘0) = 𝑋 → ({(𝑤‘0)} ∈ (Edg‘𝐺) ↔ {𝑋} ∈ 𝐸)) |
| 28 | 27 | biimpd 229 |
. . . . . . . . . . 11
⊢ ((𝑤‘0) = 𝑋 → ({(𝑤‘0)} ∈ (Edg‘𝐺) → {𝑋} ∈ 𝐸)) |
| 29 | 28 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑉 → ((𝑤‘0) = 𝑋 → ({(𝑤‘0)} ∈ (Edg‘𝐺) → {𝑋} ∈ 𝐸))) |
| 30 | 29 | com13 88 |
. . . . . . . . 9
⊢ ({(𝑤‘0)} ∈
(Edg‘𝐺) →
((𝑤‘0) = 𝑋 → (𝑋 ∈ 𝑉 → {𝑋} ∈ 𝐸))) |
| 31 | 30 | 3ad2ant3 1136 |
. . . . . . . 8
⊢
(((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0)} ∈
(Edg‘𝐺)) →
((𝑤‘0) = 𝑋 → (𝑋 ∈ 𝑉 → {𝑋} ∈ 𝐸))) |
| 32 | 31 | imp 406 |
. . . . . . 7
⊢
((((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0)} ∈
(Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋) → (𝑋 ∈ 𝑉 → {𝑋} ∈ 𝐸)) |
| 33 | 32 | impcom 407 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋)) → {𝑋} ∈ 𝐸) |
| 34 | 14, 22, 33 | jca32 515 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋)) → (𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸))) |
| 35 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑤 = 〈“𝑋”〉 →
(♯‘𝑤) =
(♯‘〈“𝑋”〉)) |
| 36 | | s1len 14644 |
. . . . . . . . . 10
⊢
(♯‘〈“𝑋”〉) = 1 |
| 37 | 35, 36 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑤 = 〈“𝑋”〉 →
(♯‘𝑤) =
1) |
| 38 | 37 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸)) → (♯‘𝑤) = 1) |
| 39 | 38 | adantl 481 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸))) → (♯‘𝑤) = 1) |
| 40 | 8 | wrdeqi 14575 |
. . . . . . . . . 10
⊢ Word
𝑉 = Word (Vtx‘𝐺) |
| 41 | 40 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑤 ∈ Word 𝑉 ↔ 𝑤 ∈ Word (Vtx‘𝐺)) |
| 42 | 41 | biimpi 216 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝑉 → 𝑤 ∈ Word (Vtx‘𝐺)) |
| 43 | 42 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸))) → 𝑤 ∈ Word (Vtx‘𝐺)) |
| 44 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈“𝑋”〉 → (𝑤‘0) = (〈“𝑋”〉‘0)) |
| 45 | | s1fv 14648 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ 𝑉 → (〈“𝑋”〉‘0) = 𝑋) |
| 46 | 44, 45 | sylan9eq 2797 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 = 〈“𝑋”〉 ∧ 𝑋 ∈ 𝑉) → (𝑤‘0) = 𝑋) |
| 47 | 46 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ ((𝑤 = 〈“𝑋”〉 ∧ 𝑋 ∈ 𝑉) → 𝑋 = (𝑤‘0)) |
| 48 | 47 | sneqd 4638 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 〈“𝑋”〉 ∧ 𝑋 ∈ 𝑉) → {𝑋} = {(𝑤‘0)}) |
| 49 | 24 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 〈“𝑋”〉 ∧ 𝑋 ∈ 𝑉) → 𝐸 = (Edg‘𝐺)) |
| 50 | 48, 49 | eleq12d 2835 |
. . . . . . . . . . 11
⊢ ((𝑤 = 〈“𝑋”〉 ∧ 𝑋 ∈ 𝑉) → ({𝑋} ∈ 𝐸 ↔ {(𝑤‘0)} ∈ (Edg‘𝐺))) |
| 51 | 50 | biimpd 229 |
. . . . . . . . . 10
⊢ ((𝑤 = 〈“𝑋”〉 ∧ 𝑋 ∈ 𝑉) → ({𝑋} ∈ 𝐸 → {(𝑤‘0)} ∈ (Edg‘𝐺))) |
| 52 | 51 | impancom 451 |
. . . . . . . . 9
⊢ ((𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸) → (𝑋 ∈ 𝑉 → {(𝑤‘0)} ∈ (Edg‘𝐺))) |
| 53 | 52 | adantl 481 |
. . . . . . . 8
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸)) → (𝑋 ∈ 𝑉 → {(𝑤‘0)} ∈ (Edg‘𝐺))) |
| 54 | 53 | impcom 407 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸))) → {(𝑤‘0)} ∈ (Edg‘𝐺)) |
| 55 | 39, 43, 54 | 3jca 1129 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸))) → ((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺))) |
| 56 | 46 | ex 412 |
. . . . . . . 8
⊢ (𝑤 = 〈“𝑋”〉 → (𝑋 ∈ 𝑉 → (𝑤‘0) = 𝑋)) |
| 57 | 56 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸)) → (𝑋 ∈ 𝑉 → (𝑤‘0) = 𝑋)) |
| 58 | 57 | impcom 407 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸))) → (𝑤‘0) = 𝑋) |
| 59 | 55, 58 | jca 511 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸))) → (((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋)) |
| 60 | 34, 59 | impbida 801 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → ((((♯‘𝑤) = 1 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋) ↔ (𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸)))) |
| 61 | 7, 60 | bitrid 283 |
. . 3
⊢ (𝑋 ∈ 𝑉 → ((𝑤 ∈ (1 ClWWalksN 𝐺) ∧ (𝑤‘0) = 𝑋) ↔ (𝑤 ∈ Word 𝑉 ∧ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸)))) |
| 62 | 61 | rabbidva2 3438 |
. 2
⊢ (𝑋 ∈ 𝑉 → {𝑤 ∈ (1 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} = {𝑤 ∈ Word 𝑉 ∣ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸)}) |
| 63 | 3, 5, 62 | 3eqtrd 2781 |
1
⊢ (𝑋 ∈ 𝑉 → (𝑋𝐶1) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸)}) |