Proof of Theorem usgra2adedgwlk
Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
3 | | usgraedgrnv 25906 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
4 | 3 | ancomd 466 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
5 | 4 | adantrr 749 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
6 | 5 | simprd 478 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → 𝐴 ∈ 𝑉) |
7 | 3 | adantrr 749 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
8 | 7 | simprd 478 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → 𝐵 ∈ 𝑉) |
9 | | usgraedgrnv 25906 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
10 | 9 | adantrl 748 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
11 | 10 | simprd 478 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → 𝐶 ∈ 𝑉) |
12 | 6, 8, 11 | 3jca 1235 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
13 | 2, 12 | jca 553 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
14 | | simpl 472 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
15 | | usgra2adedgspthlem1 26139 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) |
16 | 15 | adantl 481 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) → ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) |
17 | | fvex 6113 |
. . . . . . 7
⊢ (◡𝐸‘{𝐴, 𝐵}) ∈ V |
18 | | fvex 6113 |
. . . . . . 7
⊢ (◡𝐸‘{𝐵, 𝐶}) ∈ V |
19 | 17, 18 | pm3.2i 470 |
. . . . . 6
⊢ ((◡𝐸‘{𝐴, 𝐵}) ∈ V ∧ (◡𝐸‘{𝐵, 𝐶}) ∈ V) |
20 | | usgra2adedgspth.f |
. . . . . 6
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} |
21 | | usgra2adedgspth.p |
. . . . . 6
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
22 | 19, 20, 21 | constr2wlk 26128 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶}) → 𝐹(𝑉 Walks 𝐸)𝑃)) |
23 | 14, 16, 22 | sylc 63 |
. . . 4
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) → 𝐹(𝑉 Walks 𝐸)𝑃) |
24 | 19, 20 | 2trllemA 26080 |
. . . . 5
⊢
(#‘𝐹) =
2 |
25 | 24 | a1i 11 |
. . . 4
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) → (#‘𝐹) = 2) |
26 | 21 | 2wlklemA 26084 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑃‘0) = 𝐴) |
27 | 26 | eqcomd 2616 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝐴 = (𝑃‘0)) |
28 | 21 | 2wlklemB 26085 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → (𝑃‘1) = 𝐵) |
29 | 28 | eqcomd 2616 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑉 → 𝐵 = (𝑃‘1)) |
30 | 21 | 2wlklemC 26086 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑉 → (𝑃‘2) = 𝐶) |
31 | 30 | eqcomd 2616 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝑃‘2)) |
32 | 27, 29, 31 | 3anim123i 1240 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) |
33 | 32 | adantl 481 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) |
34 | 33 | adantr 480 |
. . . 4
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) → (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))) |
35 | 23, 25, 34 | 3jca 1235 |
. . 3
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) → (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)))) |
36 | 13, 35 | mpancom 700 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)))) |
37 | 36 | ex 449 |
1
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2))))) |