theorem nffin {x: nat} (A: set x): $ FS/ x A $ > $ F/ x finite A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h | FS/ x A |
|
| 2 | 1 | nfel2 | F/ x a2 e. A |
| 3 | nfv | F/ x a2 < a1 |
|
| 4 | 2, 3 | nfim | F/ x a2 e. A -> a2 < a1 |
| 5 | 4 | nfal | F/ x A. a2 (a2 e. A -> a2 < a1) |
| 6 | 5 | nfex | F/ x E. a1 A. a2 (a2 e. A -> a2 < a1) |
| 7 | 6 | conv finite | F/ x finite A |