This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uztrn2

Description: Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013)

		Ref	Expression
	Hypothesis	uztrn2.1	$⊢ Z = ℤ_{\geq K}$
	Assertion	uztrn2	$⊢ (N \in Z \land M \in ℤ_{\geq N}) \to M \in Z$

Step	Hyp	Ref	Expression
1		uztrn2.1	$⊢ Z = ℤ_{\geq K}$
2	1	eleq2i	$⊢ N \in Z \leftrightarrow N \in ℤ_{\geq K}$
3		uztrn	$⊢ (M \in ℤ_{\geq N} \land N \in ℤ_{\geq K}) \to M \in ℤ_{\geq K}$
4	3	ancoms	$⊢ (N \in ℤ_{\geq K} \land M \in ℤ_{\geq N}) \to M \in ℤ_{\geq K}$
5	2 4	sylanb	$⊢ (N \in Z \land M \in ℤ_{\geq N}) \to M \in ℤ_{\geq K}$
6	5 1	eleqtrrdi	$⊢ (N \in Z \land M \in ℤ_{\geq N}) \to M \in Z$