Metamath Proof Explorer


Theorem ioorinv

Description: The function F is an "inverse" of sorts to the open interval function. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypothesis ioorf.1 F = x ran . if x = 0 0 sup x * < sup x * <
Assertion ioorinv A ran . . F A = A

Proof

Step Hyp Ref Expression
1 ioorf.1 F = x ran . if x = 0 0 sup x * < sup x * <
2 ioof . : * × * 𝒫
3 ffn . : * × * 𝒫 . Fn * × *
4 ovelrn . Fn * × * A ran . a * b * A = a b
5 2 3 4 mp2b A ran . a * b * A = a b
6 1 ioorinv2 a b F a b = a b
7 6 fveq2d a b . F a b = . a b
8 df-ov a b = . a b
9 7 8 eqtr4di a b . F a b = a b
10 df-ne A ¬ A =
11 neeq1 A = a b A a b
12 10 11 bitr3id A = a b ¬ A = a b
13 2fveq3 A = a b . F A = . F a b
14 id A = a b A = a b
15 13 14 eqeq12d A = a b . F A = A . F a b = a b
16 12 15 imbi12d A = a b ¬ A = . F A = A a b . F a b = a b
17 9 16 mpbiri A = a b ¬ A = . F A = A
18 17 a1i a * b * A = a b ¬ A = . F A = A
19 18 rexlimivv a * b * A = a b ¬ A = . F A = A
20 5 19 sylbi A ran . ¬ A = . F A = A
21 ioorebas 0 0 ran .
22 1 ioorval 0 0 ran . F 0 0 = if 0 0 = 0 0 sup 0 0 * < sup 0 0 * <
23 21 22 ax-mp F 0 0 = if 0 0 = 0 0 sup 0 0 * < sup 0 0 * <
24 iooid 0 0 =
25 24 iftruei if 0 0 = 0 0 sup 0 0 * < sup 0 0 * < = 0 0
26 23 25 eqtri F 0 0 = 0 0
27 26 fveq2i . F 0 0 = . 0 0
28 df-ov 0 0 = . 0 0
29 27 28 eqtr4i . F 0 0 = 0 0
30 24 eqeq2i A = 0 0 A =
31 30 biimpri A = A = 0 0
32 31 fveq2d A = F A = F 0 0
33 32 fveq2d A = . F A = . F 0 0
34 29 33 31 3eqtr4a A = . F A = A
35 20 34 pm2.61d2 A ran . . F A = A