Metamath Proof Explorer

Theorem nnuzdisj

Description: The first N elements of the set of nonnegative integers are distinct from any later members. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Assertion nnuzdisj 
|- ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)

Proof

Step Hyp Ref Expression
1 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
2 ssrin 
 |-  ( ( 1 ... N ) C_ ( 0 ... N ) -> ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) C_ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
3 1 2 ax-mp 
 |-  ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) C_ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) )
4 nn0disj 
 |-  ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)
5 sseq0 
 |-  ( ( ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) C_ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) -> ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) )
6 3 4 5 mp2an 
 |-  ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)