theorem finss (A B: set): $ A C_ B -> finite B -> finite A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssel | A C_ B -> x e. A -> x e. B |
|
| 2 | 1 | imim1d | A C_ B -> (x e. B -> x < n) -> x e. A -> x < n |
| 3 | 2 | alimd | A C_ B -> A. x (x e. B -> x < n) -> A. x (x e. A -> x < n) |
| 4 | 3 | eximd | A C_ B -> E. n A. x (x e. B -> x < n) -> E. n A. x (x e. A -> x < n) |
| 5 | 4 | conv finite | A C_ B -> finite B -> finite A |