Step |
Hyp |
Ref |
Expression |
1 |
|
iswspthsnon.v |
|- V = ( Vtx ` G ) |
2 |
|
0ov |
|- ( A (/) B ) = (/) |
3 |
|
df-wspthsnon |
|- WSPathsNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } ) ) |
4 |
3
|
mpondm0 |
|- ( -. ( N e. NN0 /\ G e. _V ) -> ( N WSPathsNOn G ) = (/) ) |
5 |
4
|
oveqd |
|- ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WSPathsNOn G ) B ) = ( A (/) B ) ) |
6 |
|
id |
|- ( -. ( N e. NN0 /\ G e. _V ) -> -. ( N e. NN0 /\ G e. _V ) ) |
7 |
6
|
intnanrd |
|- ( -. ( N e. NN0 /\ G e. _V ) -> -. ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) ) |
8 |
1
|
wwlksnon0 |
|- ( -. ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( N WWalksNOn G ) B ) = (/) ) |
9 |
7 8
|
syl |
|- ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WWalksNOn G ) B ) = (/) ) |
10 |
9
|
rabeqdv |
|- ( -. ( N e. NN0 /\ G e. _V ) -> { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = { w e. (/) | E. f f ( A ( SPathsOn ` G ) B ) w } ) |
11 |
|
rab0 |
|- { w e. (/) | E. f f ( A ( SPathsOn ` G ) B ) w } = (/) |
12 |
10 11
|
eqtrdi |
|- ( -. ( N e. NN0 /\ G e. _V ) -> { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = (/) ) |
13 |
2 5 12
|
3eqtr4a |
|- ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } ) |
14 |
1
|
wspthsnon |
|- ( ( N e. NN0 /\ G e. _V ) -> ( N WSPathsNOn G ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) ) |
15 |
14
|
adantr |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( N WSPathsNOn G ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) ) |
16 |
15
|
oveqd |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( A ( N WSPathsNOn G ) B ) = ( A ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) B ) ) |
17 |
|
eqid |
|- ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) |
18 |
17
|
mpondm0 |
|- ( -. ( A e. V /\ B e. V ) -> ( A ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) B ) = (/) ) |
19 |
18
|
adantl |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( A ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) B ) = (/) ) |
20 |
16 19
|
eqtrd |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( A ( N WSPathsNOn G ) B ) = (/) ) |
21 |
20
|
ex |
|- ( ( N e. NN0 /\ G e. _V ) -> ( -. ( A e. V /\ B e. V ) -> ( A ( N WSPathsNOn G ) B ) = (/) ) ) |
22 |
5 2
|
eqtrdi |
|- ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WSPathsNOn G ) B ) = (/) ) |
23 |
22
|
a1d |
|- ( -. ( N e. NN0 /\ G e. _V ) -> ( -. ( A e. V /\ B e. V ) -> ( A ( N WSPathsNOn G ) B ) = (/) ) ) |
24 |
21 23
|
pm2.61i |
|- ( -. ( A e. V /\ B e. V ) -> ( A ( N WSPathsNOn G ) B ) = (/) ) |
25 |
1
|
wwlksonvtx |
|- ( w e. ( A ( N WWalksNOn G ) B ) -> ( A e. V /\ B e. V ) ) |
26 |
25
|
pm2.24d |
|- ( w e. ( A ( N WWalksNOn G ) B ) -> ( -. ( A e. V /\ B e. V ) -> -. f ( A ( SPathsOn ` G ) B ) w ) ) |
27 |
26
|
impcom |
|- ( ( -. ( A e. V /\ B e. V ) /\ w e. ( A ( N WWalksNOn G ) B ) ) -> -. f ( A ( SPathsOn ` G ) B ) w ) |
28 |
27
|
nexdv |
|- ( ( -. ( A e. V /\ B e. V ) /\ w e. ( A ( N WWalksNOn G ) B ) ) -> -. E. f f ( A ( SPathsOn ` G ) B ) w ) |
29 |
28
|
ralrimiva |
|- ( -. ( A e. V /\ B e. V ) -> A. w e. ( A ( N WWalksNOn G ) B ) -. E. f f ( A ( SPathsOn ` G ) B ) w ) |
30 |
|
rabeq0 |
|- ( { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = (/) <-> A. w e. ( A ( N WWalksNOn G ) B ) -. E. f f ( A ( SPathsOn ` G ) B ) w ) |
31 |
29 30
|
sylibr |
|- ( -. ( A e. V /\ B e. V ) -> { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = (/) ) |
32 |
24 31
|
eqtr4d |
|- ( -. ( A e. V /\ B e. V ) -> ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } ) |
33 |
14
|
adantr |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( N WSPathsNOn G ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) ) |
34 |
|
oveq12 |
|- ( ( a = A /\ b = B ) -> ( a ( N WWalksNOn G ) b ) = ( A ( N WWalksNOn G ) B ) ) |
35 |
|
oveq12 |
|- ( ( a = A /\ b = B ) -> ( a ( SPathsOn ` G ) b ) = ( A ( SPathsOn ` G ) B ) ) |
36 |
35
|
breqd |
|- ( ( a = A /\ b = B ) -> ( f ( a ( SPathsOn ` G ) b ) w <-> f ( A ( SPathsOn ` G ) B ) w ) ) |
37 |
36
|
exbidv |
|- ( ( a = A /\ b = B ) -> ( E. f f ( a ( SPathsOn ` G ) b ) w <-> E. f f ( A ( SPathsOn ` G ) B ) w ) ) |
38 |
34 37
|
rabeqbidv |
|- ( ( a = A /\ b = B ) -> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } ) |
39 |
38
|
adantl |
|- ( ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) /\ ( a = A /\ b = B ) ) -> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } ) |
40 |
|
simprl |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> A e. V ) |
41 |
|
simprr |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> B e. V ) |
42 |
|
ovex |
|- ( A ( N WWalksNOn G ) B ) e. _V |
43 |
42
|
rabex |
|- { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } e. _V |
44 |
43
|
a1i |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } e. _V ) |
45 |
33 39 40 41 44
|
ovmpod |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } ) |
46 |
13 32 45
|
ecase |
|- ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } |