Description: Equivalence between two infiniteness criteria for sets. (Contributed by David Moews, 1-May-2017) (Proof shortened by Scott Fenton, 20-Feb-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | infinf | |- ( A e. B -> ( -. A e. Fin <-> _om ~<_ A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | omex | |- _om e. _V |
|
| 2 | infinfg | |- ( ( _om e. _V /\ A e. B ) -> ( -. A e. Fin <-> _om ~<_ A ) ) |
|
| 3 | 1 2 | mpan | |- ( A e. B -> ( -. A e. Fin <-> _om ~<_ A ) ) |