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 bilani 
 |-  ( ( 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 ) ) ) )
11 nfcv 
 |-  F/_ k f
12 nfcv 
 |-  F/_ k NN
13 nfixp1 
 |-  F/_ k X_ k e. X ( A [,) ( B + ( 1 / m ) ) )
14 12 13 nfiin 
 |-  F/_ k |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) )
15 11 14 nfel 
 |-  F/ k f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) )
16 1 15 nfan 
 |-  F/ k ( ph /\ f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) )
17 2 adantlr 
 |-  ( ( ( ph /\ f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) ) /\ k e. X ) -> A e. RR )
18 3 adantlr 
 |-  ( ( ( ph /\ f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) ) /\ k e. X ) -> B e. RR )
19 9 bilanri 
 |-  ( ( 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 ) ) ) )
20 16 17 18 19 iinhoiicclem 
 |-  ( ( ph /\ f e. |^|_ m e. NN X_ k e. X ( A [,) ( B + ( 1 / m ) ) ) ) -> f e. X_ k e. X ( A [,] B ) )
21 10 20 syldan 
 |-  ( ( ph /\ f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) -> f e. X_ k e. X ( A [,] B ) )
22 21 ralrimiva 
 |-  ( ph -> A. f e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) f e. X_ k e. X ( A [,] B ) )
23 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 ) )
24 22 23 sylibr 
 |-  ( ph -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,] B ) )
25 nfv 
 |-  F/ k n e. NN
26 1 25 nfan 
 |-  F/ k ( ph /\ n e. NN )
27 2 rexrd 
 |-  ( ( ph /\ k e. X ) -> A e. RR* )
28 27 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A e. RR* )
29 3 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> B e. RR )
30 nnrp 
 |-  ( n e. NN -> n e. RR+ )
31 30 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> n e. RR+ )
32 31 rpreccld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR+ )
33 32 rpred 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR )
34 29 33 readdcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B + ( 1 / n ) ) e. RR )
35 34 rexrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( B + ( 1 / n ) ) e. RR* )
36 2 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A e. RR )
37 36 leidd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A <_ A )
38 29 32 ltaddrpd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> B < ( B + ( 1 / n ) ) )
39 iccssico 
 |-  ( ( ( A e. RR* /\ ( B + ( 1 / n ) ) e. RR* ) /\ ( A <_ A /\ B < ( B + ( 1 / n ) ) ) ) -> ( A [,] B ) C_ ( A [,) ( B + ( 1 / n ) ) ) )
40 28 35 37 38 39 syl22anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( A [,] B ) C_ ( A [,) ( B + ( 1 / n ) ) ) )
41 26 40 ixpssixp 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( A [,] B ) C_ X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
42 41 ralrimiva 
 |-  ( ph -> A. n e. NN X_ k e. X ( A [,] B ) C_ X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
43 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 ) ) ) )
44 42 43 sylibr 
 |-  ( ph -> X_ k e. X ( A [,] B ) C_ |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) )
45 24 44 eqssd 
 |-  ( ph -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) = X_ k e. X ( A [,] B ) )