Theorem uzinf

Description: An upper integer set is infinite. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypothesis	uzinf.1	|- Z = ( ZZ>= ` M )
Assertion	uzinf	|- ( M e. ZZ -> -. Z e. Fin )

Proof

Step	Hyp	Ref	Expression
1		uzinf.1	|- Z = ( ZZ>= ` M )
2		ominf	|- -. _om e. Fin
3	1	uzenom	|- ( M e. ZZ -> Z ~~ _om )
4		enfi	|- ( Z ~~ _om -> ( Z e. Fin <-> _om e. Fin ) )
5	3 4	syl	|- ( M e. ZZ -> ( Z e. Fin <-> _om e. Fin ) )
6	2 5	mtbiri	|- ( M e. ZZ -> -. Z e. Fin )