Description: Alternate definition of IV-finite sets: they lack a denumerable subset. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | isfin4-2 | |- ( A e. V -> ( A e. Fin4 <-> -. _om ~<_ A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isfin4 | |- ( A e. V -> ( A e. Fin4 <-> -. E. x ( x C. A /\ x ~~ A ) ) ) |
|
2 | infpssr | |- ( ( x C. A /\ x ~~ A ) -> _om ~<_ A ) |
|
3 | 2 | exlimiv | |- ( E. x ( x C. A /\ x ~~ A ) -> _om ~<_ A ) |
4 | infpss | |- ( _om ~<_ A -> E. x ( x C. A /\ x ~~ A ) ) |
|
5 | 3 4 | impbii | |- ( E. x ( x C. A /\ x ~~ A ) <-> _om ~<_ A ) |
6 | 5 | notbii | |- ( -. E. x ( x C. A /\ x ~~ A ) <-> -. _om ~<_ A ) |
7 | 1 6 | bitrdi | |- ( A e. V -> ( A e. Fin4 <-> -. _om ~<_ A ) ) |