Metamath Proof Explorer

Theorem hoimbl2

Description: Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses hoimbl2.k 
|- F/ k ph
hoimbl2.x 
|- ( ph -> X e. Fin )
hoimbl2.s 
|- S = dom ( voln ` X )
hoimbl2.a 
|- ( ( ph /\ k e. X ) -> A e. RR )
hoimbl2.b 
|- ( ( ph /\ k e. X ) -> B e. RR )
Assertion hoimbl2 
|- ( ph -> X_ k e. X ( A [,) B ) e. S )

Proof

Step Hyp Ref Expression
1 hoimbl2.k 
 |-  F/ k ph
2 hoimbl2.x 
 |-  ( ph -> X e. Fin )
3 hoimbl2.s 
 |-  S = dom ( voln ` X )
4 hoimbl2.a 
 |-  ( ( ph /\ k e. X ) -> A e. RR )
5 hoimbl2.b 
 |-  ( ( ph /\ k e. X ) -> B e. RR )
6 simpr 
 |-  ( ( ph /\ j e. X ) -> j e. X )
7 nfv 
 |-  F/ k j e. X
8 1 7 nfan 
 |-  F/ k ( ph /\ j e. X )
9 nfcsb1v 
 |-  F/_ k [_ j / k ]_ A
10 nfcv 
 |-  F/_ k RR
11 9 10 nfel 
 |-  F/ k [_ j / k ]_ A e. RR
12 8 11 nfim 
 |-  F/ k ( ( ph /\ j e. X ) -> [_ j / k ]_ A e. RR )
13 eleq1w 
 |-  ( k = j -> ( k e. X <-> j e. X ) )
14 13 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. X ) <-> ( ph /\ j e. X ) ) )
15 csbeq1a 
 |-  ( k = j -> A = [_ j / k ]_ A )
16 15 eleq1d 
 |-  ( k = j -> ( A e. RR <-> [_ j / k ]_ A e. RR ) )
17 14 16 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. X ) -> A e. RR ) <-> ( ( ph /\ j e. X ) -> [_ j / k ]_ A e. RR ) ) )
18 12 17 4 chvarfv 
 |-  ( ( ph /\ j e. X ) -> [_ j / k ]_ A e. RR )
19 nfcv 
 |-  F/_ k j
20 19 nfcsb1 
 |-  F/_ k [_ j / k ]_ A
21 eqid 
 |-  ( k e. X |-> A ) = ( k e. X |-> A )
22 19 20 15 21 fvmptf 
 |-  ( ( j e. X /\ [_ j / k ]_ A e. RR ) -> ( ( k e. X |-> A ) ` j ) = [_ j / k ]_ A )
23 6 18 22 syl2anc 
 |-  ( ( ph /\ j e. X ) -> ( ( k e. X |-> A ) ` j ) = [_ j / k ]_ A )
24 19 nfcsb1 
 |-  F/_ k [_ j / k ]_ B
25 24 10 nfel 
 |-  F/ k [_ j / k ]_ B e. RR
26 8 25 nfim 
 |-  F/ k ( ( ph /\ j e. X ) -> [_ j / k ]_ B e. RR )
27 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
28 27 eleq1d 
 |-  ( k = j -> ( B e. RR <-> [_ j / k ]_ B e. RR ) )
29 14 28 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. X ) -> B e. RR ) <-> ( ( ph /\ j e. X ) -> [_ j / k ]_ B e. RR ) ) )
30 26 29 5 chvarfv 
 |-  ( ( ph /\ j e. X ) -> [_ j / k ]_ B e. RR )
31 eqid 
 |-  ( k e. X |-> B ) = ( k e. X |-> B )
32 19 24 27 31 fvmptf 
 |-  ( ( j e. X /\ [_ j / k ]_ B e. RR ) -> ( ( k e. X |-> B ) ` j ) = [_ j / k ]_ B )
33 6 30 32 syl2anc 
 |-  ( ( ph /\ j e. X ) -> ( ( k e. X |-> B ) ` j ) = [_ j / k ]_ B )
34 23 33 oveq12d 
 |-  ( ( ph /\ j e. X ) -> ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) = ( [_ j / k ]_ A [,) [_ j / k ]_ B ) )
35 34 ixpeq2dva 
 |-  ( ph -> X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) = X_ j e. X ( [_ j / k ]_ A [,) [_ j / k ]_ B ) )
36 nfcv 
 |-  F/_ j ( A [,) B )
37 nfcv 
 |-  F/_ k [,)
38 9 37 24 nfov 
 |-  F/_ k ( [_ j / k ]_ A [,) [_ j / k ]_ B )
39 15 27 oveq12d 
 |-  ( k = j -> ( A [,) B ) = ( [_ j / k ]_ A [,) [_ j / k ]_ B ) )
40 36 38 39 cbvixp 
 |-  X_ k e. X ( A [,) B ) = X_ j e. X ( [_ j / k ]_ A [,) [_ j / k ]_ B )
41 40 eqcomi 
 |-  X_ j e. X ( [_ j / k ]_ A [,) [_ j / k ]_ B ) = X_ k e. X ( A [,) B )
42 41 a1i 
 |-  ( ph -> X_ j e. X ( [_ j / k ]_ A [,) [_ j / k ]_ B ) = X_ k e. X ( A [,) B ) )
43 35 42 eqtr2d 
 |-  ( ph -> X_ k e. X ( A [,) B ) = X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) )
44 1 4 21 fmptdf 
 |-  ( ph -> ( k e. X |-> A ) : X --> RR )
45 1 5 31 fmptdf 
 |-  ( ph -> ( k e. X |-> B ) : X --> RR )
46 2 3 44 45 hoimbl 
 |-  ( ph -> X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) e. S )
47 43 46 eqeltrd 
 |-  ( ph -> X_ k e. X ( A [,) B ) e. S )