Theorem uztrn2

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

	Ref	Expression
Hypothesis	uztrn2.1	|- Z = ( ZZ>= ` K )
Assertion	uztrn2	|- ( ( N e. Z /\ M e. ( ZZ>= ` N ) ) -> M e. Z )

Proof

Step	Hyp	Ref	Expression
1		uztrn2.1	|- Z = ( ZZ>= ` K )
2	1	eleq2i	|- ( N e. Z <-> N e. ( ZZ>= ` K ) )
3		uztrn	|- ( ( M e. ( ZZ>= ` N ) /\ N e. ( ZZ>= ` K ) ) -> M e. ( ZZ>= ` K ) )
4	3	ancoms	|- ( ( N e. ( ZZ>= ` K ) /\ M e. ( ZZ>= ` N ) ) -> M e. ( ZZ>= ` K ) )
5	2 4	sylanb	|- ( ( N e. Z /\ M e. ( ZZ>= ` N ) ) -> M e. ( ZZ>= ` K ) )
6	5 1	eleqtrrdi	|- ( ( N e. Z /\ M e. ( ZZ>= ` N ) ) -> M e. Z )