Step |
Hyp |
Ref |
Expression |
1 |
|
wwlknon |
⊢ ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) |
2 |
1
|
a1i |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ) |
3 |
2
|
anbi1d |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) |
4 |
|
3anass |
⊢ ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ) |
5 |
4
|
anbi1i |
⊢ ( ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) |
6 |
|
anass |
⊢ ( ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) |
7 |
5 6
|
bitri |
⊢ ( ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) |
8 |
3 7
|
bitrdi |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) ) |
9 |
8
|
rabbidva2 |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → { 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) } ) |
10 |
|
usgrupgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph ) |
11 |
|
wlklnwwlknupgr |
⊢ ( 𝐺 ∈ UPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) ) |
12 |
10 11
|
syl |
⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) ) |
13 |
12
|
bicomd |
⊢ ( 𝐺 ∈ USGraph → ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) |
15 |
|
simprl |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ) |
16 |
|
simprl |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( 𝑤 ‘ 0 ) = 𝐴 ) |
17 |
16
|
adantr |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ 0 ) = 𝐴 ) |
18 |
|
fveq2 |
⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑤 ‘ 2 ) ) |
19 |
18
|
ad2antll |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑤 ‘ 2 ) ) |
20 |
|
simprr |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( 𝑤 ‘ 2 ) = 𝐵 ) |
21 |
20
|
adantr |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ 2 ) = 𝐵 ) |
22 |
19 21
|
eqtrd |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) |
23 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
24 |
23
|
wlkp |
⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 → 𝑤 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) |
25 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( 0 ... ( ♯ ‘ 𝑓 ) ) = ( 0 ... 2 ) ) |
26 |
25
|
feq2d |
⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑤 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) ) ) |
27 |
24 26
|
syl5ibcom |
⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 → ( ( ♯ ‘ 𝑓 ) = 2 → 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) ) ) |
28 |
27
|
imp |
⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) ) |
29 |
|
id |
⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) ) |
30 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
31 |
|
0elfz |
⊢ ( 2 ∈ ℕ0 → 0 ∈ ( 0 ... 2 ) ) |
32 |
30 31
|
mp1i |
⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → 0 ∈ ( 0 ... 2 ) ) |
33 |
29 32
|
ffvelrnd |
⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ) |
34 |
|
nn0fz0 |
⊢ ( 2 ∈ ℕ0 ↔ 2 ∈ ( 0 ... 2 ) ) |
35 |
30 34
|
mpbi |
⊢ 2 ∈ ( 0 ... 2 ) |
36 |
35
|
a1i |
⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → 2 ∈ ( 0 ... 2 ) ) |
37 |
29 36
|
ffvelrnd |
⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) |
38 |
33 37
|
jca |
⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) ) |
39 |
28 38
|
syl |
⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) ) |
40 |
|
eleq1 |
⊢ ( ( 𝑤 ‘ 0 ) = 𝐴 → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) |
41 |
|
eleq1 |
⊢ ( ( 𝑤 ‘ 2 ) = 𝐵 → ( ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) |
42 |
40 41
|
bi2anan9 |
⊢ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ( ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) ↔ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
43 |
39 42
|
syl5ib |
⊢ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
44 |
43
|
adantl |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
45 |
44
|
imp |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) |
46 |
|
vex |
⊢ 𝑓 ∈ V |
47 |
|
vex |
⊢ 𝑤 ∈ V |
48 |
46 47
|
pm3.2i |
⊢ ( 𝑓 ∈ V ∧ 𝑤 ∈ V ) |
49 |
23
|
iswlkon |
⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑓 ∈ V ∧ 𝑤 ∈ V ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) ) |
50 |
45 48 49
|
sylancl |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) ) |
51 |
15 17 22 50
|
mpbir3and |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) |
52 |
|
simplll |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝐺 ∈ USGraph ) |
53 |
|
simprr |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( ♯ ‘ 𝑓 ) = 2 ) |
54 |
|
simpllr |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝐴 ≠ 𝐵 ) |
55 |
|
usgr2wlkspth |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) |
56 |
52 53 54 55
|
syl3anc |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) |
57 |
51 56
|
mpbid |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) |
58 |
57
|
ex |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) |
59 |
58
|
eximdv |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) |
60 |
59
|
ex |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) |
61 |
60
|
com23 |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) |
62 |
14 61
|
sylbid |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) |
63 |
62
|
imp |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) |
64 |
63
|
pm4.71d |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ↔ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) |
65 |
64
|
bicomd |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) → ( ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ) |
66 |
65
|
rabbidva |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) } = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) } ) |
67 |
9 66
|
eqtrd |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → { 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) } ) |
68 |
23
|
iswspthsnon |
⊢ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } |
69 |
23
|
iswwlksnon |
⊢ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) } |
70 |
67 68 69
|
3eqtr4g |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ) |