Metamath Proof Explorer


Theorem pimdecfgtioc

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

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

Proof

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