Proof of Theorem usgra2adedgwlkonALT
Step | Hyp | Ref
| Expression |
1 | | usgra2adedgspth.f |
. . 3
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} |
2 | | usgra2adedgspth.p |
. . 3
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
3 | 1, 2 | usgra2adedgwlk 26142 |
. 2
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))))) |
4 | | simp1 1054 |
. . . 4
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → 𝐹(𝑉 Walks 𝐸)𝑃) |
5 | | eqcom 2617 |
. . . . . . 7
⊢ (𝐴 = (𝑃‘0) ↔ (𝑃‘0) = 𝐴) |
6 | 5 | biimpi 205 |
. . . . . 6
⊢ (𝐴 = (𝑃‘0) → (𝑃‘0) = 𝐴) |
7 | 6 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)) → (𝑃‘0) = 𝐴) |
8 | 7 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → (𝑃‘0) = 𝐴) |
9 | | fveq2 6103 |
. . . . . 6
⊢
((#‘𝐹) = 2
→ (𝑃‘(#‘𝐹)) = (𝑃‘2)) |
10 | | eqcom 2617 |
. . . . . . . 8
⊢ (𝐶 = (𝑃‘2) ↔ (𝑃‘2) = 𝐶) |
11 | 10 | biimpi 205 |
. . . . . . 7
⊢ (𝐶 = (𝑃‘2) → (𝑃‘2) = 𝐶) |
12 | 11 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)) → (𝑃‘2) = 𝐶) |
13 | 9, 12 | sylan9eq 2664 |
. . . . 5
⊢
(((#‘𝐹) = 2
∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → (𝑃‘(#‘𝐹)) = 𝐶) |
14 | 13 | 3adant1 1072 |
. . . 4
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → (𝑃‘(#‘𝐹)) = 𝐶) |
15 | 4, 8, 14 | 3jca 1235 |
. . 3
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶)) |
16 | | wlkbprop 26051 |
. . . . . 6
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
17 | | 2mwlk 26049 |
. . . . . 6
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
18 | | simp-4l 802 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) ∧ (#‘𝐹) = 2) ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
19 | | simp-4r 803 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) ∧ (#‘𝐹) = 2) ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
20 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ (0...(#‘𝐹)) =
(0...2)) |
21 | 20 | feq2d 5944 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...2)⟶𝑉)) |
22 | 21 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 2
→ ((𝐹 ∈ Word dom
𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...2)⟶𝑉))) |
23 | 22 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 2
→ ((((𝑉 ∈ V ∧
𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) ↔ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...2)⟶𝑉)))) |
24 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
V |
25 | 24 | tpid1 4246 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
{0, 1, 2} |
26 | | fz0tp 12309 |
. . . . . . . . . . . . . . . . . 18
⊢ (0...2) =
{0, 1, 2} |
27 | 25, 26 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
(0...2) |
28 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃:(0...2)⟶𝑉 ∧ 0 ∈ (0...2)) →
(𝑃‘0) ∈ 𝑉) |
29 | 27, 28 | mpan2 703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0...2)⟶𝑉 → (𝑃‘0) ∈ 𝑉) |
30 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℤ |
31 | 30 | elexi 3186 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
V |
32 | 31 | tpid3 4250 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
{0, 1, 2} |
33 | 32, 26 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
(0...2) |
34 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃:(0...2)⟶𝑉 ∧ 2 ∈ (0...2)) →
(𝑃‘2) ∈ 𝑉) |
35 | 33, 34 | mpan2 703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0...2)⟶𝑉 → (𝑃‘2) ∈ 𝑉) |
36 | 29, 35 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (𝑃:(0...2)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...2)⟶𝑉) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...2)⟶𝑉)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
39 | 23, 38 | syl6bi 242 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ ((((𝑉 ∈ V ∧
𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
40 | 39 | impcom 445 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) ∧ (#‘𝐹) = 2) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) ∧ (#‘𝐹) = 2) ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
42 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝐴 = (𝑃‘0) → (𝐴 ∈ 𝑉 ↔ (𝑃‘0) ∈ 𝑉)) |
43 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝐶 = (𝑃‘2) → (𝐶 ∈ 𝑉 ↔ (𝑃‘2) ∈ 𝑉)) |
44 | 42, 43 | bi2anan9 913 |
. . . . . . . . . . . 12
⊢ ((𝐴 = (𝑃‘0) ∧ 𝐶 = (𝑃‘2)) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
45 | 44 | 3adant2 1073 |
. . . . . . . . . . 11
⊢ ((𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
46 | 45 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) ∧ (#‘𝐹) = 2) ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
47 | 41, 46 | mpbird 246 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) ∧ (#‘𝐹) = 2) ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
48 | 18, 19, 47 | 3jca 1235 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) ∧ (#‘𝐹) = 2) ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
49 | 48 | exp41 636 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((#‘𝐹) = 2 → ((𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))))) |
50 | 49 | 3adant1 1072 |
. . . . . 6
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((#‘𝐹) = 2 → ((𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))))) |
51 | 16, 17, 50 | sylc 63 |
. . . . 5
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) = 2 → ((𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
52 | 51 | 3imp 1249 |
. . . 4
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
53 | | iswlkon 26062 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶))) |
54 | 52, 53 | syl 17 |
. . 3
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶))) |
55 | 15, 54 | mpbird 246 |
. 2
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃) |
56 | 3, 55 | syl6 34 |
1
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃)) |