Step |
Hyp |
Ref |
Expression |
1 |
|
infrecl |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) ∈ ℝ ) |
2 |
1
|
recnd |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) ∈ ℂ ) |
3 |
2
|
negnegd |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → - - inf ( 𝐴 , ℝ , < ) = inf ( 𝐴 , ℝ , < ) ) |
4 |
|
negeq |
⊢ ( 𝑤 = 𝑧 → - 𝑤 = - 𝑧 ) |
5 |
4
|
cbvmptv |
⊢ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑧 ∈ ℝ ↦ - 𝑧 ) |
6 |
5
|
mptpreima |
⊢ ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) = { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } |
7 |
|
eqid |
⊢ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 ) |
8 |
7
|
negiso |
⊢ ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , ◡ < ( ℝ , ℝ ) ∧ ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ) |
9 |
8
|
simpri |
⊢ ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 ) |
10 |
9
|
imaeq1i |
⊢ ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) |
11 |
6 10
|
eqtr3i |
⊢ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) |
12 |
11
|
supeq1i |
⊢ sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) = sup ( ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) , ℝ , < ) |
13 |
8
|
simpli |
⊢ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , ◡ < ( ℝ , ℝ ) |
14 |
|
isocnv |
⊢ ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , ◡ < ( ℝ , ℝ ) → ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) ) |
15 |
13 14
|
ax-mp |
⊢ ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) |
16 |
|
isoeq1 |
⊢ ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 ) → ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) ↔ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) ) ) |
17 |
9 16
|
ax-mp |
⊢ ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) ↔ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) ) |
18 |
15 17
|
mpbi |
⊢ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) |
19 |
18
|
a1i |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) ) |
20 |
|
simp1 |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → 𝐴 ⊆ ℝ ) |
21 |
|
infm3 |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) |
22 |
|
vex |
⊢ 𝑥 ∈ V |
23 |
|
vex |
⊢ 𝑦 ∈ V |
24 |
22 23
|
brcnv |
⊢ ( 𝑥 ◡ < 𝑦 ↔ 𝑦 < 𝑥 ) |
25 |
24
|
notbii |
⊢ ( ¬ 𝑥 ◡ < 𝑦 ↔ ¬ 𝑦 < 𝑥 ) |
26 |
25
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ) |
27 |
23 22
|
brcnv |
⊢ ( 𝑦 ◡ < 𝑥 ↔ 𝑥 < 𝑦 ) |
28 |
|
vex |
⊢ 𝑧 ∈ V |
29 |
23 28
|
brcnv |
⊢ ( 𝑦 ◡ < 𝑧 ↔ 𝑧 < 𝑦 ) |
30 |
29
|
rexbii |
⊢ ( ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) |
31 |
27 30
|
imbi12i |
⊢ ( ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) |
32 |
31
|
ralbii |
⊢ ( ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) |
33 |
26 32
|
anbi12i |
⊢ ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) |
34 |
33
|
rexbii |
⊢ ( ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) |
35 |
21 34
|
sylibr |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) ) |
36 |
|
gtso |
⊢ ◡ < Or ℝ |
37 |
36
|
a1i |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ◡ < Or ℝ ) |
38 |
19 20 35 37
|
supiso |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → sup ( ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) , ℝ , < ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) ) |
39 |
12 38
|
eqtrid |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) ) |
40 |
|
df-inf |
⊢ inf ( 𝐴 , ℝ , < ) = sup ( 𝐴 , ℝ , ◡ < ) |
41 |
40
|
eqcomi |
⊢ sup ( 𝐴 , ℝ , ◡ < ) = inf ( 𝐴 , ℝ , < ) |
42 |
41
|
fveq2i |
⊢ ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ inf ( 𝐴 , ℝ , < ) ) |
43 |
|
negeq |
⊢ ( 𝑤 = inf ( 𝐴 , ℝ , < ) → - 𝑤 = - inf ( 𝐴 , ℝ , < ) ) |
44 |
|
negex |
⊢ - inf ( 𝐴 , ℝ , < ) ∈ V |
45 |
43 7 44
|
fvmpt |
⊢ ( inf ( 𝐴 , ℝ , < ) ∈ ℝ → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ inf ( 𝐴 , ℝ , < ) ) = - inf ( 𝐴 , ℝ , < ) ) |
46 |
42 45
|
eqtrid |
⊢ ( inf ( 𝐴 , ℝ , < ) ∈ ℝ → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) = - inf ( 𝐴 , ℝ , < ) ) |
47 |
1 46
|
syl |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) = - inf ( 𝐴 , ℝ , < ) ) |
48 |
39 47
|
eqtr2d |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → - inf ( 𝐴 , ℝ , < ) = sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) ) |
49 |
48
|
negeqd |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → - - inf ( 𝐴 , ℝ , < ) = - sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) ) |
50 |
3 49
|
eqtr3d |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) = - sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) ) |