uzss

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

		Ref	Expression
	Assertion	uzss	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$

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

Metamath Proof Explorer