Metamath Proof Explorer

Theorem pimdecfgtioo

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

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

Proof

Step Hyp Ref Expression
1 pimdecfgtioo.x 
 |-  F/ x ph
2 pimdecfgtioo.h 
 |-  F/ y ph
3 pimdecfgtioo.a 
 |-  ( ph -> A C_ RR )
4 pimdecfgtioo.f 
 |-  ( ph -> F : A --> RR* )
5 pimdecfgtioo.d 
 |-  ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
6 pimdecfgtioo.r 
 |-  ( ph -> R e. RR* )
7 pimdecfgtioo.y 
 |-  Y = { x e. A | R < ( F ` x ) }
8 pimdecfgtioo.c 
 |-  S = sup ( Y , RR* , < )
9 pimdecfgtioo.e 
 |-  ( ph -> -. S e. Y )
10 pimdecfgtioo.i 
 |-  I = ( -oo (,) S )
11 ssrab2 
 |-  { x e. A | R < ( F ` x ) } 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 ressioosup 
 |-  ( 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 mnfxr 
 |-  -oo e. RR*
20 19 a1i 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> -oo e. RR* )
21 ressxr 
 |-  RR C_ RR*
22 14 21 sstrdi 
 |-  ( ph -> Y C_ RR* )
23 22 supxrcld 
 |-  ( ph -> sup ( Y , RR* , < ) e. RR* )
24 8 23 eqeltrid 
 |-  ( ph -> S e. RR* )
25 24 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> S e. RR* )
26 elinel1 
 |-  ( x e. ( I i^i A ) -> x e. I )
27 26 10 eleqtrdi 
 |-  ( x e. ( I i^i A ) -> x e. ( -oo (,) S ) )
28 27 adantl 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x e. ( -oo (,) S ) )
29 iooltub 
 |-  ( ( -oo e. RR* /\ S e. RR* /\ x e. ( -oo (,) S ) ) -> x < S )
30 20 25 28 29 syl3anc 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x < S )
31 30 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> x < S )
32 simpr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> -. R < ( F ` x ) )
33 4 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> F : A --> RR* )
34 33 18 ffvelrnd 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` x ) e. RR* )
35 34 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> ( F ` x ) e. RR* )
36 6 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> R e. RR* )
37 36 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> R e. RR* )
38 35 37 xrlenltd 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> ( ( F ` x ) <_ R <-> -. R < ( F ` x ) ) )
39 32 38 mpbird 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> ( F ` x ) <_ R )
40 nfv 
 |-  F/ y x e. ( I i^i A )
41 2 40 nfan 
 |-  F/ y ( ph /\ x e. ( I i^i A ) )
42 nfv 
 |-  F/ y ( F ` x ) <_ R
43 41 42 nfan 
 |-  F/ y ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R )
44 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
45 44 breq2d 
 |-  ( x = y -> ( R < ( F ` x ) <-> R < ( F ` y ) ) )
46 45 7 elrab2 
 |-  ( y e. Y <-> ( y e. A /\ R < ( F ` y ) ) )
47 46 biimpi 
 |-  ( y e. Y -> ( y e. A /\ R < ( F ` y ) ) )
48 47 simprd 
 |-  ( y e. Y -> R < ( F ` y ) )
49 48 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ -. y <_ x ) -> R < ( F ` y ) )
50 3 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> A C_ RR )
51 50 18 sseldd 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x e. RR )
52 51 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> x e. RR )
53 14 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. RR )
54 53 ad4ant13 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> y e. RR )
55 simpr 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> -. y <_ x )
56 52 54 ltnled 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> ( x < y <-> -. y <_ x ) )
57 55 56 mpbird 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> x < y )
58 52 54 57 ltled 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> x <_ y )
59 58 adantllr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ -. y <_ x ) -> x <_ y )
60 4 adantr 
 |-  ( ( ph /\ y e. Y ) -> F : A --> RR* )
61 13 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. A )
62 60 61 ffvelrnd 
 |-  ( ( ph /\ y e. Y ) -> ( F ` y ) e. RR* )
63 62 ad5ant14 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ x <_ y ) -> ( F ` y ) e. RR* )
64 34 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ x <_ y ) -> ( F ` x ) e. RR* )
65 36 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ x <_ y ) -> R e. RR* )
66 simpr 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> x <_ y )
67 rspa 
 |-  ( ( A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) /\ x e. A ) -> A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
68 5 17 67 syl2an 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
69 68 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
70 61 ad4ant13 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> y e. A )
71 rspa 
 |-  ( ( A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) /\ y e. A ) -> ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
72 69 70 71 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
73 66 72 mpd 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> ( F ` y ) <_ ( F ` x ) )
74 73 adantllr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ x <_ y ) -> ( F ` y ) <_ ( F ` x ) )
75 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ x <_ y ) -> ( F ` x ) <_ R )
76 63 64 65 74 75 xrletrd 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ x <_ y ) -> ( F ` y ) <_ R )
77 63 65 xrlenltd 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ x <_ y ) -> ( ( F ` y ) <_ R <-> -. R < ( F ` y ) ) )
78 76 77 mpbid 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ x <_ y ) -> -. R < ( F ` y ) )
79 59 78 syldan 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) /\ -. y <_ x ) -> -. R < ( F ` y ) )
80 49 79 condan 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) /\ y e. Y ) -> y <_ x )
81 80 ex 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) -> ( y e. Y -> y <_ x ) )
82 43 81 ralrimi 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ ( F ` x ) <_ R ) -> A. y e. Y y <_ x )
83 39 82 syldan 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> A. y e. Y y <_ x )
84 22 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> Y C_ RR* )
85 21 51 sselid 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x e. RR* )
86 supxrleub 
 |-  ( ( Y C_ RR* /\ x e. RR* ) -> ( sup ( Y , RR* , < ) <_ x <-> A. y e. Y y <_ x ) )
87 84 85 86 syl2anc 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( sup ( Y , RR* , < ) <_ x <-> A. y e. Y y <_ x ) )
88 87 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> ( sup ( Y , RR* , < ) <_ x <-> A. y e. Y y <_ x ) )
89 83 88 mpbird 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> sup ( Y , RR* , < ) <_ x )
90 8 89 eqbrtrid 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> S <_ x )
91 25 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> S e. RR* )
92 85 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> x e. RR* )
93 91 92 xrlenltd 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> ( S <_ x <-> -. x < S ) )
94 90 93 mpbid 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. R < ( F ` x ) ) -> -. x < S )
95 31 94 condan 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> R < ( F ` x ) )
96 18 95 jca 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( x e. A /\ R < ( F ` x ) ) )
97 7 rabeq2i 
 |-  ( x e. Y <-> ( x e. A /\ R < ( F ` x ) ) )
98 96 97 sylibr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x e. Y )
99 98 ex 
 |-  ( ph -> ( x e. ( I i^i A ) -> x e. Y ) )
100 1 99 ralrimi 
 |-  ( ph -> A. x e. ( I i^i A ) x e. Y )
101 nfcv 
 |-  F/_ x ( I i^i A )
102 nfrab1 
 |-  F/_ x { x e. A | R < ( F ` x ) }
103 7 102 nfcxfr 
 |-  F/_ x Y
104 101 103 dfss3f 
 |-  ( ( I i^i A ) C_ Y <-> A. x e. ( I i^i A ) x e. Y )
105 100 104 sylibr 
 |-  ( ph -> ( I i^i A ) C_ Y )
106 16 105 eqssd 
 |-  ( ph -> Y = ( I i^i A ) )