Step | Hyp | Ref
| Expression |
1 | | infrecl 12145 |
. . . 4
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β inf(π΄, β, < ) β
β) |
2 | 1 | recnd 11191 |
. . 3
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β inf(π΄, β, < ) β
β) |
3 | 2 | negnegd 11511 |
. 2
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β --inf(π΄, β, < ) = inf(π΄, β, < )) |
4 | | negeq 11401 |
. . . . . . . . 9
β’ (π€ = π§ β -π€ = -π§) |
5 | 4 | cbvmptv 5222 |
. . . . . . . 8
β’ (π€ β β β¦ -π€) = (π§ β β β¦ -π§) |
6 | 5 | mptpreima 6194 |
. . . . . . 7
β’ (β‘(π€ β β β¦ -π€) β π΄) = {π§ β β β£ -π§ β π΄} |
7 | | eqid 2733 |
. . . . . . . . . 10
β’ (π€ β β β¦ -π€) = (π€ β β β¦ -π€) |
8 | 7 | negiso 12143 |
. . . . . . . . 9
β’ ((π€ β β β¦ -π€) Isom < , β‘ < (β, β) β§ β‘(π€ β β β¦ -π€) = (π€ β β β¦ -π€)) |
9 | 8 | simpri 487 |
. . . . . . . 8
β’ β‘(π€ β β β¦ -π€) = (π€ β β β¦ -π€) |
10 | 9 | imaeq1i 6014 |
. . . . . . 7
β’ (β‘(π€ β β β¦ -π€) β π΄) = ((π€ β β β¦ -π€) β π΄) |
11 | 6, 10 | eqtr3i 2763 |
. . . . . 6
β’ {π§ β β β£ -π§ β π΄} = ((π€ β β β¦ -π€) β π΄) |
12 | 11 | supeq1i 9391 |
. . . . 5
β’
sup({π§ β
β β£ -π§ β
π΄}, β, < ) =
sup(((π€ β β
β¦ -π€) β π΄), β, <
) |
13 | 8 | simpli 485 |
. . . . . . . . 9
β’ (π€ β β β¦ -π€) Isom < , β‘ < (β, β) |
14 | | isocnv 7279 |
. . . . . . . . 9
β’ ((π€ β β β¦ -π€) Isom < , β‘ < (β, β) β β‘(π€ β β β¦ -π€) Isom β‘ < , < (β,
β)) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . 8
β’ β‘(π€ β β β¦ -π€) Isom β‘ < , < (β,
β) |
16 | | isoeq1 7266 |
. . . . . . . . 9
β’ (β‘(π€ β β β¦ -π€) = (π€ β β β¦ -π€) β (β‘(π€ β β β¦ -π€) Isom β‘ < , < (β, β) β
(π€ β β β¦
-π€) Isom β‘ < , < (β,
β))) |
17 | 9, 16 | ax-mp 5 |
. . . . . . . 8
β’ (β‘(π€ β β β¦ -π€) Isom β‘ < , < (β, β) β
(π€ β β β¦
-π€) Isom β‘ < , < (β,
β)) |
18 | 15, 17 | mpbi 229 |
. . . . . . 7
β’ (π€ β β β¦ -π€) Isom β‘ < , < (β,
β) |
19 | 18 | a1i 11 |
. . . . . 6
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β (π€ β β β¦ -π€) Isom β‘ < , < (β,
β)) |
20 | | simp1 1137 |
. . . . . 6
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β π΄ β β) |
21 | | infm3 12122 |
. . . . . . 7
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β βπ₯ β β (βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β (π₯ < π¦ β βπ§ β π΄ π§ < π¦))) |
22 | | vex 3451 |
. . . . . . . . . . . 12
β’ π₯ β V |
23 | | vex 3451 |
. . . . . . . . . . . 12
β’ π¦ β V |
24 | 22, 23 | brcnv 5842 |
. . . . . . . . . . 11
β’ (π₯β‘ < π¦ β π¦ < π₯) |
25 | 24 | notbii 320 |
. . . . . . . . . 10
β’ (Β¬
π₯β‘ < π¦ β Β¬ π¦ < π₯) |
26 | 25 | ralbii 3093 |
. . . . . . . . 9
β’
(βπ¦ β
π΄ Β¬ π₯β‘
< π¦ β βπ¦ β π΄ Β¬ π¦ < π₯) |
27 | 23, 22 | brcnv 5842 |
. . . . . . . . . . 11
β’ (π¦β‘ < π₯ β π₯ < π¦) |
28 | | vex 3451 |
. . . . . . . . . . . . 13
β’ π§ β V |
29 | 23, 28 | brcnv 5842 |
. . . . . . . . . . . 12
β’ (π¦β‘ < π§ β π§ < π¦) |
30 | 29 | rexbii 3094 |
. . . . . . . . . . 11
β’
(βπ§ β
π΄ π¦β‘
< π§ β βπ§ β π΄ π§ < π¦) |
31 | 27, 30 | imbi12i 351 |
. . . . . . . . . 10
β’ ((π¦β‘ < π₯ β βπ§ β π΄ π¦β‘
< π§) β (π₯ < π¦ β βπ§ β π΄ π§ < π¦)) |
32 | 31 | ralbii 3093 |
. . . . . . . . 9
β’
(βπ¦ β
β (π¦β‘ < π₯ β βπ§ β π΄ π¦β‘
< π§) β
βπ¦ β β
(π₯ < π¦ β βπ§ β π΄ π§ < π¦)) |
33 | 26, 32 | anbi12i 628 |
. . . . . . . 8
β’
((βπ¦ β
π΄ Β¬ π₯β‘
< π¦ β§ βπ¦ β β (π¦β‘ < π₯ β βπ§ β π΄ π¦β‘
< π§)) β
(βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β (π₯ < π¦ β βπ§ β π΄ π§ < π¦))) |
34 | 33 | rexbii 3094 |
. . . . . . 7
β’
(βπ₯ β
β (βπ¦ β
π΄ Β¬ π₯β‘
< π¦ β§ βπ¦ β β (π¦β‘ < π₯ β βπ§ β π΄ π¦β‘
< π§)) β
βπ₯ β β
(βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β (π₯ < π¦ β βπ§ β π΄ π§ < π¦))) |
35 | 21, 34 | sylibr 233 |
. . . . . 6
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯β‘
< π¦ β§ βπ¦ β β (π¦β‘ < π₯ β βπ§ β π΄ π¦β‘
< π§))) |
36 | | gtso 11244 |
. . . . . . 7
β’ β‘ < Or β |
37 | 36 | a1i 11 |
. . . . . 6
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β β‘ < Or β) |
38 | 19, 20, 35, 37 | supiso 9419 |
. . . . 5
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β sup(((π€ β β β¦ -π€) β π΄), β, < ) = ((π€ β β β¦ -π€)βsup(π΄, β, β‘ < ))) |
39 | 12, 38 | eqtrid 2785 |
. . . 4
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β sup({π§ β β β£ -π§ β π΄}, β, < ) = ((π€ β β β¦ -π€)βsup(π΄, β, β‘ < ))) |
40 | | df-inf 9387 |
. . . . . . . 8
β’ inf(π΄, β, < ) = sup(π΄, β, β‘ < ) |
41 | 40 | eqcomi 2742 |
. . . . . . 7
β’ sup(π΄, β, β‘ < ) = inf(π΄, β, < ) |
42 | 41 | fveq2i 6849 |
. . . . . 6
β’ ((π€ β β β¦ -π€)βsup(π΄, β, β‘ < )) = ((π€ β β β¦ -π€)βinf(π΄, β, < )) |
43 | | negeq 11401 |
. . . . . . 7
β’ (π€ = inf(π΄, β, < ) β -π€ = -inf(π΄, β, < )) |
44 | | negex 11407 |
. . . . . . 7
β’
-inf(π΄, β,
< ) β V |
45 | 43, 7, 44 | fvmpt 6952 |
. . . . . 6
β’
(inf(π΄, β,
< ) β β β ((π€ β β β¦ -π€)βinf(π΄, β, < )) = -inf(π΄, β, < )) |
46 | 42, 45 | eqtrid 2785 |
. . . . 5
β’
(inf(π΄, β,
< ) β β β ((π€ β β β¦ -π€)βsup(π΄, β, β‘ < )) = -inf(π΄, β, < )) |
47 | 1, 46 | syl 17 |
. . . 4
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β ((π€ β β β¦ -π€)βsup(π΄, β, β‘ < )) = -inf(π΄, β, < )) |
48 | 39, 47 | eqtr2d 2774 |
. . 3
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β -inf(π΄, β, < ) = sup({π§ β β β£ -π§ β π΄}, β, < )) |
49 | 48 | negeqd 11403 |
. 2
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β --inf(π΄, β, < ) = -sup({π§ β β β£ -π§ β π΄}, β, < )) |
50 | 3, 49 | eqtr3d 2775 |
1
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β inf(π΄, β, < ) = -sup({π§ β β β£ -π§ β π΄}, β, < )) |