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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	uzid3	⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		uzid3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2	1	eleq2i	⊢ ( 𝑁 ∈ 𝑍 ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3	2	biimpi	⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4		uzid2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
5	3 4	syl	⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )