Theorem 1pi

Description: Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	1pi	⊢ 1o ∈ N

Proof

Step	Hyp	Ref	Expression
1		1onn	⊢ 1o ∈ ω
2		1n0	⊢ 1o ≠ ∅
3		elni	⊢ ( 1o ∈ N ↔ ( 1o ∈ ω ∧ 1o ≠ ∅ ) )
4	1 2 3	mpbir2an	⊢ 1o ∈ N