Metamath Proof Explorer

Theorem hoimbl

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, 24-Dec-2020)

Ref Expression
Hypotheses hoimbl.x 
|- ( ph -> X e. Fin )
hoimbl.s 
|- S = dom ( voln ` X )
hoimbl.a 
|- ( ph -> A : X --> RR )
hoimbl.b 
|- ( ph -> B : X --> RR )
Assertion hoimbl 
|- ( ph -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) e. S )

Proof

Step Hyp Ref Expression
1 hoimbl.x 
 |-  ( ph -> X e. Fin )
2 hoimbl.s 
 |-  S = dom ( voln ` X )
3 hoimbl.a 
 |-  ( ph -> A : X --> RR )
4 hoimbl.b 
 |-  ( ph -> B : X --> RR )
5 1 adantr 
 |-  ( ( ph /\ X = (/) ) -> X e. Fin )
6 5 rrnmbl 
 |-  ( ( ph /\ X = (/) ) -> ( RR ^m X ) e. dom ( voln ` X ) )
7 reex 
 |-  RR e. _V
8 mapdm0 
 |-  ( RR e. _V -> ( RR ^m (/) ) = { (/) } )
9 7 8 ax-mp 
 |-  ( RR ^m (/) ) = { (/) }
10 9 eqcomi 
 |-  { (/) } = ( RR ^m (/) )
11 10 a1i 
 |-  ( X = (/) -> { (/) } = ( RR ^m (/) ) )
12 id 
 |-  ( X = (/) -> X = (/) )
13 12 ixpeq1d 
 |-  ( X = (/) -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) = X_ i e. (/) ( ( A ` i ) [,) ( B ` i ) ) )
14 ixp0x 
 |-  X_ i e. (/) ( ( A ` i ) [,) ( B ` i ) ) = { (/) }
15 14 a1i 
 |-  ( X = (/) -> X_ i e. (/) ( ( A ` i ) [,) ( B ` i ) ) = { (/) } )
16 13 15 eqtrd 
 |-  ( X = (/) -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) = { (/) } )
17 oveq2 
 |-  ( X = (/) -> ( RR ^m X ) = ( RR ^m (/) ) )
18 11 16 17 3eqtr4d 
 |-  ( X = (/) -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) = ( RR ^m X ) )
19 18 adantl 
 |-  ( ( ph /\ X = (/) ) -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) = ( RR ^m X ) )
20 2 a1i 
 |-  ( ( ph /\ X = (/) ) -> S = dom ( voln ` X ) )
21 19 20 eleq12d 
 |-  ( ( ph /\ X = (/) ) -> ( X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) e. S <-> ( RR ^m X ) e. dom ( voln ` X ) ) )
22 6 21 mpbird 
 |-  ( ( ph /\ X = (/) ) -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) e. S )
23 1 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> X e. Fin )
24 12 necon3bi 
 |-  ( -. X = (/) -> X =/= (/) )
25 24 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
26 3 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> A : X --> RR )
27 4 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> B : X --> RR )
28 id 
 |-  ( w = x -> w = x )
29 eqidd 
 |-  ( w = x -> RR = RR )
30 28 ixpeq1d 
 |-  ( w = x -> X_ j e. w if ( j = h , ( -oo (,) z ) , RR ) = X_ j e. x if ( j = h , ( -oo (,) z ) , RR ) )
31 eqeq1 
 |-  ( j = i -> ( j = h <-> i = h ) )
32 31 ifbid 
 |-  ( j = i -> if ( j = h , ( -oo (,) z ) , RR ) = if ( i = h , ( -oo (,) z ) , RR ) )
33 32 cbvixpv 
 |-  X_ j e. x if ( j = h , ( -oo (,) z ) , RR ) = X_ i e. x if ( i = h , ( -oo (,) z ) , RR )
34 33 a1i 
 |-  ( w = x -> X_ j e. x if ( j = h , ( -oo (,) z ) , RR ) = X_ i e. x if ( i = h , ( -oo (,) z ) , RR ) )
35 30 34 eqtrd 
 |-  ( w = x -> X_ j e. w if ( j = h , ( -oo (,) z ) , RR ) = X_ i e. x if ( i = h , ( -oo (,) z ) , RR ) )
36 28 29 35 mpoeq123dv 
 |-  ( w = x -> ( h e. w , z e. RR |-> X_ j e. w if ( j = h , ( -oo (,) z ) , RR ) ) = ( h e. x , z e. RR |-> X_ i e. x if ( i = h , ( -oo (,) z ) , RR ) ) )
37 eqeq2 
 |-  ( h = l -> ( i = h <-> i = l ) )
38 37 ifbid 
 |-  ( h = l -> if ( i = h , ( -oo (,) z ) , RR ) = if ( i = l , ( -oo (,) z ) , RR ) )
39 38 ixpeq2dv 
 |-  ( h = l -> X_ i e. x if ( i = h , ( -oo (,) z ) , RR ) = X_ i e. x if ( i = l , ( -oo (,) z ) , RR ) )
40 oveq2 
 |-  ( z = y -> ( -oo (,) z ) = ( -oo (,) y ) )
41 40 ifeq1d 
 |-  ( z = y -> if ( i = l , ( -oo (,) z ) , RR ) = if ( i = l , ( -oo (,) y ) , RR ) )
42 41 ixpeq2dv 
 |-  ( z = y -> X_ i e. x if ( i = l , ( -oo (,) z ) , RR ) = X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) )
43 39 42 cbvmpov 
 |-  ( h e. x , z e. RR |-> X_ i e. x if ( i = h , ( -oo (,) z ) , RR ) ) = ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) )
44 43 a1i 
 |-  ( w = x -> ( h e. x , z e. RR |-> X_ i e. x if ( i = h , ( -oo (,) z ) , RR ) ) = ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) )
45 36 44 eqtrd 
 |-  ( w = x -> ( h e. w , z e. RR |-> X_ j e. w if ( j = h , ( -oo (,) z ) , RR ) ) = ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) )
46 45 cbvmptv 
 |-  ( w e. Fin |-> ( h e. w , z e. RR |-> X_ j e. w if ( j = h , ( -oo (,) z ) , RR ) ) ) = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) )
47 23 25 2 26 27 46 hoimbllem 
 |-  ( ( ph /\ -. X = (/) ) -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) e. S )
48 22 47 pm2.61dan 
 |-  ( ph -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) e. S )