Step |
Hyp |
Ref |
Expression |
1 |
|
ssel |
⊢ ( 𝐴 ⊆ ℝ → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ ) ) |
2 |
|
leloe |
⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) |
3 |
2
|
expcom |
⊢ ( 𝑥 ∈ ℝ → ( 𝑦 ∈ ℝ → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) ) |
4 |
1 3
|
syl9 |
⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ ℝ → ( 𝑦 ∈ 𝐴 → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) ) ) |
5 |
4
|
imp31 |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) |
6 |
5
|
ralbidva |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) |
7 |
6
|
rexbidva |
⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) |
8 |
7
|
anbi2d |
⊢ ( 𝐴 ⊆ ℝ → ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ↔ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) ) |
9 |
8
|
pm5.32i |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) ) |
10 |
|
3anass |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ↔ ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) ) |
11 |
|
3anass |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) ) |
12 |
9 10 11
|
3bitr4i |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ↔ ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) |
13 |
|
sup2 |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) |
14 |
12 13
|
sylbi |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) |