# 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}\in {ℤ}_{\ge {M}}\to {ℤ}_{\ge {N}}\subseteq {ℤ}_{\ge {M}}$

### Proof

Step Hyp Ref Expression
1 eluzle ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\le {N}$
2 1 adantr ${⊢}\left({N}\in {ℤ}_{\ge {M}}\wedge {k}\in ℤ\right)\to {M}\le {N}$
3 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
4 eluzelz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℤ$
5 3 4 jca ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
6 zletr ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {k}\in ℤ\right)\to \left(\left({M}\le {N}\wedge {N}\le {k}\right)\to {M}\le {k}\right)$
7 6 3expa ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {k}\in ℤ\right)\to \left(\left({M}\le {N}\wedge {N}\le {k}\right)\to {M}\le {k}\right)$
8 5 7 sylan ${⊢}\left({N}\in {ℤ}_{\ge {M}}\wedge {k}\in ℤ\right)\to \left(\left({M}\le {N}\wedge {N}\le {k}\right)\to {M}\le {k}\right)$
9 2 8 mpand ${⊢}\left({N}\in {ℤ}_{\ge {M}}\wedge {k}\in ℤ\right)\to \left({N}\le {k}\to {M}\le {k}\right)$
10 9 imdistanda ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(\left({k}\in ℤ\wedge {N}\le {k}\right)\to \left({k}\in ℤ\wedge {M}\le {k}\right)\right)$
11 eluz1 ${⊢}{N}\in ℤ\to \left({k}\in {ℤ}_{\ge {N}}↔\left({k}\in ℤ\wedge {N}\le {k}\right)\right)$
12 4 11 syl ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({k}\in {ℤ}_{\ge {N}}↔\left({k}\in ℤ\wedge {N}\le {k}\right)\right)$
13 eluz1 ${⊢}{M}\in ℤ\to \left({k}\in {ℤ}_{\ge {M}}↔\left({k}\in ℤ\wedge {M}\le {k}\right)\right)$
14 3 13 syl ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({k}\in {ℤ}_{\ge {M}}↔\left({k}\in ℤ\wedge {M}\le {k}\right)\right)$
15 10 12 14 3imtr4d ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({k}\in {ℤ}_{\ge {N}}\to {k}\in {ℤ}_{\ge {M}}\right)$
16 15 ssrdv ${⊢}{N}\in {ℤ}_{\ge {M}}\to {ℤ}_{\ge {N}}\subseteq {ℤ}_{\ge {M}}$