Step |
Hyp |
Ref |
Expression |
1 |
|
xrsupssd.1 |
⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 ) |
2 |
|
xrsupssd.2 |
⊢ ( 𝜑 → 𝐶 ⊆ ℝ* ) |
3 |
|
xrltso |
⊢ < Or ℝ* |
4 |
3
|
a1i |
⊢ ( 𝜑 → < Or ℝ* ) |
5 |
1 2
|
sstrd |
⊢ ( 𝜑 → 𝐵 ⊆ ℝ* ) |
6 |
|
xrsupss |
⊢ ( 𝐵 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ) ) |
7 |
5 6
|
syl |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ) ) |
8 |
|
xrsupss |
⊢ ( 𝐶 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 < 𝑧 ) ) ) |
9 |
2 8
|
syl |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 < 𝑧 ) ) ) |
10 |
4 1 2 7 9
|
supssd |
⊢ ( 𝜑 → ¬ sup ( 𝐶 , ℝ* , < ) < sup ( 𝐵 , ℝ* , < ) ) |
11 |
4 7
|
supcl |
⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) ∈ ℝ* ) |
12 |
4 9
|
supcl |
⊢ ( 𝜑 → sup ( 𝐶 , ℝ* , < ) ∈ ℝ* ) |
13 |
|
xrlenlt |
⊢ ( ( sup ( 𝐵 , ℝ* , < ) ∈ ℝ* ∧ sup ( 𝐶 , ℝ* , < ) ∈ ℝ* ) → ( sup ( 𝐵 , ℝ* , < ) ≤ sup ( 𝐶 , ℝ* , < ) ↔ ¬ sup ( 𝐶 , ℝ* , < ) < sup ( 𝐵 , ℝ* , < ) ) ) |
14 |
11 12 13
|
syl2anc |
⊢ ( 𝜑 → ( sup ( 𝐵 , ℝ* , < ) ≤ sup ( 𝐶 , ℝ* , < ) ↔ ¬ sup ( 𝐶 , ℝ* , < ) < sup ( 𝐵 , ℝ* , < ) ) ) |
15 |
10 14
|
mpbird |
⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) ≤ sup ( 𝐶 , ℝ* , < ) ) |