Theorem uztrn2

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

	Ref	Expression
Hypothesis	uztrn2.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝐾 )
Assertion	uztrn2	⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		uztrn2.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝐾 )
2	1	eleq2i	⊢ ( 𝑁 ∈ 𝑍 ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
3		uztrn	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) )
4	3	ancoms	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) )
5	2 4	sylanb	⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) )
6	5 1	eleqtrrdi	⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ 𝑍 )