| Step | Hyp | Ref
| Expression |
| 1 | | infxrgelbrnmpt.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 2 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 3 | | infxrgelbrnmpt.b |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
| 4 | 1, 2, 3 | rnmptssd 45201 |
. . 3
⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆
ℝ*) |
| 5 | | infxrgelbrnmpt.c |
. . 3
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
| 6 | | infxrgelb 13377 |
. . 3
⊢ ((ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ* ∧ 𝐶 ∈ ℝ*)
→ (𝐶 ≤ inf(ran
(𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ↔
∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧)) |
| 7 | 4, 5, 6 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐶 ≤ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ↔
∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧)) |
| 8 | | nfmpt1 5250 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 9 | 8 | nfrn 5963 |
. . . . . 6
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 10 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑥 𝐶 ≤ 𝑧 |
| 11 | 9, 10 | nfralw 3311 |
. . . . 5
⊢
Ⅎ𝑥∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧 |
| 12 | 1, 11 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) |
| 13 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 14 | 2 | elrnmpt1 5971 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ*) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 15 | 13, 3, 14 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 16 | 15 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 17 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) |
| 18 | | breq2 5147 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (𝐶 ≤ 𝑧 ↔ 𝐶 ≤ 𝐵)) |
| 19 | 18 | rspcva 3620 |
. . . . . 6
⊢ ((𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) → 𝐶 ≤ 𝐵) |
| 20 | 16, 17, 19 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) ∧ 𝑥 ∈ 𝐴) → 𝐶 ≤ 𝐵) |
| 21 | 20 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) → (𝑥 ∈ 𝐴 → 𝐶 ≤ 𝐵)) |
| 22 | 12, 21 | ralrimi 3257 |
. . 3
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) → ∀𝑥 ∈ 𝐴 𝐶 ≤ 𝐵) |
| 23 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
| 24 | 2 | elrnmpt 5969 |
. . . . . . . . 9
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
| 25 | 23, 24 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
| 26 | 25 | biimpi 216 |
. . . . . . 7
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
| 27 | 26 | adantl 481 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 𝐶 ≤ 𝐵 ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
| 28 | | nfra1 3284 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 |
| 29 | | rspa 3248 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 𝐶 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≤ 𝐵) |
| 30 | 18 | biimprcd 250 |
. . . . . . . . . 10
⊢ (𝐶 ≤ 𝐵 → (𝑧 = 𝐵 → 𝐶 ≤ 𝑧)) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝐶 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑧 = 𝐵 → 𝐶 ≤ 𝑧)) |
| 32 | 31 | ex 412 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝐶 ≤ 𝐵 → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝐶 ≤ 𝑧))) |
| 33 | 28, 10, 32 | rexlimd 3266 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝐶 ≤ 𝐵 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝐶 ≤ 𝑧)) |
| 34 | 33 | adantr 480 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 𝐶 ≤ 𝐵 ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝐶 ≤ 𝑧)) |
| 35 | 27, 34 | mpd 15 |
. . . . 5
⊢
((∀𝑥 ∈
𝐴 𝐶 ≤ 𝐵 ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝐶 ≤ 𝑧) |
| 36 | 35 | ralrimiva 3146 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 𝐶 ≤ 𝐵 → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) |
| 37 | 36 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐶 ≤ 𝐵) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧) |
| 38 | 22, 37 | impbida 801 |
. 2
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ≤ 𝑧 ↔ ∀𝑥 ∈ 𝐴 𝐶 ≤ 𝐵)) |
| 39 | 7, 38 | bitrd 279 |
1
⊢ (𝜑 → (𝐶 ≤ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ↔
∀𝑥 ∈ 𝐴 𝐶 ≤ 𝐵)) |