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	$⊢ A \in On \to (A \in Fin \leftrightarrow A \in ω)$

Step	Hyp	Ref	Expression
1		isfi	$⊢ A \in Fin \leftrightarrow \exists x \in ω A \approx x$
2		onomeneq	$⊢ (A \in On \land x \in ω) \to (A \approx x \leftrightarrow A = x)$
3		eleq1a	$⊢ x \in ω \to (A = x \to A \in ω)$
4	3	adantl	$⊢ (A \in On \land x \in ω) \to (A = x \to A \in ω)$
5	2 4	sylbid	$⊢ (A \in On \land x \in ω) \to (A \approx x \to A \in ω)$
6	5	rexlimdva	$⊢ A \in On \to (\exists x \in ω A \approx x \to A \in ω)$
7		enrefg	$⊢ A \in ω \to A \approx A$
8		breq2	$⊢ x = A \to (A \approx x \leftrightarrow A \approx A)$
9	8	rspcev	$⊢ (A \in ω \land A \approx A) \to \exists x \in ω A \approx x$
10	7 9	mpdan	$⊢ A \in ω \to \exists x \in ω A \approx x$
11	6 10	impbid1	$⊢ A \in On \to (\exists x \in ω A \approx x \leftrightarrow A \in ω)$
12	1 11	bitrid	$⊢ A \in On \to (A \in Fin \leftrightarrow A \in ω)$

Metamath Proof Explorer