Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksonvtx.v |
|- V = ( Vtx ` G ) |
2 |
|
fvex |
|- ( Vtx ` g ) e. _V |
3 |
2 2
|
pm3.2i |
|- ( ( Vtx ` g ) e. _V /\ ( Vtx ` g ) e. _V ) |
4 |
3
|
rgen2w |
|- A. n e. NN0 A. g e. _V ( ( Vtx ` g ) e. _V /\ ( Vtx ` g ) e. _V ) |
5 |
|
df-wwlksnon |
|- WWalksNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) ) |
6 |
|
fveq2 |
|- ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) ) |
7 |
6 6
|
jca |
|- ( g = G -> ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( Vtx ` g ) = ( Vtx ` G ) ) ) |
8 |
7
|
adantl |
|- ( ( n = N /\ g = G ) -> ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( Vtx ` g ) = ( Vtx ` G ) ) ) |
9 |
5 8
|
el2mpocl |
|- ( A. n e. NN0 A. g e. _V ( ( Vtx ` g ) e. _V /\ ( Vtx ` g ) e. _V ) -> ( W e. ( A ( N WWalksNOn G ) C ) -> ( ( N e. NN0 /\ G e. _V ) /\ ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) ) ) |
10 |
4 9
|
ax-mp |
|- ( W e. ( A ( N WWalksNOn G ) C ) -> ( ( N e. NN0 /\ G e. _V ) /\ ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) ) |
11 |
1
|
eleq2i |
|- ( A e. V <-> A e. ( Vtx ` G ) ) |
12 |
1
|
eleq2i |
|- ( C e. V <-> C e. ( Vtx ` G ) ) |
13 |
11 12
|
anbi12i |
|- ( ( A e. V /\ C e. V ) <-> ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) |
14 |
13
|
biimpri |
|- ( ( A e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) -> ( A e. V /\ C e. V ) ) |
15 |
10 14
|
simpl2im |
|- ( W e. ( A ( N WWalksNOn G ) C ) -> ( A e. V /\ C e. V ) ) |