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