Step | Hyp | Ref
| Expression |
1 | | ioof 13373 |
. . . 4
β’
(,):(β* Γ β*)βΆπ«
β |
2 | | ffn 6672 |
. . . 4
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
3 | | ovelrn 7534 |
. . . 4
β’ ((,) Fn
(β* Γ β*) β (π΄ β ran (,) β βπ β β*
βπ β
β* π΄ =
(π(,)π))) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
β’ (π΄ β ran (,) β
βπ β
β* βπ β β* π΄ = (π(,)π)) |
5 | | ioorf.1 |
. . . . . . . . 9
β’ πΉ = (π₯ β ran (,) β¦ if(π₯ = β
, β¨0, 0β©, β¨inf(π₯, β*, < ),
sup(π₯, β*,
< )β©)) |
6 | 5 | ioorinv2 24962 |
. . . . . . . 8
β’ ((π(,)π) β β
β (πΉβ(π(,)π)) = β¨π, πβ©) |
7 | 6 | fveq2d 6850 |
. . . . . . 7
β’ ((π(,)π) β β
β ((,)β(πΉβ(π(,)π))) = ((,)ββ¨π, πβ©)) |
8 | | df-ov 7364 |
. . . . . . 7
β’ (π(,)π) = ((,)ββ¨π, πβ©) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . 6
β’ ((π(,)π) β β
β ((,)β(πΉβ(π(,)π))) = (π(,)π)) |
10 | | df-ne 2941 |
. . . . . . . 8
β’ (π΄ β β
β Β¬ π΄ = β
) |
11 | | neeq1 3003 |
. . . . . . . 8
β’ (π΄ = (π(,)π) β (π΄ β β
β (π(,)π) β β
)) |
12 | 10, 11 | bitr3id 285 |
. . . . . . 7
β’ (π΄ = (π(,)π) β (Β¬ π΄ = β
β (π(,)π) β β
)) |
13 | | 2fveq3 6851 |
. . . . . . . 8
β’ (π΄ = (π(,)π) β ((,)β(πΉβπ΄)) = ((,)β(πΉβ(π(,)π)))) |
14 | | id 22 |
. . . . . . . 8
β’ (π΄ = (π(,)π) β π΄ = (π(,)π)) |
15 | 13, 14 | eqeq12d 2749 |
. . . . . . 7
β’ (π΄ = (π(,)π) β (((,)β(πΉβπ΄)) = π΄ β ((,)β(πΉβ(π(,)π))) = (π(,)π))) |
16 | 12, 15 | imbi12d 345 |
. . . . . 6
β’ (π΄ = (π(,)π) β ((Β¬ π΄ = β
β ((,)β(πΉβπ΄)) = π΄) β ((π(,)π) β β
β ((,)β(πΉβ(π(,)π))) = (π(,)π)))) |
17 | 9, 16 | mpbiri 258 |
. . . . 5
β’ (π΄ = (π(,)π) β (Β¬ π΄ = β
β ((,)β(πΉβπ΄)) = π΄)) |
18 | 17 | a1i 11 |
. . . 4
β’ ((π β β*
β§ π β
β*) β (π΄ = (π(,)π) β (Β¬ π΄ = β
β ((,)β(πΉβπ΄)) = π΄))) |
19 | 18 | rexlimivv 3193 |
. . 3
β’
(βπ β
β* βπ β β* π΄ = (π(,)π) β (Β¬ π΄ = β
β ((,)β(πΉβπ΄)) = π΄)) |
20 | 4, 19 | sylbi 216 |
. 2
β’ (π΄ β ran (,) β (Β¬
π΄ = β
β
((,)β(πΉβπ΄)) = π΄)) |
21 | | ioorebas 13377 |
. . . . . . 7
β’ (0(,)0)
β ran (,) |
22 | 5 | ioorval 24961 |
. . . . . . 7
β’ ((0(,)0)
β ran (,) β (πΉβ(0(,)0)) = if((0(,)0) = β
,
β¨0, 0β©, β¨inf((0(,)0), β*, < ), sup((0(,)0),
β*, < )β©)) |
23 | 21, 22 | ax-mp 5 |
. . . . . 6
β’ (πΉβ(0(,)0)) = if((0(,)0) =
β
, β¨0, 0β©, β¨inf((0(,)0), β*, < ),
sup((0(,)0), β*, < )β©) |
24 | | iooid 13301 |
. . . . . . 7
β’ (0(,)0) =
β
|
25 | 24 | iftruei 4497 |
. . . . . 6
β’
if((0(,)0) = β
, β¨0, 0β©, β¨inf((0(,)0),
β*, < ), sup((0(,)0), β*, < )β©) =
β¨0, 0β© |
26 | 23, 25 | eqtri 2761 |
. . . . 5
β’ (πΉβ(0(,)0)) = β¨0,
0β© |
27 | 26 | fveq2i 6849 |
. . . 4
β’
((,)β(πΉβ(0(,)0))) = ((,)ββ¨0,
0β©) |
28 | | df-ov 7364 |
. . . 4
β’ (0(,)0) =
((,)ββ¨0, 0β©) |
29 | 27, 28 | eqtr4i 2764 |
. . 3
β’
((,)β(πΉβ(0(,)0))) = (0(,)0) |
30 | 24 | eqeq2i 2746 |
. . . . . 6
β’ (π΄ = (0(,)0) β π΄ = β
) |
31 | 30 | biimpri 227 |
. . . . 5
β’ (π΄ = β
β π΄ = (0(,)0)) |
32 | 31 | fveq2d 6850 |
. . . 4
β’ (π΄ = β
β (πΉβπ΄) = (πΉβ(0(,)0))) |
33 | 32 | fveq2d 6850 |
. . 3
β’ (π΄ = β
β
((,)β(πΉβπ΄)) = ((,)β(πΉβ(0(,)0)))) |
34 | 29, 33, 31 | 3eqtr4a 2799 |
. 2
β’ (π΄ = β
β
((,)β(πΉβπ΄)) = π΄) |
35 | 20, 34 | pm2.61d2 181 |
1
β’ (π΄ β ran (,) β
((,)β(πΉβπ΄)) = π΄) |