Theorem 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 ∩ Fin )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ On )
2		onfin	⊢ ( 𝑥 ∈ On → ( 𝑥 ∈ Fin ↔ 𝑥 ∈ ω ) )
3	2	biimprcd	⊢ ( 𝑥 ∈ ω → ( 𝑥 ∈ On → 𝑥 ∈ Fin ) )
4	1 3	jcai	⊢ ( 𝑥 ∈ ω → ( 𝑥 ∈ On ∧ 𝑥 ∈ Fin ) )
5	2	biimpa	⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ∈ Fin ) → 𝑥 ∈ ω )
6	4 5	impbii	⊢ ( 𝑥 ∈ ω ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ Fin ) )
7		elin	⊢ ( 𝑥 ∈ ( On ∩ Fin ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ Fin ) )
8	6 7	bitr4i	⊢ ( 𝑥 ∈ ω ↔ 𝑥 ∈ ( On ∩ Fin ) )
9	8	eqriv	⊢ ω = ( On ∩ Fin )