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

Metamath Proof Explorer

Theorem onfin

Description: An ordinal number is finite iff it is a natural number. Proposition 10.32 of TakeutiZaring p. 92. (Contributed by NM, 26-Jul-2004)

Ref Expression
Assertion onfin ( 𝐴 ∈ On → ( 𝐴 ∈ Fin ↔ 𝐴 ∈ ω ) )

Proof

Step Hyp Ref Expression
1 isfi ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
2 onomeneq ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ ω ) → ( 𝐴 ≈ 𝑥 ↔ 𝐴 = 𝑥 ) )
3 eleq1a ⊢ ( 𝑥 ∈ ω → ( 𝐴 = 𝑥 → 𝐴 ∈ ω ) )
4 3 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ ω ) → ( 𝐴 = 𝑥 → 𝐴 ∈ ω ) )
5 2 4 sylbid ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ ω ) → ( 𝐴 ≈ 𝑥 → 𝐴 ∈ ω ) )
6 5 rexlimdva ⊢ ( 𝐴 ∈ On → ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → 𝐴 ∈ ω ) )
7 enrefnn ⊢ ( 𝐴 ∈ ω → 𝐴 ≈ 𝐴 )
8 breq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 ≈ 𝑥 ↔ 𝐴 ≈ 𝐴 ) )
9 8 rspcev ⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≈ 𝐴 ) → ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
10 7 9 mpdan ⊢ ( 𝐴 ∈ ω → ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
11 6 10 impbid1 ⊢ ( 𝐴 ∈ On → ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ↔ 𝐴 ∈ ω ) )
12 1 11 bitrid ⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ Fin ↔ 𝐴 ∈ ω ) )