Step | Hyp | Ref
| Expression |
1 | | elwwlks2on.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | wspthnon 41054 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑊))) |
3 | 2 | biimpd 218 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑊))) |
4 | 3 | 3adant1 1072 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑊))) |
5 | 1 | elwwlks2on 41162 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)))) |
6 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → 𝑊 = 〈“𝐴𝑏𝐶”〉) |
7 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑊 = 〈“𝐴𝑏𝐶”〉 → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))) |
8 | 7 | biimpa 500 |
. . . . . . . . . . . . 13
⊢ ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) |
9 | 6, 8 | jca 553 |
. . . . . . . . . . . 12
⊢ ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))) |
10 | 9 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑊 = 〈“𝐴𝑏𝐶”〉 → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))) |
11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))) |
12 | 11 | com12 32 |
. . . . . . . . 9
⊢ (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) → (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))) |
13 | 12 | reximdv 2999 |
. . . . . . . 8
⊢ (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))) |
14 | 13 | a1i13 27 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑊 → (∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))))) |
15 | 14 | com24 93 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) → (∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑊 → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))))) |
16 | 5, 15 | sylbid 229 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → (∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑊 → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))))) |
17 | 16 | impd 446 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑊) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))))) |
18 | 17 | com23 84 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → ((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑊) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))))) |
19 | 4, 18 | mpdd 42 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))) |
20 | 7 | biimpar 501 |
. . . 4
⊢ ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → 𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) |
21 | 20 | a1i 11 |
. . 3
⊢ (((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → 𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))) |
22 | 21 | rexlimdva 3013 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → 𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶))) |
23 | 19, 22 | impbid 201 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))) |