Metamath Proof Explorer

Theorem ordfin

Description: A generalization of onfin to include the class of all ordinals. (Contributed by Scott Fenton, 19-Feb-2026)

Ref Expression
Assertion ordfin ⊢ Ord ⁡ A → A ∈ Fin ↔ A ∈ ω

Proof

Step Hyp Ref Expression
1 ordeleqon ⊢ Ord ⁡ A ↔ A ∈ On ∨ A = On
2 onfin ⊢ A ∈ On → A ∈ Fin ↔ A ∈ ω
3 onprc ⊢ ¬ On ∈ V
4 elex ⊢ On ∈ Fin → On ∈ V
5 3 4 mto ⊢ ¬ On ∈ Fin
6 eleq1 ⊢ A = On → A ∈ Fin ↔ On ∈ Fin
7 5 6 mtbiri ⊢ A = On → ¬ A ∈ Fin
8 elex ⊢ On ∈ ω → On ∈ V
9 3 8 mto ⊢ ¬ On ∈ ω
10 eleq1 ⊢ A = On → A ∈ ω ↔ On ∈ ω
11 9 10 mtbiri ⊢ A = On → ¬ A ∈ ω
12 7 11 2falsed ⊢ A = On → A ∈ Fin ↔ A ∈ ω
13 2 12 jaoi ⊢ A ∈ On ∨ A = On → A ∈ Fin ↔ A ∈ ω
14 1 13 sylbi ⊢ Ord ⁡ A → A ∈ Fin ↔ A ∈ ω