Description: The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | finresfin | |- ( E e. Fin -> ( E |` B ) e. Fin ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resss | |- ( E |` B ) C_ E |
|
2 | ssfi | |- ( ( E e. Fin /\ ( E |` B ) C_ E ) -> ( E |` B ) e. Fin ) |
|
3 | 1 2 | mpan2 | |- ( E e. Fin -> ( E |` B ) e. Fin ) |