This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infinf

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 ∈ B → ¬ A ∈ Fin ↔ ω ≼ A

Proof

Step Hyp Ref Expression
1 omex ⊢ ω ∈ V
2 infinfg ⊢ ω ∈ V ∧ A ∈ B → ¬ A ∈ Fin ↔ ω ≼ A
3 1 2 mpan ⊢ A ∈ B → ¬ A ∈ Fin ↔ ω ≼ A