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 ffvelcdmda 
 |-  ( ( 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 sselid 
 |-  ( ( ( 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 sselid 
 |-  ( ( 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 ) )