Metamath Proof Explorer

Theorem iunhoiioolem

Description: A n-dimensional open interval expressed as the indexed union of half-open intervals. One side of the double inclusion. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses iunhoiioolem.K 
|- F/ k ph
iunhoiioolem.x 
|- ( ph -> X e. Fin )
iunhoiioolem.n 
|- ( ph -> X =/= (/) )
iunhoiioolem.a 
|- ( ( ph /\ k e. X ) -> A e. RR )
iunhoiioolem.b 
|- ( ( ph /\ k e. X ) -> B e. RR* )
iunhoiioolem.f 
|- ( ph -> F e. X_ k e. X ( A (,) B ) )
iunhoiioolem.c 
|- C = inf ( ran ( k e. X |-> ( ( F ` k ) - A ) ) , RR , < )
Assertion iunhoiioolem 
|- ( ph -> F e. U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) )

Proof

Step Hyp Ref Expression
1 iunhoiioolem.K 
 |-  F/ k ph
2 iunhoiioolem.x 
 |-  ( ph -> X e. Fin )
3 iunhoiioolem.n 
 |-  ( ph -> X =/= (/) )
4 iunhoiioolem.a 
 |-  ( ( ph /\ k e. X ) -> A e. RR )
5 iunhoiioolem.b 
 |-  ( ( ph /\ k e. X ) -> B e. RR* )
6 iunhoiioolem.f 
 |-  ( ph -> F e. X_ k e. X ( A (,) B ) )
7 iunhoiioolem.c 
 |-  C = inf ( ran ( k e. X |-> ( ( F ` k ) - A ) ) , RR , < )
8 eqid 
 |-  ( k e. X |-> ( ( F ` k ) - A ) ) = ( k e. X |-> ( ( F ` k ) - A ) )
9 ixpf 
 |-  ( F e. X_ k e. X ( A (,) B ) -> F : X --> U_ k e. X ( A (,) B ) )
10 6 9 syl 
 |-  ( ph -> F : X --> U_ k e. X ( A (,) B ) )
11 ioossre 
 |-  ( A (,) B ) C_ RR
12 11 rgenw 
 |-  A. k e. X ( A (,) B ) C_ RR
13 12 a1i 
 |-  ( ph -> A. k e. X ( A (,) B ) C_ RR )
14 iunss 
 |-  ( U_ k e. X ( A (,) B ) C_ RR <-> A. k e. X ( A (,) B ) C_ RR )
15 13 14 sylibr 
 |-  ( ph -> U_ k e. X ( A (,) B ) C_ RR )
16 10 15 fssd 
 |-  ( ph -> F : X --> RR )
17 16 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( F ` k ) e. RR )
18 17 4 resubcld 
 |-  ( ( ph /\ k e. X ) -> ( ( F ` k ) - A ) e. RR )
19 4 rexrd 
 |-  ( ( ph /\ k e. X ) -> A e. RR* )
20 6 adantr 
 |-  ( ( ph /\ k e. X ) -> F e. X_ k e. X ( A (,) B ) )
21 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
22 fvixp2 
 |-  ( ( F e. X_ k e. X ( A (,) B ) /\ k e. X ) -> ( F ` k ) e. ( A (,) B ) )
23 20 21 22 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( F ` k ) e. ( A (,) B ) )
24 ioogtlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( F ` k ) e. ( A (,) B ) ) -> A < ( F ` k ) )
25 19 5 23 24 syl3anc 
 |-  ( ( ph /\ k e. X ) -> A < ( F ` k ) )
26 4 17 posdifd 
 |-  ( ( ph /\ k e. X ) -> ( A < ( F ` k ) <-> 0 < ( ( F ` k ) - A ) ) )
27 25 26 mpbid 
 |-  ( ( ph /\ k e. X ) -> 0 < ( ( F ` k ) - A ) )
28 18 27 elrpd 
 |-  ( ( ph /\ k e. X ) -> ( ( F ` k ) - A ) e. RR+ )
29 1 8 28 rnmptssd 
 |-  ( ph -> ran ( k e. X |-> ( ( F ` k ) - A ) ) C_ RR+ )
30 ltso 
 |-  < Or RR
31 30 a1i 
 |-  ( ph -> < Or RR )
32 8 rnmptfi 
 |-  ( X e. Fin -> ran ( k e. X |-> ( ( F ` k ) - A ) ) e. Fin )
33 2 32 syl 
 |-  ( ph -> ran ( k e. X |-> ( ( F ` k ) - A ) ) e. Fin )
34 1 18 8 3 rnmptn0 
 |-  ( ph -> ran ( k e. X |-> ( ( F ` k ) - A ) ) =/= (/) )
35 1 8 18 rnmptssd 
 |-  ( ph -> ran ( k e. X |-> ( ( F ` k ) - A ) ) C_ RR )
36 fiinfcl 
 |-  ( ( < Or RR /\ ( ran ( k e. X |-> ( ( F ` k ) - A ) ) e. Fin /\ ran ( k e. X |-> ( ( F ` k ) - A ) ) =/= (/) /\ ran ( k e. X |-> ( ( F ` k ) - A ) ) C_ RR ) ) -> inf ( ran ( k e. X |-> ( ( F ` k ) - A ) ) , RR , < ) e. ran ( k e. X |-> ( ( F ` k ) - A ) ) )
37 31 33 34 35 36 syl13anc 
 |-  ( ph -> inf ( ran ( k e. X |-> ( ( F ` k ) - A ) ) , RR , < ) e. ran ( k e. X |-> ( ( F ` k ) - A ) ) )
38 7 37 eqeltrid 
 |-  ( ph -> C e. ran ( k e. X |-> ( ( F ` k ) - A ) ) )
39 29 38 sseldd 
 |-  ( ph -> C e. RR+ )
40 rpgtrecnn 
 |-  ( C e. RR+ -> E. n e. NN ( 1 / n ) < C )
41 39 40 syl 
 |-  ( ph -> E. n e. NN ( 1 / n ) < C )
42 6 elexd 
 |-  ( ph -> F e. _V )
43 42 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) -> F e. _V )
44 10 ffnd 
 |-  ( ph -> F Fn X )
45 44 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) -> F Fn X )
46 nfv 
 |-  F/ k n e. NN
47 1 46 nfan 
 |-  F/ k ( ph /\ n e. NN )
48 nfcv 
 |-  F/_ k ( 1 / n )
49 nfcv 
 |-  F/_ k <
50 nfmpt1 
 |-  F/_ k ( k e. X |-> ( ( F ` k ) - A ) )
51 50 nfrn 
 |-  F/_ k ran ( k e. X |-> ( ( F ` k ) - A ) )
52 nfcv 
 |-  F/_ k RR
53 51 52 49 nfinf 
 |-  F/_ k inf ( ran ( k e. X |-> ( ( F ` k ) - A ) ) , RR , < )
54 7 53 nfcxfr 
 |-  F/_ k C
55 48 49 54 nfbr 
 |-  F/ k ( 1 / n ) < C
56 47 55 nfan 
 |-  F/ k ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C )
57 4 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A e. RR )
58 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
59 58 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR )
60 57 59 readdcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A + ( 1 / n ) ) e. RR )
61 60 rexrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A + ( 1 / n ) ) e. RR* )
62 61 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( A + ( 1 / n ) ) e. RR* )
63 5 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> B e. RR* )
64 63 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> B e. RR* )
65 ressxr 
 |-  RR C_ RR*
66 65 a1i 
 |-  ( ph -> RR C_ RR* )
67 16 66 fssd 
 |-  ( ph -> F : X --> RR* )
68 67 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) -> F : X --> RR* )
69 68 ffvelrnda 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( F ` k ) e. RR* )
70 60 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( A + ( 1 / n ) ) e. RR )
71 17 ad4ant14 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( F ` k ) e. RR )
72 59 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( 1 / n ) e. RR )
73 35 38 sseldd 
 |-  ( ph -> C e. RR )
74 73 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> C e. RR )
75 18 ad4ant14 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( ( F ` k ) - A ) e. RR )
76 simplr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( 1 / n ) < C )
77 35 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ran ( k e. X |-> ( ( F ` k ) - A ) ) C_ RR )
78 33 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ran ( k e. X |-> ( ( F ` k ) - A ) ) e. Fin )
79 id 
 |-  ( k e. X -> k e. X )
80 ovexd 
 |-  ( k e. X -> ( ( F ` k ) - A ) e. _V )
81 8 elrnmpt1 
 |-  ( ( k e. X /\ ( ( F ` k ) - A ) e. _V ) -> ( ( F ` k ) - A ) e. ran ( k e. X |-> ( ( F ` k ) - A ) ) )
82 79 80 81 syl2anc 
 |-  ( k e. X -> ( ( F ` k ) - A ) e. ran ( k e. X |-> ( ( F ` k ) - A ) ) )
83 82 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( F ` k ) - A ) e. ran ( k e. X |-> ( ( F ` k ) - A ) ) )
84 infrefilb 
 |-  ( ( ran ( k e. X |-> ( ( F ` k ) - A ) ) C_ RR /\ ran ( k e. X |-> ( ( F ` k ) - A ) ) e. Fin /\ ( ( F ` k ) - A ) e. ran ( k e. X |-> ( ( F ` k ) - A ) ) ) -> inf ( ran ( k e. X |-> ( ( F ` k ) - A ) ) , RR , < ) <_ ( ( F ` k ) - A ) )
85 77 78 83 84 syl3anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> inf ( ran ( k e. X |-> ( ( F ` k ) - A ) ) , RR , < ) <_ ( ( F ` k ) - A ) )
86 7 85 eqbrtrid 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> C <_ ( ( F ` k ) - A ) )
87 86 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> C <_ ( ( F ` k ) - A ) )
88 72 74 75 76 87 ltletrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( 1 / n ) < ( ( F ` k ) - A ) )
89 57 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> A e. RR )
90 89 72 71 ltaddsub2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( ( A + ( 1 / n ) ) < ( F ` k ) <-> ( 1 / n ) < ( ( F ` k ) - A ) ) )
91 88 90 mpbird 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( A + ( 1 / n ) ) < ( F ` k ) )
92 70 71 91 ltled 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( A + ( 1 / n ) ) <_ ( F ` k ) )
93 iooltub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( F ` k ) e. ( A (,) B ) ) -> ( F ` k ) < B )
94 19 5 23 93 syl3anc 
 |-  ( ( ph /\ k e. X ) -> ( F ` k ) < B )
95 94 ad4ant14 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( F ` k ) < B )
96 62 64 69 92 95 elicod 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) /\ k e. X ) -> ( F ` k ) e. ( ( A + ( 1 / n ) ) [,) B ) )
97 96 ex 
 |-  ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) -> ( k e. X -> ( F ` k ) e. ( ( A + ( 1 / n ) ) [,) B ) ) )
98 56 97 ralrimi 
 |-  ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) -> A. k e. X ( F ` k ) e. ( ( A + ( 1 / n ) ) [,) B ) )
99 43 45 98 3jca 
 |-  ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) -> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( ( A + ( 1 / n ) ) [,) B ) ) )
100 elixp2 
 |-  ( F e. X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) <-> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( ( A + ( 1 / n ) ) [,) B ) ) )
101 99 100 sylibr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( 1 / n ) < C ) -> F e. X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) )
102 101 ex 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1 / n ) < C -> F e. X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) ) )
103 102 reximdva 
 |-  ( ph -> ( E. n e. NN ( 1 / n ) < C -> E. n e. NN F e. X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) ) )
104 41 103 mpd 
 |-  ( ph -> E. n e. NN F e. X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) )
105 eliun 
 |-  ( F e. U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) <-> E. n e. NN F e. X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) )
106 104 105 sylibr 
 |-  ( ph -> F e. U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) )