Step | Hyp | Ref
| Expression |
1 | | lttri3 8037 |
. . . . . 6
β’ ((π β β β§ π β β) β (π = π β (Β¬ π < π β§ Β¬ π < π))) |
2 | 1 | adantl 277 |
. . . . 5
β’ ((π β§ (π β β β§ π β β)) β (π = π β (Β¬ π < π β§ Β¬ π < π))) |
3 | | infrenegsupex.ex |
. . . . 5
β’ (π β βπ₯ β β (βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β (π₯ < π¦ β βπ§ β π΄ π§ < π¦))) |
4 | 2, 3 | infclti 7022 |
. . . 4
β’ (π β inf(π΄, β, < ) β
β) |
5 | 4 | recnd 7986 |
. . 3
β’ (π β inf(π΄, β, < ) β
β) |
6 | 5 | negnegd 8259 |
. 2
β’ (π β --inf(π΄, β, < ) = inf(π΄, β, < )) |
7 | | negeq 8150 |
. . . . . . . . 9
β’ (π€ = π§ β -π€ = -π§) |
8 | 7 | cbvmptv 4100 |
. . . . . . . 8
β’ (π€ β β β¦ -π€) = (π§ β β β¦ -π§) |
9 | 8 | mptpreima 5123 |
. . . . . . 7
β’ (β‘(π€ β β β¦ -π€) β π΄) = {π§ β β β£ -π§ β π΄} |
10 | | eqid 2177 |
. . . . . . . . . 10
β’ (π€ β β β¦ -π€) = (π€ β β β¦ -π€) |
11 | 10 | negiso 8912 |
. . . . . . . . 9
β’ ((π€ β β β¦ -π€) Isom < , β‘ < (β, β) β§ β‘(π€ β β β¦ -π€) = (π€ β β β¦ -π€)) |
12 | 11 | simpri 113 |
. . . . . . . 8
β’ β‘(π€ β β β¦ -π€) = (π€ β β β¦ -π€) |
13 | 12 | imaeq1i 4968 |
. . . . . . 7
β’ (β‘(π€ β β β¦ -π€) β π΄) = ((π€ β β β¦ -π€) β π΄) |
14 | 9, 13 | eqtr3i 2200 |
. . . . . 6
β’ {π§ β β β£ -π§ β π΄} = ((π€ β β β¦ -π€) β π΄) |
15 | 14 | supeq1i 6987 |
. . . . 5
β’
sup({π§ β
β β£ -π§ β
π΄}, β, < ) =
sup(((π€ β β
β¦ -π€) β π΄), β, <
) |
16 | 11 | simpli 111 |
. . . . . . . . 9
β’ (π€ β β β¦ -π€) Isom < , β‘ < (β, β) |
17 | | isocnv 5812 |
. . . . . . . . 9
β’ ((π€ β β β¦ -π€) Isom < , β‘ < (β, β) β β‘(π€ β β β¦ -π€) Isom β‘ < , < (β,
β)) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
β’ β‘(π€ β β β¦ -π€) Isom β‘ < , < (β,
β) |
19 | | isoeq1 5802 |
. . . . . . . . 9
β’ (β‘(π€ β β β¦ -π€) = (π€ β β β¦ -π€) β (β‘(π€ β β β¦ -π€) Isom β‘ < , < (β, β) β
(π€ β β β¦
-π€) Isom β‘ < , < (β,
β))) |
20 | 12, 19 | ax-mp 5 |
. . . . . . . 8
β’ (β‘(π€ β β β¦ -π€) Isom β‘ < , < (β, β) β
(π€ β β β¦
-π€) Isom β‘ < , < (β,
β)) |
21 | 18, 20 | mpbi 145 |
. . . . . . 7
β’ (π€ β β β¦ -π€) Isom β‘ < , < (β,
β) |
22 | 21 | a1i 9 |
. . . . . 6
β’ (π β (π€ β β β¦ -π€) Isom β‘ < , < (β,
β)) |
23 | | infrenegsupex.ss |
. . . . . 6
β’ (π β π΄ β β) |
24 | 3 | cnvinfex 7017 |
. . . . . 6
β’ (π β βπ₯ β β (βπ¦ β π΄ Β¬ π₯β‘
< π¦ β§ βπ¦ β β (π¦β‘ < π₯ β βπ§ β π΄ π¦β‘
< π§))) |
25 | 2 | cnvti 7018 |
. . . . . 6
β’ ((π β§ (π β β β§ π β β)) β (π = π β (Β¬ πβ‘
< π β§ Β¬ πβ‘ < π))) |
26 | 22, 23, 24, 25 | supisoti 7009 |
. . . . 5
β’ (π β sup(((π€ β β β¦ -π€) β π΄), β, < ) = ((π€ β β β¦ -π€)βsup(π΄, β, β‘ < ))) |
27 | 15, 26 | eqtrid 2222 |
. . . 4
β’ (π β sup({π§ β β β£ -π§ β π΄}, β, < ) = ((π€ β β β¦ -π€)βsup(π΄, β, β‘ < ))) |
28 | | df-inf 6984 |
. . . . . . 7
β’ inf(π΄, β, < ) = sup(π΄, β, β‘ < ) |
29 | 28 | eqcomi 2181 |
. . . . . 6
β’ sup(π΄, β, β‘ < ) = inf(π΄, β, < ) |
30 | 29 | fveq2i 5519 |
. . . . 5
β’ ((π€ β β β¦ -π€)βsup(π΄, β, β‘ < )) = ((π€ β β β¦ -π€)βinf(π΄, β, < )) |
31 | | eqidd 2178 |
. . . . . 6
β’ (π β (π€ β β β¦ -π€) = (π€ β β β¦ -π€)) |
32 | | negeq 8150 |
. . . . . . 7
β’ (π€ = inf(π΄, β, < ) β -π€ = -inf(π΄, β, < )) |
33 | 32 | adantl 277 |
. . . . . 6
β’ ((π β§ π€ = inf(π΄, β, < )) β -π€ = -inf(π΄, β, < )) |
34 | 5 | negcld 8255 |
. . . . . 6
β’ (π β -inf(π΄, β, < ) β
β) |
35 | 31, 33, 4, 34 | fvmptd 5598 |
. . . . 5
β’ (π β ((π€ β β β¦ -π€)βinf(π΄, β, < )) = -inf(π΄, β, < )) |
36 | 30, 35 | eqtrid 2222 |
. . . 4
β’ (π β ((π€ β β β¦ -π€)βsup(π΄, β, β‘ < )) = -inf(π΄, β, < )) |
37 | 27, 36 | eqtr2d 2211 |
. . 3
β’ (π β -inf(π΄, β, < ) = sup({π§ β β β£ -π§ β π΄}, β, < )) |
38 | 37 | negeqd 8152 |
. 2
β’ (π β --inf(π΄, β, < ) = -sup({π§ β β β£ -π§ β π΄}, β, < )) |
39 | 6, 38 | eqtr3d 2212 |
1
β’ (π β inf(π΄, β, < ) = -sup({π§ β β β£ -π§ β π΄}, β, < )) |