Metamath Proof Explorer


Theorem ioorcl

Description: The function F does not always return real numbers, but it does on intervals of finite volume. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypothesis ioorf.1 F=xran.ifx=00supx*<supx*<
Assertion ioorcl Aran.vol*AFA2

Proof

Step Hyp Ref Expression
1 ioorf.1 F=xran.ifx=00supx*<supx*<
2 1 ioorf F:ran.*×*
3 2 ffvelrni Aran.FA*×*
4 3 adantr Aran.vol*AFA*×*
5 4 elin1d Aran.vol*AFA
6 1 ioorval Aran.FA=ifA=00supA*<supA*<
7 6 adantr Aran.vol*AFA=ifA=00supA*<supA*<
8 iftrue A=ifA=00supA*<supA*<=00
9 7 8 sylan9eq Aran.vol*AA=FA=00
10 0re 0
11 opelxpi 00002
12 10 10 11 mp2an 002
13 9 12 eqeltrdi Aran.vol*AA=FA2
14 ioof .:*×*𝒫
15 ffn .:*×*𝒫.Fn*×*
16 ovelrn .Fn*×*Aran.a*b*A=ab
17 14 15 16 mp2b Aran.a*b*A=ab
18 1 ioorinv2 abFab=ab
19 18 adantl vol*ababFab=ab
20 ioorcl2 abvol*abab
21 20 ancoms vol*ababab
22 opelxpi abab2
23 21 22 syl vol*ababab2
24 19 23 eqeltrd vol*ababFab2
25 fveq2 A=abvol*A=vol*ab
26 25 eleq1d A=abvol*Avol*ab
27 neeq1 A=abAab
28 26 27 anbi12d A=abvol*AAvol*abab
29 fveq2 A=abFA=Fab
30 29 eleq1d A=abFA2Fab2
31 28 30 imbi12d A=abvol*AAFA2vol*ababFab2
32 24 31 mpbiri A=abvol*AAFA2
33 32 a1i a*b*A=abvol*AAFA2
34 33 rexlimivv a*b*A=abvol*AAFA2
35 17 34 sylbi Aran.vol*AAFA2
36 35 impl Aran.vol*AAFA2
37 13 36 pm2.61dane Aran.vol*AFA2
38 5 37 elind Aran.vol*AFA2