| Step | Hyp | Ref
| Expression |
| 1 | | supminfxrrnmpt.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 2 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 3 | | supminfxrrnmpt.b |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
| 4 | 1, 2, 3 | rnmptssd 45201 |
. . 3
⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆
ℝ*) |
| 5 | 4 | supminfxr2 45480 |
. 2
⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) =
-𝑒inf({𝑦
∈ ℝ* ∣ -𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)}, ℝ*, <
)) |
| 6 | | xnegex 13250 |
. . . . . . . . . . . 12
⊢
-𝑒𝑦 ∈ V |
| 7 | 2 | elrnmpt 5969 |
. . . . . . . . . . . 12
⊢
(-𝑒𝑦 ∈ V → (-𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 -𝑒𝑦 = 𝐵)) |
| 8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(-𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 -𝑒𝑦 = 𝐵) |
| 9 | 8 | biimpi 216 |
. . . . . . . . . 10
⊢
(-𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 -𝑒𝑦 = 𝐵) |
| 10 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 ↦ -𝑒𝐵) = (𝑥 ∈ 𝐴 ↦ -𝑒𝐵) |
| 11 | | xnegneg 13256 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ*
→ -𝑒-𝑒𝑦 = 𝑦) |
| 12 | 11 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ*
→ 𝑦 =
-𝑒-𝑒𝑦) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ*
∧ -𝑒𝑦 = 𝐵) → 𝑦 =
-𝑒-𝑒𝑦) |
| 14 | | xnegeq 13249 |
. . . . . . . . . . . . . . . 16
⊢
(-𝑒𝑦 = 𝐵 →
-𝑒-𝑒𝑦 = -𝑒𝐵) |
| 15 | 14 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ*
∧ -𝑒𝑦 = 𝐵) →
-𝑒-𝑒𝑦 = -𝑒𝐵) |
| 16 | 13, 15 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ*
∧ -𝑒𝑦 = 𝐵) → 𝑦 = -𝑒𝐵) |
| 17 | 16 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ (-𝑒𝑦 = 𝐵 → 𝑦 = -𝑒𝐵)) |
| 18 | 17 | reximdv 3170 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (∃𝑥 ∈
𝐴
-𝑒𝑦 =
𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = -𝑒𝐵)) |
| 19 | 18 | imp 406 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ*
∧ ∃𝑥 ∈ 𝐴 -𝑒𝑦 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 = -𝑒𝐵) |
| 20 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ*
∧ ∃𝑥 ∈ 𝐴 -𝑒𝑦 = 𝐵) → 𝑦 ∈ ℝ*) |
| 21 | 10, 19, 20 | elrnmptd 5974 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ*
∧ ∃𝑥 ∈ 𝐴 -𝑒𝑦 = 𝐵) → 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵)) |
| 22 | 9, 21 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ*
∧ -𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵)) |
| 23 | 22 | ex 412 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ*
→ (-𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵))) |
| 24 | 23 | rgen 3063 |
. . . . . . 7
⊢
∀𝑦 ∈
ℝ* (-𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵)) |
| 25 | | rabss 4072 |
. . . . . . . 8
⊢ ({𝑦 ∈ ℝ*
∣ -𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)} ⊆ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵) ↔ ∀𝑦 ∈ ℝ*
(-𝑒𝑦
∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵))) |
| 26 | 25 | biimpri 228 |
. . . . . . 7
⊢
(∀𝑦 ∈
ℝ* (-𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵)) → {𝑦 ∈ ℝ* ∣
-𝑒𝑦
∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)} ⊆ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵)) |
| 27 | 24, 26 | ax-mp 5 |
. . . . . 6
⊢ {𝑦 ∈ ℝ*
∣ -𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)} ⊆ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵) |
| 28 | 27 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑦 ∈ ℝ* ∣
-𝑒𝑦
∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)} ⊆ ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵)) |
| 29 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥-𝑒𝑦 |
| 30 | | nfmpt1 5250 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 31 | 30 | nfrn 5963 |
. . . . . . . 8
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 32 | 29, 31 | nfel 2920 |
. . . . . . 7
⊢
Ⅎ𝑥-𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 33 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥ℝ* |
| 34 | 32, 33 | nfrabw 3475 |
. . . . . 6
⊢
Ⅎ𝑥{𝑦 ∈ ℝ* ∣
-𝑒𝑦
∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)} |
| 35 | | xnegeq 13249 |
. . . . . . . 8
⊢ (𝑦 = -𝑒𝐵 →
-𝑒𝑦 =
-𝑒-𝑒𝐵) |
| 36 | 35 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑦 = -𝑒𝐵 →
(-𝑒𝑦
∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔
-𝑒-𝑒𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵))) |
| 37 | 3 | xnegcld 13342 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝑒𝐵 ∈
ℝ*) |
| 38 | | xnegneg 13256 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ -𝑒-𝑒𝐵 = 𝐵) |
| 39 | 3, 38 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) →
-𝑒-𝑒𝐵 = 𝐵) |
| 40 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 41 | 2, 40, 3 | elrnmpt1d 5975 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 42 | 39, 41 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) →
-𝑒-𝑒𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 43 | 36, 37, 42 | elrabd 3694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝑒𝐵 ∈ {𝑦 ∈ ℝ* ∣
-𝑒𝑦
∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)}) |
| 44 | 1, 34, 10, 43 | rnmptssdf 45261 |
. . . . 5
⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵) ⊆ {𝑦 ∈ ℝ* ∣
-𝑒𝑦
∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)}) |
| 45 | 28, 44 | eqssd 4001 |
. . . 4
⊢ (𝜑 → {𝑦 ∈ ℝ* ∣
-𝑒𝑦
∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)} = ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵)) |
| 46 | 45 | infeq1d 9517 |
. . 3
⊢ (𝜑 → inf({𝑦 ∈ ℝ* ∣
-𝑒𝑦
∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)}, ℝ*, < ) = inf(ran
(𝑥 ∈ 𝐴 ↦ -𝑒𝐵), ℝ*, <
)) |
| 47 | 46 | xnegeqd 45448 |
. 2
⊢ (𝜑 →
-𝑒inf({𝑦
∈ ℝ* ∣ -𝑒𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)}, ℝ*, < ) =
-𝑒inf(ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵), ℝ*, <
)) |
| 48 | 5, 47 | eqtrd 2777 |
1
⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) =
-𝑒inf(ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵), ℝ*, <
)) |