onfin2

Description: A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013)

		Ref	Expression
	Assertion	onfin2	$⊢ ω = On \cap Fin$

Step	Hyp	Ref	Expression
1		nnon	$⊢ x \in ω \to x \in On$
2		onfin	$⊢ x \in On \to (x \in Fin \leftrightarrow x \in ω)$
3	2	biimprcd	$⊢ x \in ω \to (x \in On \to x \in Fin)$
4	1 3	jcai	$⊢ x \in ω \to (x \in On \land x \in Fin)$
5	2	biimpa	$⊢ (x \in On \land x \in Fin) \to x \in ω$
6	4 5	impbii	$⊢ x \in ω \leftrightarrow (x \in On \land x \in Fin)$
7		elin	$⊢ x \in (On \cap Fin) \leftrightarrow (x \in On \land x \in Fin)$
8	6 7	bitr4i	$⊢ x \in ω \leftrightarrow x \in (On \cap Fin)$
9	8	eqriv	$⊢ ω = On \cap Fin$

Metamath Proof Explorer