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=K
Assertion uztrn2 NZMNMZ

Proof

Step Hyp Ref Expression
1 uztrn2.1 Z=K
2 1 eleq2i NZNK
3 uztrn MNNKMK
4 3 ancoms NKMNMK
5 2 4 sylanb NZMNMK
6 5 1 eleqtrrdi NZMNMZ