Theorem ominf

Description: The set of natural numbers is infinite. Corollary 6D(b) of Enderton p. 136. (Contributed by NM, 2-Jun-1998) Avoid ax-pow . (Revised by BTernaryTau, 2-Jan-2025)

	Ref	Expression
Assertion	ominf	|- -. _om e. Fin

Proof

Step	Hyp	Ref	Expression
1		isfi	|- ( _om e. Fin <-> E. x e. _om _om ~~ x )
2		nnord	|- ( x e. _om -> Ord x )
3		ordom	|- Ord _om
4		ordelssne	|- ( ( Ord x /\ Ord _om ) -> ( x e. _om <-> ( x C_ _om /\ x =/= _om ) ) )
5	2 3 4	sylancl	|- ( x e. _om -> ( x e. _om <-> ( x C_ _om /\ x =/= _om ) ) )
6	5	ibi	|- ( x e. _om -> ( x C_ _om /\ x =/= _om ) )
7		df-pss	|- ( x C. _om <-> ( x C_ _om /\ x =/= _om ) )
8	6 7	sylibr	|- ( x e. _om -> x C. _om )
9		nnfi	|- ( x e. _om -> x e. Fin )
10		ensymfib	|- ( x e. Fin -> ( x ~~ _om <-> _om ~~ x ) )
11	9 10	syl	|- ( x e. _om -> ( x ~~ _om <-> _om ~~ x ) )
12	11	biimpar	|- ( ( x e. _om /\ _om ~~ x ) -> x ~~ _om )
13		pssinf	|- ( ( x C. _om /\ x ~~ _om ) -> -. _om e. Fin )
14	8 12 13	syl2an2r	|- ( ( x e. _om /\ _om ~~ x ) -> -. _om e. Fin )
15	14	rexlimiva	|- ( E. x e. _om _om ~~ x -> -. _om e. Fin )
16	1 15	sylbi	|- ( _om e. Fin -> -. _om e. Fin )
17		pm2.01	|- ( ( _om e. Fin -> -. _om e. Fin ) -> -. _om e. Fin )
18	16 17	ax-mp	|- -. _om e. Fin