Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksnon.v |
|- V = ( Vtx ` G ) |
2 |
|
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 } ) ) |
3 |
2
|
a1i |
|- ( ( N e. NN0 /\ G e. U ) -> 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 |
|
fveq2 |
|- ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) ) |
5 |
4 1
|
eqtr4di |
|- ( g = G -> ( Vtx ` g ) = V ) |
6 |
5
|
adantl |
|- ( ( n = N /\ g = G ) -> ( Vtx ` g ) = V ) |
7 |
|
oveq12 |
|- ( ( n = N /\ g = G ) -> ( n WWalksNOn g ) = ( N WWalksNOn G ) ) |
8 |
7
|
oveqd |
|- ( ( n = N /\ g = G ) -> ( a ( n WWalksNOn g ) b ) = ( a ( N WWalksNOn G ) b ) ) |
9 |
|
fveq2 |
|- ( g = G -> ( SPathsOn ` g ) = ( SPathsOn ` G ) ) |
10 |
9
|
oveqd |
|- ( g = G -> ( a ( SPathsOn ` g ) b ) = ( a ( SPathsOn ` G ) b ) ) |
11 |
10
|
breqd |
|- ( g = G -> ( f ( a ( SPathsOn ` g ) b ) w <-> f ( a ( SPathsOn ` G ) b ) w ) ) |
12 |
11
|
adantl |
|- ( ( n = N /\ g = G ) -> ( f ( a ( SPathsOn ` g ) b ) w <-> f ( a ( SPathsOn ` G ) b ) w ) ) |
13 |
12
|
exbidv |
|- ( ( n = N /\ g = G ) -> ( E. f f ( a ( SPathsOn ` g ) b ) w <-> E. f f ( a ( SPathsOn ` G ) b ) w ) ) |
14 |
8 13
|
rabeqbidv |
|- ( ( n = N /\ g = G ) -> { 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 } ) |
15 |
6 6 14
|
mpoeq123dv |
|- ( ( n = N /\ g = G ) -> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { 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 } ) ) |
16 |
15
|
adantl |
|- ( ( ( N e. NN0 /\ G e. U ) /\ ( n = N /\ g = G ) ) -> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { 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 } ) ) |
17 |
|
simpl |
|- ( ( N e. NN0 /\ G e. U ) -> N e. NN0 ) |
18 |
|
elex |
|- ( G e. U -> G e. _V ) |
19 |
18
|
adantl |
|- ( ( N e. NN0 /\ G e. U ) -> G e. _V ) |
20 |
1
|
fvexi |
|- V e. _V |
21 |
20 20
|
mpoex |
|- ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) e. _V |
22 |
21
|
a1i |
|- ( ( N e. NN0 /\ G e. U ) -> ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) e. _V ) |
23 |
3 16 17 19 22
|
ovmpod |
|- ( ( N e. NN0 /\ G e. U ) -> ( N WSPathsNOn G ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) ) |