Metamath Proof Explorer

Theorem pimincfltioo

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

Proof

Step Hyp Ref Expression
1 pimincfltioo.x 
 |-  F/ x ph
2 pimincfltioo.h 
 |-  F/ y ph
3 pimincfltioo.a 
 |-  ( ph -> A C_ RR )
4 pimincfltioo.f 
 |-  ( ph -> F : A --> RR* )
5 pimincfltioo.i 
 |-  ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
6 pimincfltioo.r 
 |-  ( ph -> R e. RR* )
7 pimincfltioo.y 
 |-  Y = { x e. A | ( F ` x ) < R }
8 pimincfltioo.c 
 |-  S = sup ( Y , RR* , < )
9 pimincfltioo.e 
 |-  ( ph -> -. S e. Y )
10 pimincfltioo.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 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 ) ) /\ -. ( F ` x ) < R ) -> x < S )
32 simpr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> -. ( F ` x ) < R )
33 6 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> R e. RR* )
34 33 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> R e. RR* )
35 4 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> F : A --> RR* )
36 35 18 ffvelrnd 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` x ) e. RR* )
37 36 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> ( F ` x ) e. RR* )
38 34 37 xrlenltd 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> ( R <_ ( F ` x ) <-> -. ( F ` x ) < R ) )
39 32 38 mpbird 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> R <_ ( F ` x ) )
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 R <_ ( F ` x )
43 41 42 nfan 
 |-  F/ y ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) )
44 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
45 44 breq1d 
 |-  ( x = y -> ( ( F ` x ) < R <-> ( F ` y ) < R ) )
46 45 7 elrab2 
 |-  ( y e. Y <-> ( y e. A /\ ( F ` y ) < R ) )
47 46 biimpi 
 |-  ( y e. Y -> ( y e. A /\ ( F ` y ) < R ) )
48 47 simprd 
 |-  ( y e. Y -> ( F ` y ) < R )
49 48 adantl 
 |-  ( ( ph /\ y e. Y ) -> ( F ` y ) < R )
50 49 ad5ant14 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ -. y <_ x ) -> ( F ` y ) < R )
51 3 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> A C_ RR )
52 51 18 sseldd 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x e. RR )
53 52 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ -. y <_ x ) -> x e. RR )
54 14 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. RR )
55 54 ad5ant14 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ -. y <_ x ) -> y e. RR )
56 simpr 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> -. y <_ x )
57 52 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> x e. RR )
58 54 ad4ant13 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> y e. RR )
59 57 58 ltnled 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> ( x < y <-> -. y <_ x ) )
60 56 59 mpbird 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ -. y <_ x ) -> x < y )
61 60 adantllr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ -. y <_ x ) -> x < y )
62 53 55 61 ltled 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ -. y <_ x ) -> x <_ y )
63 33 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ x <_ y ) -> R e. RR* )
64 36 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ x <_ y ) -> ( F ` x ) e. RR* )
65 4 adantr 
 |-  ( ( ph /\ y e. Y ) -> F : A --> RR* )
66 13 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. A )
67 65 66 ffvelrnd 
 |-  ( ( ph /\ y e. Y ) -> ( F ` y ) e. RR* )
68 67 ad5ant14 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ x <_ y ) -> ( F ` y ) e. RR* )
69 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ x <_ y ) -> R <_ ( F ` x ) )
70 nfv 
 |-  F/ w ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y )
71 nfv 
 |-  F/ z ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y )
72 breq1 
 |-  ( w = x -> ( w <_ z <-> x <_ z ) )
73 fveq2 
 |-  ( w = x -> ( F ` w ) = ( F ` x ) )
74 73 breq1d 
 |-  ( w = x -> ( ( F ` w ) <_ ( F ` z ) <-> ( F ` x ) <_ ( F ` z ) ) )
75 72 74 imbi12d 
 |-  ( w = x -> ( ( w <_ z -> ( F ` w ) <_ ( F ` z ) ) <-> ( x <_ z -> ( F ` x ) <_ ( F ` z ) ) ) )
76 breq2 
 |-  ( z = y -> ( x <_ z <-> x <_ y ) )
77 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
78 77 breq2d 
 |-  ( z = y -> ( ( F ` x ) <_ ( F ` z ) <-> ( F ` x ) <_ ( F ` y ) ) )
79 76 78 imbi12d 
 |-  ( z = y -> ( ( x <_ z -> ( F ` x ) <_ ( F ` z ) ) <-> ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) ) )
80 75 79 cbvral2vw 
 |-  ( A. w e. A A. z e. A ( w <_ z -> ( F ` w ) <_ ( F ` z ) ) <-> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
81 5 80 sylibr 
 |-  ( ph -> A. w e. A A. z e. A ( w <_ z -> ( F ` w ) <_ ( F ` z ) ) )
82 81 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> A. w e. A A. z e. A ( w <_ z -> ( F ` w ) <_ ( F ` z ) ) )
83 18 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> x e. A )
84 66 ad4ant13 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> y e. A )
85 simpr 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> x <_ y )
86 70 71 82 83 84 85 dmrelrnrel 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ y e. Y ) /\ x <_ y ) -> ( F ` x ) <_ ( F ` y ) )
87 86 adantllr 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ x <_ y ) -> ( F ` x ) <_ ( F ` y ) )
88 63 64 68 69 87 xrletrd 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ x <_ y ) -> R <_ ( F ` y ) )
89 63 68 xrlenltd 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ x <_ y ) -> ( R <_ ( F ` y ) <-> -. ( F ` y ) < R ) )
90 88 89 mpbid 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ x <_ y ) -> -. ( F ` y ) < R )
91 62 90 syldan 
 |-  ( ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) /\ -. y <_ x ) -> -. ( F ` y ) < R )
92 50 91 condan 
 |-  ( ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) /\ y e. Y ) -> y <_ x )
93 92 ex 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) -> ( y e. Y -> y <_ x ) )
94 43 93 ralrimi 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ R <_ ( F ` x ) ) -> A. y e. Y y <_ x )
95 39 94 syldan 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> A. y e. Y y <_ x )
96 22 adantr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> Y C_ RR* )
97 21 52 sselid 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x e. RR* )
98 supxrleub 
 |-  ( ( Y C_ RR* /\ x e. RR* ) -> ( sup ( Y , RR* , < ) <_ x <-> A. y e. Y y <_ x ) )
99 96 97 98 syl2anc 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( sup ( Y , RR* , < ) <_ x <-> A. y e. Y y <_ x ) )
100 99 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> ( sup ( Y , RR* , < ) <_ x <-> A. y e. Y y <_ x ) )
101 95 100 mpbird 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> sup ( Y , RR* , < ) <_ x )
102 8 101 eqbrtrid 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> S <_ x )
103 25 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> S e. RR* )
104 97 adantr 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> x e. RR* )
105 103 104 xrlenltd 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> ( S <_ x <-> -. x < S ) )
106 102 105 mpbid 
 |-  ( ( ( ph /\ x e. ( I i^i A ) ) /\ -. ( F ` x ) < R ) -> -. x < S )
107 31 106 condan 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( F ` x ) < R )
108 18 107 jca 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> ( x e. A /\ ( F ` x ) < R ) )
109 7 rabeq2i 
 |-  ( x e. Y <-> ( x e. A /\ ( F ` x ) < R ) )
110 108 109 sylibr 
 |-  ( ( ph /\ x e. ( I i^i A ) ) -> x e. Y )
111 110 ex 
 |-  ( ph -> ( x e. ( I i^i A ) -> x e. Y ) )
112 1 111 ralrimi 
 |-  ( ph -> A. x e. ( I i^i A ) x e. Y )
113 nfcv 
 |-  F/_ x ( I i^i A )
114 nfrab1 
 |-  F/_ x { x e. A | ( F ` x ) < R }
115 7 114 nfcxfr 
 |-  F/_ x Y
116 113 115 dfss3f 
 |-  ( ( I i^i A ) C_ Y <-> A. x e. ( I i^i A ) x e. Y )
117 112 116 sylibr 
 |-  ( ph -> ( I i^i A ) C_ Y )
118 16 117 eqssd 
 |-  ( ph -> Y = ( I i^i A ) )