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)

Ref Expression
Assertion infinf ⊢ A ∈ B → ¬ A ∈ Fin ↔ ω ≼ A

Proof

Step Hyp Ref Expression
1 isfinite ⊢ A ∈ Fin ↔ A ≺ ω
2 1 notbii ⊢ ¬ A ∈ Fin ↔ ¬ A ≺ ω
3 omex ⊢ ω ∈ V
4 domtri ⊢ ω ∈ V ∧ A ∈ B → ω ≼ A ↔ ¬ A ≺ ω
5 3 4 mpan ⊢ A ∈ B → ω ≼ A ↔ ¬ A ≺ ω
6 2 5 bitr4id ⊢ A ∈ B → ¬ A ∈ Fin ↔ ω ≼ A