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