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

Metamath Proof Explorer

Theorem uzssd2

Description: Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses uzssd2.1 ⊢ Z = ℤ ≥ M
uzssd2.2 ⊢ φ → N ∈ Z
Assertion uzssd2 ⊢ φ → ℤ ≥ N ⊆ Z

Proof

Step Hyp Ref Expression
1 uzssd2.1 ⊢ Z = ℤ ≥ M
2 uzssd2.2 ⊢ φ → N ∈ Z
3 2 1 eleqtrdi ⊢ φ → N ∈ ℤ ≥ M
4 3 uzssd ⊢ φ → ℤ ≥ N ⊆ ℤ ≥ M
5 4 1 sseqtrrdi ⊢ φ → ℤ ≥ N ⊆ Z