Metamath Proof Explorer

Theorem iinhoiicc

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

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

Proof

Step Hyp Ref Expression
1 iunhoiicc.k 
 |-  F/ k ph
2 iunhoiicc.a 
 |-  ( ( ph /\ k e. X ) -> A e. RR )
3 iunhoiicc.b 
 |-  ( ( ph /\ k e. X ) -> B e. RR )
4 oveq2 
 |-  ( n = m -> ( 1 / n ) = ( 1 / m ) )
5 4 oveq2d 
 |-  ( n = m -> ( B + ( 1 / n ) ) = ( B + ( 1 / m ) ) )
6 5 oveq2d 
 |-  ( n = m -> ( A [,) ( B + ( 1 / n ) ) ) = ( A [,) ( B + ( 1 / m ) ) ) )
7 6 ixpeq2dv 
 |-  ( n = m -> X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) = X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) )
8 7 cbviinv 
 |-  |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) = |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) )
9 8 eleq2i 
 |-  ( f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) <-> f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) )
10 9 biimpi 
 |-  ( f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) -> f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) )
11 10 adantl 
 |-  ( ( ph /\ f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) -> f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) )
12 nfcv 
 |-  F/_ k f
13 nfcv 
 |-  F/_ k NN
14 nfixp1 
 |-  F/_ k X_ k e. X ( A [,) ( B + ( 1 / m ) ) )
15 13 14 nfiin 
 |-  F/_ k |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) )
16 12 15 nfel 
 |-  F/ k f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) )
17 1 16 nfan 
 |-  F/ k ( ph /\ f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) )
18 2 adantlr 
 |-  ( ( ( ph /\ f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) ) /\ k e. X ) -> A e. RR )
19 3 adantlr 
 |-  ( ( ( ph /\ f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) ) /\ k e. X ) -> B e. RR )
20 9 biimpri 
 |-  ( f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) -> f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
21 20 adantl 
 |-  ( ( ph /\ f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) ) -> f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
22 17 18 19 21 iinhoiicclem 
 |-  ( ( ph /\ f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) ) -> f e. X_ k e. X ( A [,] B ) )
23 11 22 syldan 
 |-  ( ( ph /\ f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) -> f e. X_ k e. X ( A [,] B ) )
24 23 ralrimiva 
 |-  ( ph -> A. f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) f e. X_ k e. X ( A [,] B ) )
25 dfss3 
 |-  ( |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,] B ) <-> A. f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) f e. X_ k e. X ( A [,] B ) )
26 24 25 sylibr 
 |-  ( ph -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,] B ) )
27 nfv 
 |-  F/ k n e. NN
28 1 27 nfan 
 |-  F/ k ( ph /\ n e. NN )
29 2 rexrd 
 |-  ( ( ph /\ k e. X ) -> A e. RR* )
30 29 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A e. RR* )
31 3 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> B e. RR )
32 nnrp 
 |-  ( n e. NN -> n e. RR+ )
33 32 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> n e. RR+ )
34 33 rpreccld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR+ )
35 34 rpred 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR )
36 31 35 readdcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B + ( 1 / n ) ) e. RR )
37 36 rexrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B + ( 1 / n ) ) e. RR* )
38 2 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A e. RR )
39 38 leidd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A <_ A )
40 31 34 ltaddrpd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> B < ( B + ( 1 / n ) ) )
41 iccssico 
 |-  ( ( ( A e. RR* /\ ( B + ( 1 / n ) ) e. RR* ) /\ ( A <_ A /\ B < ( B + ( 1 / n ) ) ) ) -> ( A [,] B ) C_ ( A [,) ( B + ( 1 / n ) ) ) )
42 30 37 39 40 41 syl22anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A [,] B ) C_ ( A [,) ( B + ( 1 / n ) ) ) )
43 28 42 ixpssixp 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( A [,] B ) C_ X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
44 43 ralrimiva 
 |-  ( ph -> A. n e. NN X_ k e. X ( A [,] B ) C_ X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
45 ssiin 
 |-  ( X_ k e. X ( A [,] B ) C_ |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) <-> A. n e. NN X_ k e. X ( A [,] B ) C_ X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
46 44 45 sylibr 
 |-  ( ph -> X_ k e. X ( A [,] B ) C_ |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
47 26 46 eqssd 
 |-  ( ph -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) = X_ k e. X ( A [,] B ) )