Metamath Proof Explorer

Theorem pimincfltioc

Description: Given a nondecreasing function, the preimage of an unbounded below, open interval, when the supremum of the preimage belongs to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses pimincfltioc.x 
|- F/ x ph
pimincfltioc.h 
|- F/ y ph
pimincfltioc.a 
|- ( ph -> A C_ RR )
pimincfltioc.f 
|- ( ph -> F : A --> RR* )
pimincfltioc.i 
|- ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
pimincfltioc.r 
|- ( ph -> R e. RR* )
pimincfltioc.y 
|- Y = { x e. A | ( F ` x ) < R }
pimincfltioc.c 
|- S = sup ( Y , RR* , < )
pimincfltioc.e 
|- ( ph -> S e. Y )
pimincfltioc.d 
|- I = ( -oo (,] S )
Assertion pimincfltioc 
|- ( ph -> Y = ( I i^i A ) )

Proof

Step Hyp Ref Expression
1 pimincfltioc.x 
 |-  F/ x ph
2 pimincfltioc.h 
 |-  F/ y ph
3 pimincfltioc.a 
 |-  ( ph -> A C_ RR )
4 pimincfltioc.f 
 |-  ( ph -> F : A --> RR* )
5 pimincfltioc.i 
 |-  ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
6 pimincfltioc.r 
 |-  ( ph -> R e. RR* )
7 pimincfltioc.y 
 |-  Y = { x e. A | ( F ` x ) < R }
8 pimincfltioc.c 
 |-  S = sup ( Y , RR* , < )
9 pimincfltioc.e 
 |-  ( ph -> S e. Y )
10 pimincfltioc.d 
 |-  I = ( -oo (,] S )
11 ssrab2 
 |-  { x e. A | ( F ` x ) < R } C_ A
12 7 11 eqsstri 
 |-  Y C_ A
13 12 a1i 
 |-  ( ph -> Y C_ A )
14 13 3 sstrd 
 |-  ( ph -> Y C_ RR )
15 14 8 9 10 ressiocsup 
 |-  ( ph -> Y C_ I )
16 15 13 ssind 
 |-  ( ph -> Y C_ ( I i^i A ) )
17 elinel2 
 |-  ( x e. ( I i^i A ) -> x e. A )
18 17 adantl 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x e. A )
19 4 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> F : A --> RR* )
20 19 18 ffvelrnd 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` x ) e. RR* )
21 12 9 sseldi 
 |-  ( ph -> S e. A )
22 4 21 ffvelrnd 
 |-  ( ph -> ( F ` S ) e. RR* )
23 22 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` S ) e. RR* )
24 6 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> R e. RR* )
25 eleq1w 
 |-  ( z = x -> ( z e. ( I i^i A ) <-> x e. ( I i^i A ) ) )
26 25 anbi2d 
 |-  ( z = x -> ( ( ph /\ z e. ( I i^i A ) ) <-> ( ph /\ x e. ( I i^i A ) ) ) )
27 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
28 27 breq1d 
 |-  ( z = x -> ( ( F ` z ) <_ ( F ` S ) <-> ( F ` x ) <_ ( F ` S ) ) )
29 26 28 imbi12d 
 |-  ( z = x -> ( ( ( ph /\ z e. ( I i^i A ) ) -> ( F ` z ) <_ ( F ` S ) ) <-> ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` x ) <_ ( F ` S ) ) ) )
30 nfv 
 |-  F/ x z e. ( I i^i A )
31 1 30 nfan 
 |-  F/ x ( ph /\ z e. ( I i^i A ) )
32 nfv 
 |-  F/ y z e. ( I i^i A )
33 2 32 nfan 
 |-  F/ y ( ph /\ z e. ( I i^i A ) )
34 5 adantr 
 |-  ( ( ph /\ z e. ( I i^i A ) ) -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
35 elinel2 
 |-  ( z e. ( I i^i A ) -> z e. A )
36 35 adantl 
 |-  ( ( ph /\ z e. ( I i^i A ) ) -> z e. A )
37 21 adantr 
 |-  ( ( ph /\ z e. ( I i^i A ) ) -> S e. A )
38 mnfxr 
 |-  -oo e. RR*
39 38 a1i 
 |-  ( ( ph /\ z e. ( I i^i A ) ) -> -oo e. RR* )
40 ressxr 
 |-  RR C_ RR*
41 14 9 sseldd 
 |-  ( ph -> S e. RR )
42 40 41 sseldi 
 |-  ( ph -> S e. RR* )
43 42 adantr 
 |-  ( ( ph /\ z e. ( I i^i A ) ) -> S e. RR* )
44 elinel1 
 |-  ( z e. ( I i^i A ) -> z e. I )
45 44 10 eleqtrdi 
 |-  ( z e. ( I i^i A ) -> z e. ( -oo (,] S ) )
46 45 adantl 
 |-  ( ( ph /\ z e. ( I i^i A ) ) -> z e. ( -oo (,] S ) )
47 iocleub 
 |-  ( ( -oo e. RR* /\ S e. RR* /\ z e. ( -oo (,] S ) ) -> z <_ S )
48 39 43 46 47 syl3anc 
 |-  ( ( ph /\ z e. ( I i^i A ) ) -> z <_ S )
49 31 33 34 36 37 48 dmrelrnrel 
 |-  ( ( ph /\ z e. ( I i^i A ) ) -> ( F ` z ) <_ ( F ` S ) )
50 29 49 chvarvv 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` x ) <_ ( F ` S ) )
51 fveq2 
 |-  ( x = S -> ( F ` x ) = ( F ` S ) )
52 51 breq1d 
 |-  ( x = S -> ( ( F ` x ) < R <-> ( F ` S ) < R ) )
53 52 7 elrab2 
 |-  ( S e. Y <-> ( S e. A /\ ( F ` S ) < R ) )
54 9 53 sylib 
 |-  ( ph -> ( S e. A /\ ( F ` S ) < R ) )
55 54 simprd 
 |-  ( ph -> ( F ` S ) < R )
56 55 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` S ) < R )
57 20 23 24 50 56 xrlelttrd 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` x ) < R )
58 18 57 jca 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( x e. A /\ ( F ` x ) < R ) )
59 7 rabeq2i 
 |-  ( x e. Y <-> ( x e. A /\ ( F ` x ) < R ) )
60 58 59 sylibr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x e. Y )
61 60 ex 
 |-  ( ph -> ( x e. ( I i^i A ) -> x e. Y ) )
62 1 61 ralrimi 
 |-  ( ph -> A. x e. ( I i^i A ) x e. Y )
63 30 nfci 
 |-  F/_ x ( I i^i A )
64 nfrab1 
 |-  F/_ x { x e. A | ( F ` x ) < R }
65 7 64 nfcxfr 
 |-  F/_ x Y
66 63 65 dfss3f 
 |-  ( ( I i^i A ) C_ Y <-> A. x e. ( I i^i A ) x e. Y )
67 62 66 sylibr 
 |-  ( ph -> ( I i^i A ) C_ Y )
68 16 67 eqssd 
 |-  ( ph -> Y = ( I i^i A ) )