Metamath Proof Explorer


Theorem iinhoiicclem

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

Ref Expression
Hypotheses iinhoiicclem.k
|- F/ k ph
iinhoiicclem.a
|- ( ( ph /\ k e. X ) -> A e. RR )
iinhoiicclem.b
|- ( ( ph /\ k e. X ) -> B e. RR )
iinhoiicclem.f
|- ( ph -> F e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
Assertion iinhoiicclem
|- ( ph -> F e. X_ k e. X ( A [,] B ) )

Proof

Step Hyp Ref Expression
1 iinhoiicclem.k
 |-  F/ k ph
2 iinhoiicclem.a
 |-  ( ( ph /\ k e. X ) -> A e. RR )
3 iinhoiicclem.b
 |-  ( ( ph /\ k e. X ) -> B e. RR )
4 iinhoiicclem.f
 |-  ( ph -> F e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
5 4 elexd
 |-  ( ph -> F e. _V )
6 1nn
 |-  1 e. NN
7 6 a1i
 |-  ( ph -> 1 e. NN )
8 peano2re
 |-  ( B e. RR -> ( B + 1 ) e. RR )
9 3 8 syl
 |-  ( ( ph /\ k e. X ) -> ( B + 1 ) e. RR )
10 9 rexrd
 |-  ( ( ph /\ k e. X ) -> ( B + 1 ) e. RR* )
11 icossre
 |-  ( ( A e. RR /\ ( B + 1 ) e. RR* ) -> ( A [,) ( B + 1 ) ) C_ RR )
12 2 10 11 syl2anc
 |-  ( ( ph /\ k e. X ) -> ( A [,) ( B + 1 ) ) C_ RR )
13 1 12 ixpssixp
 |-  ( ph -> X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X RR )
14 oveq2
 |-  ( n = 1 -> ( 1 / n ) = ( 1 / 1 ) )
15 1div1e1
 |-  ( 1 / 1 ) = 1
16 15 a1i
 |-  ( n = 1 -> ( 1 / 1 ) = 1 )
17 14 16 eqtrd
 |-  ( n = 1 -> ( 1 / n ) = 1 )
18 17 oveq2d
 |-  ( n = 1 -> ( B + ( 1 / n ) ) = ( B + 1 ) )
19 18 oveq2d
 |-  ( n = 1 -> ( A [,) ( B + ( 1 / n ) ) ) = ( A [,) ( B + 1 ) ) )
20 19 ixpeq2dv
 |-  ( n = 1 -> X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) = X_ k e. X ( A [,) ( B + 1 ) ) )
21 20 sseq1d
 |-  ( n = 1 -> ( X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR <-> X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X RR ) )
22 21 rspcev
 |-  ( ( 1 e. NN /\ X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X RR ) -> E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR )
23 7 13 22 syl2anc
 |-  ( ph -> E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR )
24 iinss
 |-  ( E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR )
25 23 24 syl
 |-  ( ph -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR )
26 25 4 sseldd
 |-  ( ph -> F e. X_ k e. X RR )
27 elixpconstg
 |-  ( F e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) -> ( F e. X_ k e. X RR <-> F : X --> RR ) )
28 4 27 syl
 |-  ( ph -> ( F e. X_ k e. X RR <-> F : X --> RR ) )
29 26 28 mpbid
 |-  ( ph -> F : X --> RR )
30 29 ffnd
 |-  ( ph -> F Fn X )
31 29 ffvelrnda
 |-  ( ( ph /\ k e. X ) -> ( F ` k ) e. RR )
32 2 rexrd
 |-  ( ( ph /\ k e. X ) -> A e. RR* )
33 ssid
 |-  X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X ( A [,) ( B + 1 ) )
34 33 a1i
 |-  ( ph -> X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) )
35 20 sseq1d
 |-  ( n = 1 -> ( X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) <-> X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) ) )
36 35 rspcev
 |-  ( ( 1 e. NN /\ X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) ) -> E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) )
37 7 34 36 syl2anc
 |-  ( ph -> E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) )
38 iinss
 |-  ( E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) )
39 37 38 syl
 |-  ( ph -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) )
40 39 4 sseldd
 |-  ( ph -> F e. X_ k e. X ( A [,) ( B + 1 ) ) )
41 40 adantr
 |-  ( ( ph /\ k e. X ) -> F e. X_ k e. X ( A [,) ( B + 1 ) ) )
42 simpr
 |-  ( ( ph /\ k e. X ) -> k e. X )
43 fvixp2
 |-  ( ( F e. X_ k e. X ( A [,) ( B + 1 ) ) /\ k e. X ) -> ( F ` k ) e. ( A [,) ( B + 1 ) ) )
44 41 42 43 syl2anc
 |-  ( ( ph /\ k e. X ) -> ( F ` k ) e. ( A [,) ( B + 1 ) ) )
45 icogelb
 |-  ( ( A e. RR* /\ ( B + 1 ) e. RR* /\ ( F ` k ) e. ( A [,) ( B + 1 ) ) ) -> A <_ ( F ` k ) )
46 32 10 44 45 syl3anc
 |-  ( ( ph /\ k e. X ) -> A <_ ( F ` k ) )
47 31 adantr
 |-  ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( F ` k ) e. RR )
48 3 adantr
 |-  ( ( ( ph /\ k e. X ) /\ n e. NN ) -> B e. RR )
49 nnrecre
 |-  ( n e. NN -> ( 1 / n ) e. RR )
50 49 adantl
 |-  ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( 1 / n ) e. RR )
51 48 50 readdcld
 |-  ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( B + ( 1 / n ) ) e. RR )
52 32 adantr
 |-  ( ( ( ph /\ k e. X ) /\ n e. NN ) -> A e. RR* )
53 ressxr
 |-  RR C_ RR*
54 53 51 sseldi
 |-  ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( B + ( 1 / n ) ) e. RR* )
55 eliin
 |-  ( F e. _V -> ( F e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) <-> A. n e. NN F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) )
56 5 55 syl
 |-  ( ph -> ( F e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) <-> A. n e. NN F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) )
57 4 56 mpbid
 |-  ( ph -> A. n e. NN F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
58 57 r19.21bi
 |-  ( ( ph /\ n e. NN ) -> F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
59 elixp2
 |-  ( F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) <-> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) ) )
60 58 59 sylib
 |-  ( ( ph /\ n e. NN ) -> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) ) )
61 60 simp3d
 |-  ( ( ph /\ n e. NN ) -> A. k e. X ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) )
62 61 r19.21bi
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) )
63 62 an32s
 |-  ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) )
64 icoltub
 |-  ( ( A e. RR* /\ ( B + ( 1 / n ) ) e. RR* /\ ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) ) -> ( F ` k ) < ( B + ( 1 / n ) ) )
65 52 54 63 64 syl3anc
 |-  ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( F ` k ) < ( B + ( 1 / n ) ) )
66 47 51 65 ltled
 |-  ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( F ` k ) <_ ( B + ( 1 / n ) ) )
67 66 ralrimiva
 |-  ( ( ph /\ k e. X ) -> A. n e. NN ( F ` k ) <_ ( B + ( 1 / n ) ) )
68 nfv
 |-  F/ n ( ph /\ k e. X )
69 53 31 sseldi
 |-  ( ( ph /\ k e. X ) -> ( F ` k ) e. RR* )
70 68 69 3 xrralrecnnle
 |-  ( ( ph /\ k e. X ) -> ( ( F ` k ) <_ B <-> A. n e. NN ( F ` k ) <_ ( B + ( 1 / n ) ) ) )
71 67 70 mpbird
 |-  ( ( ph /\ k e. X ) -> ( F ` k ) <_ B )
72 2 3 31 46 71 eliccd
 |-  ( ( ph /\ k e. X ) -> ( F ` k ) e. ( A [,] B ) )
73 72 ex
 |-  ( ph -> ( k e. X -> ( F ` k ) e. ( A [,] B ) ) )
74 1 73 ralrimi
 |-  ( ph -> A. k e. X ( F ` k ) e. ( A [,] B ) )
75 5 30 74 3jca
 |-  ( ph -> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( A [,] B ) ) )
76 elixp2
 |-  ( F e. X_ k e. X ( A [,] B ) <-> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( A [,] B ) ) )
77 75 76 sylibr
 |-  ( ph -> F e. X_ k e. X ( A [,] B ) )