Metamath Proof Explorer

Theorem uzss

Description: Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005)

Ref Expression
Assertion uzss 
|- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )

Proof

Step Hyp Ref Expression
1 eluzle 
 |-  ( N e. ( ZZ>= ` M ) -> M <_ N )
2 1 adantr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ k e. ZZ ) -> M <_ N )
3 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
4 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
5 3 4 jca 
 |-  ( N e. ( ZZ>= ` M ) -> ( M e. ZZ /\ N e. ZZ ) )
6 zletr 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ k e. ZZ ) -> ( ( M <_ N /\ N <_ k ) -> M <_ k ) )
7 6 3expa 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ k e. ZZ ) -> ( ( M <_ N /\ N <_ k ) -> M <_ k ) )
8 5 7 sylan 
 |-  ( ( N e. ( ZZ>= ` M ) /\ k e. ZZ ) -> ( ( M <_ N /\ N <_ k ) -> M <_ k ) )
9 2 8 mpand 
 |-  ( ( N e. ( ZZ>= ` M ) /\ k e. ZZ ) -> ( N <_ k -> M <_ k ) )
10 9 imdistanda 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( k e. ZZ /\ N <_ k ) -> ( k e. ZZ /\ M <_ k ) ) )
11 eluz1 
 |-  ( N e. ZZ -> ( k e. ( ZZ>= ` N ) <-> ( k e. ZZ /\ N <_ k ) ) )
12 4 11 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( k e. ( ZZ>= ` N ) <-> ( k e. ZZ /\ N <_ k ) ) )
13 eluz1 
 |-  ( M e. ZZ -> ( k e. ( ZZ>= ` M ) <-> ( k e. ZZ /\ M <_ k ) ) )
14 3 13 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( k e. ( ZZ>= ` M ) <-> ( k e. ZZ /\ M <_ k ) ) )
15 10 12 14 3imtr4d 
 |-  ( N e. ( ZZ>= ` M ) -> ( k e. ( ZZ>= ` N ) -> k e. ( ZZ>= ` M ) ) )
16 15 ssrdv 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )