Step |
Hyp |
Ref |
Expression |
1 |
|
rnmptbdd.x |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
rnmptbdd.b |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) |
3 |
|
breq2 |
⊢ ( 𝑦 = 𝑣 → ( 𝐵 ≤ 𝑦 ↔ 𝐵 ≤ 𝑣 ) ) |
4 |
3
|
ralbidv |
⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑣 ) ) |
5 |
4
|
cbvrexvw |
⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑣 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑣 ) |
6 |
2 5
|
sylib |
⊢ ( 𝜑 → ∃ 𝑣 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑣 ) |
7 |
1 6
|
rnmptbddlem |
⊢ ( 𝜑 → ∃ 𝑣 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑣 ) |
8 |
|
breq2 |
⊢ ( 𝑣 = 𝑦 → ( 𝑤 ≤ 𝑣 ↔ 𝑤 ≤ 𝑦 ) ) |
9 |
8
|
ralbidv |
⊢ ( 𝑣 = 𝑦 → ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑣 ↔ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑦 ) ) |
10 |
|
breq1 |
⊢ ( 𝑤 = 𝑧 → ( 𝑤 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦 ) ) |
11 |
10
|
cbvralvw |
⊢ ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑦 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) |
12 |
9 11
|
bitrdi |
⊢ ( 𝑣 = 𝑦 → ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑣 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ) |
13 |
12
|
cbvrexvw |
⊢ ( ∃ 𝑣 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑣 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) |
14 |
7 13
|
sylib |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) |