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

Metamath Proof Explorer

Theorem infxrbnd2

Description: The infimum of a bounded-below set of extended reals is greater than minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Assertion	infxrbnd2	⊢ ( 𝐴 ⊆ ℝ^* → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ -∞ < inf ( 𝐴 , ℝ^* , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralnex	⊢ ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
2		ssel2	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ^* )
3		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ^* )
4		simpl	⊢ ( ( 𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → 𝑦 ∈ ℝ^* )
5		simpr	⊢ ( ( 𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → 𝑥 ∈ ℝ^* )
6	4 5	xrltnled	⊢ ( ( 𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( 𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
7	2 3 6	syl2an	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
8	7	an32s	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
9	8	rexbidva	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 ≤ 𝑦 ) )
10		rexnal	⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 ≤ 𝑦 ↔ ¬ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
11	9 10	bitr2di	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) → ( ¬ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
12	11	ralbidva	⊢ ( 𝐴 ⊆ ℝ^* → ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
13	1 12	bitr3id	⊢ ( 𝐴 ⊆ ℝ^* → ( ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
14		infxrunb2	⊢ ( 𝐴 ⊆ ℝ^* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf ( 𝐴 , ℝ^* , < ) = -∞ ) )
15		infxrcl	⊢ ( 𝐴 ⊆ ℝ^* → inf ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
16		ngtmnft	⊢ ( inf ( 𝐴 , ℝ^* , < ) ∈ ℝ^* → ( inf ( 𝐴 , ℝ^* , < ) = -∞ ↔ ¬ -∞ < inf ( 𝐴 , ℝ^* , < ) ) )
17	15 16	syl	⊢ ( 𝐴 ⊆ ℝ^* → ( inf ( 𝐴 , ℝ^* , < ) = -∞ ↔ ¬ -∞ < inf ( 𝐴 , ℝ^* , < ) ) )
18	13 14 17	3bitrd	⊢ ( 𝐴 ⊆ ℝ^* → ( ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ¬ -∞ < inf ( 𝐴 , ℝ^* , < ) ) )
19	18	con4bid	⊢ ( 𝐴 ⊆ ℝ^* → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ -∞ < inf ( 𝐴 , ℝ^* , < ) ) )