Description: Weakly Dedekind-infinite sets are exactly those with an _om -indexed ascending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | isfin3-4 | |- ( A e. V -> ( A e. Fin3 <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` x ) C_ ( f ` suc x ) -> U. ran f e. ran f ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- ( y e. ~P A |-> ( A \ y ) ) = ( y e. ~P A |-> ( A \ y ) ) |
|
| 2 | 1 | isf34lem6 | |- ( A e. V -> ( A e. Fin3 <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` x ) C_ ( f ` suc x ) -> U. ran f e. ran f ) ) ) |