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