Step |
Hyp |
Ref |
Expression |
1 |
|
fusgrusgr |
|- ( G e. FinUSGraph -> G e. USGraph ) |
2 |
1
|
adantr |
|- ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> G e. USGraph ) |
3 |
|
fusgrfis |
|- ( G e. FinUSGraph -> ( Edg ` G ) e. Fin ) |
4 |
3
|
adantr |
|- ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( Edg ` G ) e. Fin ) |
5 |
|
simpr |
|- ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> N e. ( Vtx ` G ) ) |
6 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
7 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
8 |
6 7
|
nbusgrfi |
|- ( ( G e. USGraph /\ ( Edg ` G ) e. Fin /\ N e. ( Vtx ` G ) ) -> ( G NeighbVtx N ) e. Fin ) |
9 |
2 4 5 8
|
syl3anc |
|- ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( G NeighbVtx N ) e. Fin ) |