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

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 𝐴 → ( 𝐴 ∈ Fin ↔ 𝐴 ∈ ω ) )

Proof

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