Proof of Theorem elwwlks2ons3im
Step | Hyp | Ref
| Expression |
1 | | wwlks2onv.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | wwlksonvtx 28121 |
. 2
⊢ (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
3 | | wwlknon 28123 |
. . 3
⊢ (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ (𝑊 ∈ (2 WWalksN 𝐺) ∧ (𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶)) |
4 | | wwlknbp1 28110 |
. . . . 5
⊢ (𝑊 ∈ (2 WWalksN 𝐺) → (2 ∈
ℕ0 ∧ 𝑊
∈ Word (Vtx‘𝐺)
∧ (♯‘𝑊) =
(2 + 1))) |
5 | | 2p1e3 12045 |
. . . . . . . 8
⊢ (2 + 1) =
3 |
6 | 5 | eqeq2i 2751 |
. . . . . . 7
⊢
((♯‘𝑊) =
(2 + 1) ↔ (♯‘𝑊) = 3) |
7 | | 1ex 10902 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
V |
8 | 7 | tpid2 4703 |
. . . . . . . . . . . . 13
⊢ 1 ∈
{0, 1, 2} |
9 | | fzo0to3tp 13401 |
. . . . . . . . . . . . 13
⊢ (0..^3) =
{0, 1, 2} |
10 | 8, 9 | eleqtrri 2838 |
. . . . . . . . . . . 12
⊢ 1 ∈
(0..^3) |
11 | | oveq2 7263 |
. . . . . . . . . . . 12
⊢
((♯‘𝑊) =
3 → (0..^(♯‘𝑊)) = (0..^3)) |
12 | 10, 11 | eleqtrrid 2846 |
. . . . . . . . . . 11
⊢
((♯‘𝑊) =
3 → 1 ∈ (0..^(♯‘𝑊))) |
13 | | wrdsymbcl 14158 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ∈
(0..^(♯‘𝑊)))
→ (𝑊‘1) ∈
(Vtx‘𝐺)) |
14 | 12, 13 | sylan2 592 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) → (𝑊‘1) ∈ (Vtx‘𝐺)) |
15 | 14 | 3ad2ant1 1131 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊‘1) ∈ (Vtx‘𝐺)) |
16 | | simpl1r 1223 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → (♯‘𝑊) = 3) |
17 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → (𝑊‘0) = 𝐴) |
18 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → (𝑊‘1) = (𝑊‘1)) |
19 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → (𝑊‘2) = 𝐶) |
20 | 17, 18, 19 | 3jca 1126 |
. . . . . . . . . . . . 13
⊢ (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)) |
21 | 20 | 3ad2ant2 1132 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)) |
22 | 21 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)) |
23 | 1 | eqcomi 2747 |
. . . . . . . . . . . . . . . . . 18
⊢
(Vtx‘𝐺) =
𝑉 |
24 | 23 | wrdeqi 14168 |
. . . . . . . . . . . . . . . . 17
⊢ Word
(Vtx‘𝐺) = Word 𝑉 |
25 | 24 | eleq2i 2830 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word (Vtx‘𝐺) ↔ 𝑊 ∈ Word 𝑉) |
26 | 25 | biimpi 215 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 ∈ Word 𝑉) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) → 𝑊 ∈ Word 𝑉) |
28 | 27 | 3ad2ant1 1131 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑊 ∈ Word 𝑉) |
29 | 28 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → 𝑊 ∈ Word 𝑉) |
30 | | simpl3l 1226 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → 𝐴 ∈ 𝑉) |
31 | 23 | eleq2i 2830 |
. . . . . . . . . . . . . 14
⊢ ((𝑊‘1) ∈
(Vtx‘𝐺) ↔ (𝑊‘1) ∈ 𝑉) |
32 | 31 | biimpi 215 |
. . . . . . . . . . . . 13
⊢ ((𝑊‘1) ∈
(Vtx‘𝐺) → (𝑊‘1) ∈ 𝑉) |
33 | 32 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → (𝑊‘1) ∈ 𝑉) |
34 | | simpl3r 1227 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → 𝐶 ∈ 𝑉) |
35 | | eqwrds3 14604 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ (𝑊‘1) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)))) |
36 | 29, 30, 33, 34, 35 | syl13anc 1370 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)))) |
37 | 16, 22, 36 | mpbir2and 709 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) |
38 | 37, 33 | jca 511 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)) |
39 | 15, 38 | mpdan 683 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)) |
40 | 39 | 3exp 1117 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 3) → (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)))) |
41 | 6, 40 | sylan2b 593 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (2 + 1)) → (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)))) |
42 | 41 | 3adant1 1128 |
. . . . 5
⊢ ((2
∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (2 + 1)) → (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)))) |
43 | 4, 42 | syl 17 |
. . . 4
⊢ (𝑊 ∈ (2 WWalksN 𝐺) → (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)))) |
44 | 43 | 3impib 1114 |
. . 3
⊢ ((𝑊 ∈ (2 WWalksN 𝐺) ∧ (𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉))) |
45 | 3, 44 | sylbi 216 |
. 2
⊢ (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉))) |
46 | 2, 45 | mpd 15 |
1
⊢ (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)) |