Metamath Proof Explorer

Theorem iunhoiioo

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

Ref Expression
Hypotheses iunhoiioo.k 
|- F/ k ph
iunhoiioo.x 
|- ( ph -> X e. Fin )
iunhoiioo.a 
|- ( ( ph /\ k e. X ) -> A e. RR )
iunhoiioo.b 
|- ( ( ph /\ k e. X ) -> B e. RR* )
Assertion iunhoiioo 
|- ( ph -> U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) = X_ k e. X ( A (,) B ) )

Proof

Step Hyp Ref Expression
1 iunhoiioo.k 
 |-  F/ k ph
2 iunhoiioo.x 
 |-  ( ph -> X e. Fin )
3 iunhoiioo.a 
 |-  ( ( ph /\ k e. X ) -> A e. RR )
4 iunhoiioo.b 
 |-  ( ( ph /\ k e. X ) -> B e. RR* )
5 nnn0 
 |-  NN =/= (/)
6 iunconst 
 |-  ( NN =/= (/) -> U_ n e. NN { (/) } = { (/) } )
7 5 6 ax-mp 
 |-  U_ n e. NN { (/) } = { (/) }
8 7 a1i 
 |-  ( X = (/) -> U_ n e. NN { (/) } = { (/) } )
9 ixpeq1 
 |-  ( X = (/) -> X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) = X_ k e. (/) ( ( A + ( 1 / n ) ) [,) B ) )
10 ixp0x 
 |-  X_ k e. (/) ( ( A + ( 1 / n ) ) [,) B ) = { (/) }
11 10 a1i 
 |-  ( X = (/) -> X_ k e. (/) ( ( A + ( 1 / n ) ) [,) B ) = { (/) } )
12 9 11 eqtrd 
 |-  ( X = (/) -> X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) = { (/) } )
13 12 adantr 
 |-  ( ( X = (/) /\ n e. NN ) -> X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) = { (/) } )
14 13 iuneq2dv 
 |-  ( X = (/) -> U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) = U_ n e. NN { (/) } )
15 ixpeq1 
 |-  ( X = (/) -> X_ k e. X ( A (,) B ) = X_ k e. (/) ( A (,) B ) )
16 ixp0x 
 |-  X_ k e. (/) ( A (,) B ) = { (/) }
17 16 a1i 
 |-  ( X = (/) -> X_ k e. (/) ( A (,) B ) = { (/) } )
18 15 17 eqtrd 
 |-  ( X = (/) -> X_ k e. X ( A (,) B ) = { (/) } )
19 8 14 18 3eqtr4d 
 |-  ( X = (/) -> U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) = X_ k e. X ( A (,) B ) )
20 19 adantl 
 |-  ( ( ph /\ X = (/) ) -> U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) = X_ k e. X ( A (,) B ) )
21 nfv 
 |-  F/ k n e. NN
22 1 21 nfan 
 |-  F/ k ( ph /\ n e. NN )
23 3 rexrd 
 |-  ( ( ph /\ k e. X ) -> A e. RR* )
24 23 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A e. RR* )
25 4 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> B e. RR* )
26 3 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A e. RR )
27 nnrp 
 |-  ( n e. NN -> n e. RR+ )
28 27 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> n e. RR+ )
29 28 rpreccld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( 1 / n ) e. RR+ )
30 26 29 ltaddrpd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> A < ( A + ( 1 / n ) ) )
31 4 xrleidd 
 |-  ( ( ph /\ k e. X ) -> B <_ B )
32 31 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> B <_ B )
33 icossioo 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A < ( A + ( 1 / n ) ) /\ B <_ B ) ) -> ( ( A + ( 1 / n ) ) [,) B ) C_ ( A (,) B ) )
34 24 25 30 32 33 syl22anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( ( A + ( 1 / n ) ) [,) B ) C_ ( A (,) B ) )
35 22 34 ixpssixp 
 |-  ( ( ph /\ n e. NN ) -> X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) C_ X_ k e. X ( A (,) B ) )
36 35 ralrimiva 
 |-  ( ph -> A. n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) C_ X_ k e. X ( A (,) B ) )
37 iunss 
 |-  ( U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) C_ X_ k e. X ( A (,) B ) <-> A. n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) C_ X_ k e. X ( A (,) B ) )
38 36 37 sylibr 
 |-  ( ph -> U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) C_ X_ k e. X ( A (,) B ) )
39 38 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) C_ X_ k e. X ( A (,) B ) )
40 nfv 
 |-  F/ k -. X = (/)
41 1 40 nfan 
 |-  F/ k ( ph /\ -. X = (/) )
42 nfcv 
 |-  F/_ k f
43 nfixp1 
 |-  F/_ k X_ k e. X ( A (,) B )
44 42 43 nfel 
 |-  F/ k f e. X_ k e. X ( A (,) B )
45 41 44 nfan 
 |-  F/ k ( ( ph /\ -. X = (/) ) /\ f e. X_ k e. X ( A (,) B ) )
46 2 ad2antrr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. X_ k e. X ( A (,) B ) ) -> X e. Fin )
47 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
48 47 ad2antlr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. X_ k e. X ( A (,) B ) ) -> X =/= (/) )
49 3 ad4ant14 
 |-  ( ( ( ( ph /\ -. X = (/) ) /\ f e. X_ k e. X ( A (,) B ) ) /\ k e. X ) -> A e. RR )
50 4 ad4ant14 
 |-  ( ( ( ( ph /\ -. X = (/) ) /\ f e. X_ k e. X ( A (,) B ) ) /\ k e. X ) -> B e. RR* )
51 simpr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. X_ k e. X ( A (,) B ) ) -> f e. X_ k e. X ( A (,) B ) )
52 eqid 
 |-  inf ( ran ( k e. X |-> ( ( f ` k ) - A ) ) , RR , < ) = inf ( ran ( k e. X |-> ( ( f ` k ) - A ) ) , RR , < )
53 45 46 48 49 50 51 52 iunhoiioolem 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. X_ k e. X ( A (,) B ) ) -> f e. U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) )
54 39 53 eqelssd 
 |-  ( ( ph /\ -. X = (/) ) -> U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) = X_ k e. X ( A (,) B ) )
55 20 54 pm2.61dan 
 |-  ( ph -> U_ n e. NN X_ k e. X ( ( A + ( 1 / n ) ) [,) B ) = X_ k e. X ( A (,) B ) )