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

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 ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) → inf ( 𝐵 , ℝ* , < ) ≤ inf ( 𝐴 , ℝ* , < ) )

Proof

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