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 sseldi 
 |-  ( 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 sseldi 
 |-  ( 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 ) )