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

Metamath Proof Explorer

Theorem infinfg

Description: Equivalence between two infiniteness criteria for sets. To avoid the axiom of infinity, we include it as a hypothesis. (Contributed by Scott Fenton, 20-Feb-2026)

Ref Expression
Assertion infinfg ⊢ ω ∈ V ∧ A ∈ B → ¬ A ∈ Fin ↔ ω ≼ A

Proof

Step Hyp Ref Expression
1 isfiniteg ⊢ ω ∈ V → A ∈ Fin ↔ A ≺ ω
2 1 adantr ⊢ ω ∈ V ∧ A ∈ B → A ∈ Fin ↔ A ≺ ω
3 2 notbid ⊢ ω ∈ V ∧ A ∈ B → ¬ A ∈ Fin ↔ ¬ A ≺ ω
4 domtri ⊢ ω ∈ V ∧ A ∈ B → ω ≼ A ↔ ¬ A ≺ ω
5 3 4 bitr4d ⊢ ω ∈ V ∧ A ∈ B → ¬ A ∈ Fin ↔ ω ≼ A