Step | Hyp | Ref
| Expression |
1 | | supxrleubrnmpt.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
2 | | eqid 2739 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
3 | | supxrleubrnmpt.b |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
4 | 1, 2, 3 | rnmptssd 42742 |
. . 3
⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆
ℝ*) |
5 | | supxrleubrnmpt.c |
. . 3
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
6 | | supxrleub 13069 |
. . 3
⊢ ((ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ* ∧ 𝐶 ∈ ℝ*)
→ (sup(ran (𝑥 ∈
𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐶 ↔ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶)) |
7 | 4, 5, 6 | syl2anc 584 |
. 2
⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐶 ↔ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶)) |
8 | | nfmpt1 5183 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
9 | 8 | nfrn 5864 |
. . . . . . 7
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
10 | | nfv 1918 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑧 ≤ 𝐶 |
11 | 9, 10 | nfralw 3152 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶 |
12 | 1, 11 | nfan 1903 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶) |
13 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
14 | 2 | elrnmpt1 5870 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ*) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
15 | 13, 3, 14 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
16 | 15 | adantlr 712 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
17 | | simplr 766 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶) |
18 | | breq1 5078 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝑧 ≤ 𝐶 ↔ 𝐵 ≤ 𝐶)) |
19 | 18 | rspcva 3560 |
. . . . . . 7
⊢ ((𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶) → 𝐵 ≤ 𝐶) |
20 | 16, 17, 19 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
21 | 20 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶) → (𝑥 ∈ 𝐴 → 𝐵 ≤ 𝐶)) |
22 | 12, 21 | ralrimi 3142 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶) → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶) |
23 | 22 | ex 413 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) |
24 | | vex 3437 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
25 | 2 | elrnmpt 5868 |
. . . . . . . . 9
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
27 | 26 | biimpi 215 |
. . . . . . 7
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
28 | 27 | adantl 482 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝐶 ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
29 | | nfra1 3145 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 |
30 | | rspa 3133 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝐶 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
31 | 18 | biimprcd 249 |
. . . . . . . . . 10
⊢ (𝐵 ≤ 𝐶 → (𝑧 = 𝐵 → 𝑧 ≤ 𝐶)) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑧 = 𝐵 → 𝑧 ≤ 𝐶)) |
33 | 32 | ex 413 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝐵 ≤ 𝐶 → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑧 ≤ 𝐶))) |
34 | 29, 10, 33 | rexlimd 3251 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝐵 ≤ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝐶)) |
35 | 34 | adantr 481 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝐶 ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝐶)) |
36 | 28, 35 | mpd 15 |
. . . . 5
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝐶 ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑧 ≤ 𝐶) |
37 | 36 | ralrimiva 3104 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 ≤ 𝐶 → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶) |
38 | 37 | a1i 11 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶)) |
39 | 23, 38 | impbid 211 |
. 2
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) |
40 | 7, 39 | bitrd 278 |
1
⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) |