| Step | Hyp | Ref
| Expression |
| 1 | | infrecl 12250 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈
ℝ) |
| 2 | 1 | recnd 11289 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈
ℂ) |
| 3 | 2 | negnegd 11611 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → --inf(𝐴, ℝ, < ) = inf(𝐴, ℝ, < )) |
| 4 | | negeq 11500 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → -𝑤 = -𝑧) |
| 5 | 4 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑤 ∈ ℝ ↦ -𝑤) = (𝑧 ∈ ℝ ↦ -𝑧) |
| 6 | 5 | mptpreima 6258 |
. . . . . . 7
⊢ (◡(𝑤 ∈ ℝ ↦ -𝑤) “ 𝐴) = {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} |
| 7 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℝ ↦ -𝑤) = (𝑤 ∈ ℝ ↦ -𝑤) |
| 8 | 7 | negiso 12248 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ ↦ -𝑤) Isom < , ◡ < (ℝ, ℝ) ∧ ◡(𝑤 ∈ ℝ ↦ -𝑤) = (𝑤 ∈ ℝ ↦ -𝑤)) |
| 9 | 8 | simpri 485 |
. . . . . . . 8
⊢ ◡(𝑤 ∈ ℝ ↦ -𝑤) = (𝑤 ∈ ℝ ↦ -𝑤) |
| 10 | 9 | imaeq1i 6075 |
. . . . . . 7
⊢ (◡(𝑤 ∈ ℝ ↦ -𝑤) “ 𝐴) = ((𝑤 ∈ ℝ ↦ -𝑤) “ 𝐴) |
| 11 | 6, 10 | eqtr3i 2767 |
. . . . . 6
⊢ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = ((𝑤 ∈ ℝ ↦ -𝑤) “ 𝐴) |
| 12 | 11 | supeq1i 9487 |
. . . . 5
⊢
sup({𝑧 ∈
ℝ ∣ -𝑧 ∈
𝐴}, ℝ, < ) =
sup(((𝑤 ∈ ℝ
↦ -𝑤) “ 𝐴), ℝ, <
) |
| 13 | 8 | simpli 483 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℝ ↦ -𝑤) Isom < , ◡ < (ℝ, ℝ) |
| 14 | | isocnv 7350 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ ↦ -𝑤) Isom < , ◡ < (ℝ, ℝ) → ◡(𝑤 ∈ ℝ ↦ -𝑤) Isom ◡ < , < (ℝ,
ℝ)) |
| 15 | 13, 14 | ax-mp 5 |
. . . . . . . 8
⊢ ◡(𝑤 ∈ ℝ ↦ -𝑤) Isom ◡ < , < (ℝ,
ℝ) |
| 16 | | isoeq1 7337 |
. . . . . . . . 9
⊢ (◡(𝑤 ∈ ℝ ↦ -𝑤) = (𝑤 ∈ ℝ ↦ -𝑤) → (◡(𝑤 ∈ ℝ ↦ -𝑤) Isom ◡ < , < (ℝ, ℝ) ↔
(𝑤 ∈ ℝ ↦
-𝑤) Isom ◡ < , < (ℝ,
ℝ))) |
| 17 | 9, 16 | ax-mp 5 |
. . . . . . . 8
⊢ (◡(𝑤 ∈ ℝ ↦ -𝑤) Isom ◡ < , < (ℝ, ℝ) ↔
(𝑤 ∈ ℝ ↦
-𝑤) Isom ◡ < , < (ℝ,
ℝ)) |
| 18 | 15, 17 | mpbi 230 |
. . . . . . 7
⊢ (𝑤 ∈ ℝ ↦ -𝑤) Isom ◡ < , < (ℝ,
ℝ) |
| 19 | 18 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (𝑤 ∈ ℝ ↦ -𝑤) Isom ◡ < , < (ℝ,
ℝ)) |
| 20 | | simp1 1137 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → 𝐴 ⊆ ℝ) |
| 21 | | infm3 12227 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
| 22 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
| 23 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
| 24 | 22, 23 | brcnv 5893 |
. . . . . . . . . . 11
⊢ (𝑥◡ < 𝑦 ↔ 𝑦 < 𝑥) |
| 25 | 24 | notbii 320 |
. . . . . . . . . 10
⊢ (¬
𝑥◡ < 𝑦 ↔ ¬ 𝑦 < 𝑥) |
| 26 | 25 | ralbii 3093 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝐴 ¬ 𝑥◡
< 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥) |
| 27 | 23, 22 | brcnv 5893 |
. . . . . . . . . . 11
⊢ (𝑦◡ < 𝑥 ↔ 𝑥 < 𝑦) |
| 28 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
| 29 | 23, 28 | brcnv 5893 |
. . . . . . . . . . . 12
⊢ (𝑦◡ < 𝑧 ↔ 𝑧 < 𝑦) |
| 30 | 29 | rexbii 3094 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
𝐴 𝑦◡
< 𝑧 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) |
| 31 | 27, 30 | imbi12i 350 |
. . . . . . . . . 10
⊢ ((𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
| 32 | 31 | ralbii 3093 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧) ↔
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
| 33 | 26, 32 | anbi12i 628 |
. . . . . . . 8
⊢
((∀𝑦 ∈
𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧)) ↔
(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
| 34 | 33 | rexbii 3094 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℝ (∀𝑦 ∈
𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧)) ↔
∃𝑥 ∈ ℝ
(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
| 35 | 21, 34 | sylibr 234 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧))) |
| 36 | | gtso 11342 |
. . . . . . 7
⊢ ◡ < Or ℝ |
| 37 | 36 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ◡ < Or ℝ) |
| 38 | 19, 20, 35, 37 | supiso 9515 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → sup(((𝑤 ∈ ℝ ↦ -𝑤) “ 𝐴), ℝ, < ) = ((𝑤 ∈ ℝ ↦ -𝑤)‘sup(𝐴, ℝ, ◡ < ))) |
| 39 | 12, 38 | eqtrid 2789 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) = ((𝑤 ∈ ℝ ↦ -𝑤)‘sup(𝐴, ℝ, ◡ < ))) |
| 40 | | df-inf 9483 |
. . . . . . . 8
⊢ inf(𝐴, ℝ, < ) = sup(𝐴, ℝ, ◡ < ) |
| 41 | 40 | eqcomi 2746 |
. . . . . . 7
⊢ sup(𝐴, ℝ, ◡ < ) = inf(𝐴, ℝ, < ) |
| 42 | 41 | fveq2i 6909 |
. . . . . 6
⊢ ((𝑤 ∈ ℝ ↦ -𝑤)‘sup(𝐴, ℝ, ◡ < )) = ((𝑤 ∈ ℝ ↦ -𝑤)‘inf(𝐴, ℝ, < )) |
| 43 | | negeq 11500 |
. . . . . . 7
⊢ (𝑤 = inf(𝐴, ℝ, < ) → -𝑤 = -inf(𝐴, ℝ, < )) |
| 44 | | negex 11506 |
. . . . . . 7
⊢
-inf(𝐴, ℝ,
< ) ∈ V |
| 45 | 43, 7, 44 | fvmpt 7016 |
. . . . . 6
⊢
(inf(𝐴, ℝ,
< ) ∈ ℝ → ((𝑤 ∈ ℝ ↦ -𝑤)‘inf(𝐴, ℝ, < )) = -inf(𝐴, ℝ, < )) |
| 46 | 42, 45 | eqtrid 2789 |
. . . . 5
⊢
(inf(𝐴, ℝ,
< ) ∈ ℝ → ((𝑤 ∈ ℝ ↦ -𝑤)‘sup(𝐴, ℝ, ◡ < )) = -inf(𝐴, ℝ, < )) |
| 47 | 1, 46 | syl 17 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ((𝑤 ∈ ℝ ↦ -𝑤)‘sup(𝐴, ℝ, ◡ < )) = -inf(𝐴, ℝ, < )) |
| 48 | 39, 47 | eqtr2d 2778 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -inf(𝐴, ℝ, < ) = sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < )) |
| 49 | 48 | negeqd 11502 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → --inf(𝐴, ℝ, < ) = -sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < )) |
| 50 | 3, 49 | eqtr3d 2779 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) = -sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < )) |