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

Metamath Proof Explorer

Theorem infxrlb

Description: A member of a set of extended reals is greater than or equal to the set's infimum. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

		Ref	Expression
	Assertion	infxrlb	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		infxrcl	⊢ ( 𝐴 ⊆ ℝ^* → inf ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
2	1	adantr	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
3		ssel2	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ℝ^* )
4		xrltso	⊢ < Or ℝ^*
5	4	a1i	⊢ ( 𝐴 ⊆ ℝ^* → < Or ℝ^* )
6		xrinfmss	⊢ ( 𝐴 ⊆ ℝ^* → ∃ 𝑥 ∈ ℝ^* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ^* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
7	5 6	inflb	⊢ ( 𝐴 ⊆ ℝ^* → ( 𝐵 ∈ 𝐴 → ¬ 𝐵 < inf ( 𝐴 , ℝ^* , < ) ) )
8	7	imp	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 < inf ( 𝐴 , ℝ^* , < ) )
9	2 3 8	xrnltled	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ≤ 𝐵 )