Metamath Proof Explorer

Theorem infxrss

Description: Larger sets of extended reals have smaller infima. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 13-Sep-2020)

Ref Expression
Assertion infxrss ⊢ A ⊆ B ∧ B ⊆ ℝ * → inf B ℝ * < ≤ inf A ℝ * <

Proof

Step Hyp Ref Expression
1 simplr ⊢ A ⊆ B ∧ B ⊆ ℝ * ∧ x ∈ A → B ⊆ ℝ *
2 simpl ⊢ A ⊆ B ∧ B ⊆ ℝ * → A ⊆ B
3 2 sselda ⊢ A ⊆ B ∧ B ⊆ ℝ * ∧ x ∈ A → x ∈ B
4 infxrlb ⊢ B ⊆ ℝ * ∧ x ∈ B → inf B ℝ * < ≤ x
5 1 3 4 syl2anc ⊢ A ⊆ B ∧ B ⊆ ℝ * ∧ x ∈ A → inf B ℝ * < ≤ x
6 5 ralrimiva ⊢ A ⊆ B ∧ B ⊆ ℝ * → ∀ x ∈ A inf B ℝ * < ≤ x
7 sstr ⊢ A ⊆ B ∧ B ⊆ ℝ * → A ⊆ ℝ *
8 infxrcl ⊢ B ⊆ ℝ * → inf B ℝ * < ∈ ℝ *
9 8 adantl ⊢ A ⊆ B ∧ B ⊆ ℝ * → inf B ℝ * < ∈ ℝ *
10 infxrgelb ⊢ A ⊆ ℝ * ∧ inf B ℝ * < ∈ ℝ * → inf B ℝ * < ≤ inf A ℝ * < ↔ ∀ x ∈ A inf B ℝ * < ≤ x
11 7 9 10 syl2anc ⊢ A ⊆ B ∧ B ⊆ ℝ * → inf B ℝ * < ≤ inf A ℝ * < ↔ ∀ x ∈ A inf B ℝ * < ≤ x
12 6 11 mpbird ⊢ A ⊆ B ∧ B ⊆ ℝ * → inf B ℝ * < ≤ inf A ℝ * <