| Step | Hyp | Ref
| Expression |
|---|
| 1 | | df-clwwlk 26279 |
. . 3
⊢ ClWWalks
= (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)}) |
| 2 | 1 | elmpt2cl 6774 |
. 2
⊢ (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
| 3 | | pm3.22 464 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉)) |
| 4 | | df-3an 1033 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉)) |
| 5 | 3, 4 | sylibr 223 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)) |
| 6 | 5 | a1d 25 |
. . . 4
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉))) |
| 7 | 6 | ex 449 |
. . 3
⊢ (𝑃 ∈ Word 𝑉 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)))) |
| 8 | | clwwlk 26294 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ClWWalks 𝐸) = {𝑝 ∈ Word 𝑉 ∣ (∀𝑖 ∈ (0..^((#‘𝑝) − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸)}) |
| 9 | 8 | eleq2d 2673 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) ↔ 𝑃 ∈ {𝑝 ∈ Word 𝑉 ∣ (∀𝑖 ∈ (0..^((#‘𝑝) − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸)})) |
| 10 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑃 → (#‘𝑝) = (#‘𝑃)) |
| 11 | 10 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → ((#‘𝑝) − 1) = ((#‘𝑃) − 1)) |
| 12 | 11 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → (0..^((#‘𝑝) − 1)) = (0..^((#‘𝑃) − 1))) |
| 13 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑃 → (𝑝‘𝑖) = (𝑃‘𝑖)) |
| 14 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑃 → (𝑝‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
| 15 | 13, 14 | preq12d 4220 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → {(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
| 16 | 15 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → ({(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
| 17 | 12, 16 | raleqbidv 3129 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (∀𝑖 ∈ (0..^((#‘𝑝) − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
| 18 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → ( lastS ‘𝑝) = ( lastS ‘𝑃)) |
| 19 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → (𝑝‘0) = (𝑃‘0)) |
| 20 | 18, 19 | preq12d 4220 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → {( lastS ‘𝑝), (𝑝‘0)} = {( lastS ‘𝑃), (𝑃‘0)}) |
| 21 | 20 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → ({( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸 ↔ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) |
| 22 | 17, 21 | anbi12d 743 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → ((∀𝑖 ∈ (0..^((#‘𝑝) − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸))) |
| 23 | 22 | elrab 3331 |
. . . . . 6
⊢ (𝑃 ∈ {𝑝 ∈ Word 𝑉 ∣ (∀𝑖 ∈ (0..^((#‘𝑝) − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸)} ↔ (𝑃 ∈ Word 𝑉 ∧ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸))) |
| 24 | | pm2.24 120 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → (¬ 𝑃 ∈ Word 𝑉 → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉))) |
| 25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (¬ 𝑃 ∈ Word 𝑉 → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉))) |
| 26 | 23, 25 | sylbi 206 |
. . . . 5
⊢ (𝑃 ∈ {𝑝 ∈ Word 𝑉 ∣ (∀𝑖 ∈ (0..^((#‘𝑝) − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸)} → (¬ 𝑃 ∈ Word 𝑉 → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉))) |
| 27 | 9, 26 | syl6bi 242 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (¬ 𝑃 ∈ Word 𝑉 → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)))) |
| 28 | 27 | com3r 85 |
. . 3
⊢ (¬
𝑃 ∈ Word 𝑉 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)))) |
| 29 | 7, 28 | pm2.61i 175 |
. 2
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉))) |
| 30 | 2, 29 | mpcom 37 |
1
⊢ (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)) |
