Step |
Hyp |
Ref |
Expression |
1 |
|
elwwlks2on.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
wspthnon |
⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) ) |
3 |
2
|
biimpi |
⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) ) |
4 |
1
|
elwwlks2on |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) ) |
5 |
|
simpl |
⊢ ( ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ) |
6 |
|
eleq1 |
⊢ ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) |
7 |
6
|
biimpa |
⊢ ( ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) |
8 |
5 7
|
jca |
⊢ ( ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) |
9 |
8
|
ex |
⊢ ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) |
10 |
9
|
adantr |
⊢ ( ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) |
11 |
10
|
com12 |
⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) |
12 |
11
|
reximdv |
⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) |
13 |
12
|
a1i13 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 → ( ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) ) |
14 |
13
|
com24 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) ) |
15 |
4 14
|
sylbid |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) ) |
16 |
15
|
impd |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) |
17 |
16
|
com23 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) |
18 |
3 17
|
mpdi |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) |
19 |
6
|
biimpar |
⊢ ( ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) |
20 |
19
|
a1i |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) |
21 |
20
|
rexlimdva |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) |
22 |
18 21
|
impbid |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑊 = 〈“ 𝐴 𝑏 𝐶 ”〉 ∧ 〈“ 𝐴 𝑏 𝐶 ”〉 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) |