Proof of Theorem usgr2wspthons3
Step | Hyp | Ref
| Expression |
1 | | 2nn 11062 |
. . . . . 6
⊢ 2 ∈
ℕ |
2 | | ne0i 3880 |
. . . . . 6
⊢
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝐴(2 WSPathsNOn 𝐺)𝐶) ≠ ∅) |
3 | | wspthsnonn0vne 41124 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ (𝐴(2
WSPathsNOn 𝐺)𝐶) ≠ ∅) → 𝐴 ≠ 𝐶) |
4 | 1, 2, 3 | sylancr 694 |
. . . . 5
⊢
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → 𝐴 ≠ 𝐶) |
5 | | simplr 788 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → 𝐴 ≠ 𝐶) |
6 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → 𝐺 ∈ USGraph ) |
7 | | 3simpb 1052 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
8 | 7 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
9 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → 𝐴 ≠ 𝐶) |
10 | 6, 8, 9 | 3jca 1235 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → (𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶)) |
11 | | usgr2wspthon0.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Vtx‘𝐺) |
12 | 11 | wpthswwlks2on 41164 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (𝐴(2 WSPathsNOn 𝐺)𝐶) = (𝐴(2 WWalksNOn 𝐺)𝐶)) |
13 | 12 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
14 | 10, 13 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
15 | 14 | biimpa 500 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) |
16 | 5, 15 | jca 553 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → (𝐴 ≠ 𝐶 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
17 | 16 | exp31 628 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 ≠ 𝐶 → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝐴 ≠ 𝐶 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))))) |
18 | 17 | com13 86 |
. . . . 5
⊢
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝐴 ≠ 𝐶 → ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 ≠ 𝐶 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))))) |
19 | 4, 18 | mpd 15 |
. . . 4
⊢
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 ≠ 𝐶 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))) |
20 | 19 | com12 32 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝐴 ≠ 𝐶 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))) |
21 | 13 | bicomd 212 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))) |
22 | 10, 21 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))) |
23 | 22 | biimpd 218 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))) |
24 | 23 | expimpd 627 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐶 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))) |
25 | 20, 24 | impbid 201 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ (𝐴 ≠ 𝐶 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))) |
26 | | usgrumgr 40409 |
. . . . 5
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph
) |
27 | | usgr2wspthon0.e |
. . . . . 6
⊢ 𝐸 = (Edg‘𝐺) |
28 | 11, 27 | umgrwwlks2on 41161 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
29 | 26, 28 | sylan 487 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
30 | 29 | anbi2d 736 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐶 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) ↔ (𝐴 ≠ 𝐶 ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))) |
31 | | 3anass 1035 |
. . 3
⊢ ((𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (𝐴 ≠ 𝐶 ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
32 | 30, 31 | syl6bbr 277 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐶 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) ↔ (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
33 | 25, 32 | bitrd 267 |
1
⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |