Description: Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | uztrn2.1 | |
|
Assertion | uztrn2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uztrn2.1 | |
|
2 | 1 | eleq2i | |
3 | uztrn | |
|
4 | 3 | ancoms | |
5 | 2 4 | sylanb | |
6 | 5 1 | eleqtrrdi | |