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

Metamath Proof Explorer

Theorem infxrgelb

Description: The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

		Ref	Expression
	Assertion	infxrgelb	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ^* , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		xrltso	⊢ < Or ℝ^*
2	1	a1i	⊢ ( 𝐴 ⊆ ℝ^* → < Or ℝ^* )
3		xrinfmss	⊢ ( 𝐴 ⊆ ℝ^* → ∃ 𝑧 ∈ ℝ^* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑧 ∧ ∀ 𝑦 ∈ ℝ^* ( 𝑧 < 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑥 < 𝑦 ) ) )
4		id	⊢ ( 𝐴 ⊆ ℝ^* → 𝐴 ⊆ ℝ^* )
5	2 3 4	infglbb	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( inf ( 𝐴 , ℝ^* , < ) < 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) )
6	5	notbid	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ¬ inf ( 𝐴 , ℝ^* , < ) < 𝐵 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) )
7		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 )
8	6 7	bitr4di	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ¬ inf ( 𝐴 , ℝ^* , < ) < 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ) )
9		id	⊢ ( 𝐵 ∈ ℝ^* → 𝐵 ∈ ℝ^* )
10		infxrcl	⊢ ( 𝐴 ⊆ ℝ^* → inf ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
11		xrlenlt	⊢ ( ( 𝐵 ∈ ℝ^* ∧ inf ( 𝐴 , ℝ^* , < ) ∈ ℝ^* ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ^* , < ) ↔ ¬ inf ( 𝐴 , ℝ^* , < ) < 𝐵 ) )
12	9 10 11	syl2anr	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ^* , < ) ↔ ¬ inf ( 𝐴 , ℝ^* , < ) < 𝐵 ) )
13		simplr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ^* )
14		simpl	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → 𝐴 ⊆ ℝ^* )
15	14	sselda	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ^* )
16	13 15	xrlenltd	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐵 ) )
17	16	ralbidva	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ) )
18	8 12 17	3bitr4d	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ^* , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ) )