Theorem uzid3

Description: Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		uzid3.1	|- Z = ( ZZ>= ` M )
2	1	eleq2i	|- ( N e. Z <-> N e. ( ZZ>= ` M ) )
3	2	biimpi	|- ( N e. Z -> N e. ( ZZ>= ` M ) )
4		uzid2	|- ( N e. ( ZZ>= ` M ) -> N e. ( ZZ>= ` N ) )
5	3 4	syl	|- ( N e. Z -> N e. ( ZZ>= ` N ) )