Step | Hyp | Ref
| Expression |
1 | | ioorf.1 |
. 2
β’ πΉ = (π₯ β ran (,) β¦ if(π₯ = β
, β¨0, 0β©, β¨inf(π₯, β*, < ),
sup(π₯, β*,
< )β©)) |
2 | | ioof 13373 |
. . . 4
β’
(,):(β* Γ β*)βΆπ«
β |
3 | | ffn 6672 |
. . . 4
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
4 | | ovelrn 7534 |
. . . 4
β’ ((,) Fn
(β* Γ β*) β (π₯ β ran (,) β βπ β β*
βπ β
β* π₯ =
(π(,)π))) |
5 | 2, 3, 4 | mp2b 10 |
. . 3
β’ (π₯ β ran (,) β
βπ β
β* βπ β β* π₯ = (π(,)π)) |
6 | | 0le0 12262 |
. . . . . . . . 9
β’ 0 β€
0 |
7 | | df-br 5110 |
. . . . . . . . 9
β’ (0 β€ 0
β β¨0, 0β© β β€ ) |
8 | 6, 7 | mpbi 229 |
. . . . . . . 8
β’ β¨0,
0β© β β€ |
9 | | 0xr 11210 |
. . . . . . . . 9
β’ 0 β
β* |
10 | | opelxpi 5674 |
. . . . . . . . 9
β’ ((0
β β* β§ 0 β β*) β β¨0,
0β© β (β* Γ
β*)) |
11 | 9, 9, 10 | mp2an 691 |
. . . . . . . 8
β’ β¨0,
0β© β (β* Γ
β*) |
12 | 8, 11 | elini 4157 |
. . . . . . 7
β’ β¨0,
0β© β ( β€ β© (β* Γ
β*)) |
13 | 12 | a1i 11 |
. . . . . 6
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ π₯ = β
) β β¨0, 0β© β (
β€ β© (β* Γ β*))) |
14 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β π₯ = (π(,)π)) |
15 | 14 | infeq1d 9421 |
. . . . . . . . 9
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β inf(π₯, β*, < ) = inf((π(,)π), β*, <
)) |
16 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β π β β*) |
17 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β π β β*) |
18 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β Β¬ π₯ = β
) |
19 | 18 | neqned 2947 |
. . . . . . . . . . 11
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β π₯ β β
) |
20 | 14, 19 | eqnetrrd 3009 |
. . . . . . . . . 10
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β (π(,)π) β β
) |
21 | | df-ioo 13277 |
. . . . . . . . . . 11
β’ (,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) |
22 | | idd 24 |
. . . . . . . . . . 11
β’ ((π€ β β*
β§ π β
β*) β (π€ < π β π€ < π)) |
23 | | xrltle 13077 |
. . . . . . . . . . 11
β’ ((π€ β β*
β§ π β
β*) β (π€ < π β π€ β€ π)) |
24 | | idd 24 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π€ β
β*) β (π < π€ β π < π€)) |
25 | | xrltle 13077 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π€ β
β*) β (π < π€ β π β€ π€)) |
26 | 21, 22, 23, 24, 25 | ixxlb 13295 |
. . . . . . . . . 10
β’ ((π β β*
β§ π β
β* β§ (π(,)π) β β
) β inf((π(,)π), β*, < ) = π) |
27 | 16, 17, 20, 26 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β inf((π(,)π), β*, < ) = π) |
28 | 15, 27 | eqtrd 2773 |
. . . . . . . 8
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β inf(π₯, β*, < ) = π) |
29 | 14 | supeq1d 9390 |
. . . . . . . . 9
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β sup(π₯, β*, < ) = sup((π(,)π), β*, <
)) |
30 | 21, 22, 23, 24, 25 | ixxub 13294 |
. . . . . . . . . 10
β’ ((π β β*
β§ π β
β* β§ (π(,)π) β β
) β sup((π(,)π), β*, < ) = π) |
31 | 16, 17, 20, 30 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β sup((π(,)π), β*, < ) = π) |
32 | 29, 31 | eqtrd 2773 |
. . . . . . . 8
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β sup(π₯, β*, < ) = π) |
33 | 28, 32 | opeq12d 4842 |
. . . . . . 7
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β β¨inf(π₯, β*, < ),
sup(π₯, β*,
< )β© = β¨π,
πβ©) |
34 | | ioon0 13299 |
. . . . . . . . . . . 12
β’ ((π β β*
β§ π β
β*) β ((π(,)π) β β
β π < π)) |
35 | 34 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β ((π(,)π) β β
β π < π)) |
36 | 20, 35 | mpbid 231 |
. . . . . . . . . 10
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β π < π) |
37 | | xrltle 13077 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π β
β*) β (π < π β π β€ π)) |
38 | 37 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β (π < π β π β€ π)) |
39 | 36, 38 | mpd 15 |
. . . . . . . . 9
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β π β€ π) |
40 | | df-br 5110 |
. . . . . . . . 9
β’ (π β€ π β β¨π, πβ© β β€ ) |
41 | 39, 40 | sylib 217 |
. . . . . . . 8
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β β¨π, πβ© β β€ ) |
42 | | opelxpi 5674 |
. . . . . . . . 9
β’ ((π β β*
β§ π β
β*) β β¨π, πβ© β (β* Γ
β*)) |
43 | 42 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β β¨π, πβ© β (β* Γ
β*)) |
44 | 41, 43 | elind 4158 |
. . . . . . 7
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β β¨π, πβ© β ( β€ β©
(β* Γ β*))) |
45 | 33, 44 | eqeltrd 2834 |
. . . . . 6
β’ ((((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β§ Β¬ π₯ = β
) β β¨inf(π₯, β*, < ),
sup(π₯, β*,
< )β© β ( β€ β© (β* Γ
β*))) |
46 | 13, 45 | ifclda 4525 |
. . . . 5
β’ (((π β β*
β§ π β
β*) β§ π₯ = (π(,)π)) β if(π₯ = β
, β¨0, 0β©, β¨inf(π₯, β*, < ),
sup(π₯, β*,
< )β©) β ( β€ β© (β* Γ
β*))) |
47 | 46 | ex 414 |
. . . 4
β’ ((π β β*
β§ π β
β*) β (π₯ = (π(,)π) β if(π₯ = β
, β¨0, 0β©, β¨inf(π₯, β*, < ),
sup(π₯, β*,
< )β©) β ( β€ β© (β* Γ
β*)))) |
48 | 47 | rexlimivv 3193 |
. . 3
β’
(βπ β
β* βπ β β* π₯ = (π(,)π) β if(π₯ = β
, β¨0, 0β©, β¨inf(π₯, β*, < ),
sup(π₯, β*,
< )β©) β ( β€ β© (β* Γ
β*))) |
49 | 5, 48 | sylbi 216 |
. 2
β’ (π₯ β ran (,) β if(π₯ = β
, β¨0, 0β©,
β¨inf(π₯,
β*, < ), sup(π₯, β*, < )β©) β (
β€ β© (β* Γ β*))) |
50 | 1, 49 | fmpti 7064 |
1
β’ πΉ:ran (,)βΆ( β€ β©
(β* Γ β*)) |