Proof of Theorem usgra2adedgwlkon
Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
3 | | usgraedgrnv 25906 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
4 | 3 | ancomd 466 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
5 | 4 | adantrr 749 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
6 | 5 | simprd 478 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → 𝐴 ∈ 𝑉) |
7 | 3 | adantrr 749 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
8 | 7 | simprd 478 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → 𝐵 ∈ 𝑉) |
9 | | usgraedgrnv 25906 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
10 | 9 | adantrl 748 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
11 | 10 | simprd 478 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → 𝐶 ∈ 𝑉) |
12 | 6, 8, 11 | 3jca 1235 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
13 | 2, 12 | jca 553 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
14 | | usgra2adedgspthlem1 26139 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) |
15 | | fvex 6113 |
. . . . . . 7
⊢ (◡𝐸‘{𝐴, 𝐵}) ∈ V |
16 | | fvex 6113 |
. . . . . . 7
⊢ (◡𝐸‘{𝐵, 𝐶}) ∈ V |
17 | 15, 16 | pm3.2i 470 |
. . . . . 6
⊢ ((◡𝐸‘{𝐴, 𝐵}) ∈ V ∧ (◡𝐸‘{𝐵, 𝐶}) ∈ V) |
18 | | usgra2adedgspth.f |
. . . . . 6
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} |
19 | | usgra2adedgspth.p |
. . . . . 6
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
20 | 17, 18, 19 | constr2wlk 26128 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶}) → 𝐹(𝑉 Walks 𝐸)𝑃)) |
21 | 13, 14, 20 | sylc 63 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → 𝐹(𝑉 Walks 𝐸)𝑃) |
22 | 3 | ex 449 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
23 | 9 | ex 449 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → ({𝐵, 𝐶} ∈ ran 𝐸 → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
24 | 22, 23 | anim12d 584 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
25 | 19 | 2wlklemA 26084 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑃‘0) = 𝐴) |
26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑃‘0) = 𝐴) |
27 | 17, 18 | 2trllemA 26080 |
. . . . . . . . . 10
⊢
(#‘𝐹) =
2 |
28 | 27 | fveq2i 6106 |
. . . . . . . . 9
⊢ (𝑃‘(#‘𝐹)) = (𝑃‘2) |
29 | 19 | 2wlklemC 26086 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → (𝑃‘2) = 𝐶) |
30 | 28, 29 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑉 → (𝑃‘(#‘𝐹)) = 𝐶) |
31 | 30 | adantl 481 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃‘(#‘𝐹)) = 𝐶) |
32 | 26, 31 | anim12i 588 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶)) |
33 | 24, 32 | syl6 34 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶))) |
34 | 33 | imp 444 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶)) |
35 | | 3anass 1035 |
. . . 4
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶) ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶))) |
36 | 21, 34, 35 | sylanbrc 695 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶)) |
37 | | prex 4836 |
. . . . . . 7
⊢ {〈0,
(◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∈ V |
38 | 18, 37 | eqeltri 2684 |
. . . . . 6
⊢ 𝐹 ∈ V |
39 | | tpex 6855 |
. . . . . . 7
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈
V |
40 | 19, 39 | eqeltri 2684 |
. . . . . 6
⊢ 𝑃 ∈ V |
41 | 38, 40 | pm3.2i 470 |
. . . . 5
⊢ (𝐹 ∈ V ∧ 𝑃 ∈ V) |
42 | 41 | a1i 11 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
43 | 3 | simpld 474 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 ∈ 𝑉) |
44 | 9 | simprd 478 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → 𝐶 ∈ 𝑉) |
45 | 43, 44 | anim12dan 878 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
46 | | iswlkon 26062 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶))) |
47 | 2, 42, 45, 46 | syl3anc 1318 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐶))) |
48 | 36, 47 | mpbird 246 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃) |
49 | 48 | ex 449 |
1
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃)) |