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