Step |
Hyp |
Ref |
Expression |
1 |
|
suprubrnmpt2.x |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
suprubrnmpt2.b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ ) |
3 |
|
suprubrnmpt2.l |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) |
4 |
|
suprubrnmpt2.c |
⊢ ( 𝜑 → 𝐶 ∈ 𝐴 ) |
5 |
|
suprubrnmpt2.d |
⊢ ( 𝜑 → 𝐷 ∈ ℝ ) |
6 |
|
suprubrnmpt2.i |
⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐷 ) |
7 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
8 |
1 7 2
|
rnmptssd |
⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ) |
9 |
7 6
|
elrnmpt1s |
⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ ℝ ) → 𝐷 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) |
10 |
4 5 9
|
syl2anc |
⊢ ( 𝜑 → 𝐷 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) |
11 |
10
|
ne0d |
⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ ) |
12 |
1 3
|
rnmptbdd |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑦 ) |
13 |
8 11 12 10
|
suprubd |
⊢ ( 𝜑 → 𝐷 ≤ sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) ) |