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

Metamath Proof Explorer

Theorem infxrunb2

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

Ref Expression
Assertion infxrunb2 ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑥 𝐴 ⊆ ℝ*
2 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥
3 1 2 nfan ⊢ Ⅎ 𝑥 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 )
4 nfv ⊢ Ⅎ 𝑦 𝐴 ⊆ ℝ*
5 nfcv ⊢ Ⅎ 𝑦 ℝ
6 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥
7 5 6 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥
8 4 7 nfan ⊢ Ⅎ 𝑦 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 )
9 simpl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → 𝐴 ⊆ ℝ* )
10 mnfxr ⊢ -∞ ∈ ℝ*
11 10 a1i ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → -∞ ∈ ℝ* )
12 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
13 nltmnf ⊢ ( 𝑥 ∈ ℝ* → ¬ 𝑥 < -∞ )
14 12 13 syl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 < -∞ )
15 14 ralrimiva ⊢ ( 𝐴 ⊆ ℝ* → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < -∞ )
16 15 adantr ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < -∞ )
17 ralimralim ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 → ∀ 𝑥 ∈ ℝ ( -∞ < 𝑥 → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
18 17 adantl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → ∀ 𝑥 ∈ ℝ ( -∞ < 𝑥 → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
19 3 8 9 11 16 18 infxr ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → inf ( 𝐴 , ℝ* , < ) = -∞ )
20 19 ex ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 → inf ( 𝐴 , ℝ* , < ) = -∞ ) )
21 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
22 21 adantl ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ* )
23 simpl ⊢ ( ( inf ( 𝐴 , ℝ* , < ) = -∞ ∧ 𝑥 ∈ ℝ ) → inf ( 𝐴 , ℝ* , < ) = -∞ )
24 mnflt ⊢ ( 𝑥 ∈ ℝ → -∞ < 𝑥 )
25 24 adantl ⊢ ( ( inf ( 𝐴 , ℝ* , < ) = -∞ ∧ 𝑥 ∈ ℝ ) → -∞ < 𝑥 )
26 23 25 eqbrtrd ⊢ ( ( inf ( 𝐴 , ℝ* , < ) = -∞ ∧ 𝑥 ∈ ℝ ) → inf ( 𝐴 , ℝ* , < ) < 𝑥 )
27 26 adantll ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → inf ( 𝐴 , ℝ* , < ) < 𝑥 )
28 xrltso ⊢ < Or ℝ*
29 28 a1i ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → < Or ℝ* )
30 xrinfmss ⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑧 ∈ ℝ* ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ* ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ) )
31 30 ad2antrr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ* ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ* ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ) )
32 29 31 infglb ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) < 𝑥 ) → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
33 22 27 32 mp2and ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 )
34 33 ralrimiva ⊢ ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 )
35 34 ex ⊢ ( 𝐴 ⊆ ℝ* → ( inf ( 𝐴 , ℝ* , < ) = -∞ → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
36 20 35 impbid ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )