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