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 ( 𝐴 , ℝ* , < ) )