Metamath Proof Explorer

Theorem opnvonmbllem2

Description: An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses opnvonmbllem2.x 
|- ( ph -> X e. Fin )
opnvonmbllem2.n 
|- S = dom ( voln ` X )
opnvonmbllem2.g 
|- ( ph -> G e. ( TopOpen ` ( RR^ ` X ) ) )
opnvonmbl.k 
|- K = { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G }
Assertion opnvonmbllem2 
|- ( ph -> G e. S )

Proof

Step Hyp Ref Expression
1 opnvonmbllem2.x 
 |-  ( ph -> X e. Fin )
2 opnvonmbllem2.n 
 |-  S = dom ( voln ` X )
3 opnvonmbllem2.g 
 |-  ( ph -> G e. ( TopOpen ` ( RR^ ` X ) ) )
4 opnvonmbl.k 
 |-  K = { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G }
5 eqid 
 |-  ( dist ` ( RR^ ` X ) ) = ( dist ` ( RR^ ` X ) )
6 5 rrxmetfi 
 |-  ( X e. Fin -> ( dist ` ( RR^ ` X ) ) e. ( Met ` ( RR ^m X ) ) )
7 1 6 syl 
 |-  ( ph -> ( dist ` ( RR^ ` X ) ) e. ( Met ` ( RR ^m X ) ) )
8 metxmet 
 |-  ( ( dist ` ( RR^ ` X ) ) e. ( Met ` ( RR ^m X ) ) -> ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) )
9 7 8 syl 
 |-  ( ph -> ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) )
10 9 adantr 
 |-  ( ( ph /\ x e. G ) -> ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) )
11 eqid 
 |-  ( RR^ ` X ) = ( RR^ ` X )
12 11 rrxval 
 |-  ( X e. Fin -> ( RR^ ` X ) = ( toCPreHil ` ( RRfld freeLMod X ) ) )
13 1 12 syl 
 |-  ( ph -> ( RR^ ` X ) = ( toCPreHil ` ( RRfld freeLMod X ) ) )
14 13 fveq2d 
 |-  ( ph -> ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) )
15 ovex 
 |-  ( RRfld freeLMod X ) e. _V
16 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod X ) ) = ( toCPreHil ` ( RRfld freeLMod X ) )
17 eqid 
 |-  ( dist ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) = ( dist ` ( toCPreHil ` ( RRfld freeLMod X ) ) )
18 eqid 
 |-  ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) = ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod X ) ) )
19 16 17 18 tcphtopn 
 |-  ( ( RRfld freeLMod X ) e. _V -> ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) = ( MetOpen ` ( dist ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) ) )
20 15 19 ax-mp 
 |-  ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) = ( MetOpen ` ( dist ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) )
21 20 a1i 
 |-  ( ph -> ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) = ( MetOpen ` ( dist ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) ) )
22 13 eqcomd 
 |-  ( ph -> ( toCPreHil ` ( RRfld freeLMod X ) ) = ( RR^ ` X ) )
23 22 fveq2d 
 |-  ( ph -> ( dist ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) = ( dist ` ( RR^ ` X ) ) )
24 23 fveq2d 
 |-  ( ph -> ( MetOpen ` ( dist ` ( toCPreHil ` ( RRfld freeLMod X ) ) ) ) = ( MetOpen ` ( dist ` ( RR^ ` X ) ) ) )
25 14 21 24 3eqtrd 
 |-  ( ph -> ( TopOpen ` ( RR^ ` X ) ) = ( MetOpen ` ( dist ` ( RR^ ` X ) ) ) )
26 3 25 eleqtrd 
 |-  ( ph -> G e. ( MetOpen ` ( dist ` ( RR^ ` X ) ) ) )
27 26 adantr 
 |-  ( ( ph /\ x e. G ) -> G e. ( MetOpen ` ( dist ` ( RR^ ` X ) ) ) )
28 simpr 
 |-  ( ( ph /\ x e. G ) -> x e. G )
29 eqid 
 |-  ( MetOpen ` ( dist ` ( RR^ ` X ) ) ) = ( MetOpen ` ( dist ` ( RR^ ` X ) ) )
30 29 mopni2 
 |-  ( ( ( dist ` ( RR^ ` X ) ) e. ( *Met ` ( RR ^m X ) ) /\ G e. ( MetOpen ` ( dist ` ( RR^ ` X ) ) ) /\ x e. G ) -> E. e e. RR+ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G )
31 10 27 28 30 syl3anc 
 |-  ( ( ph /\ x e. G ) -> E. e e. RR+ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G )
32 1 ad2antrr 
 |-  ( ( ( ph /\ x e. G ) /\ e e. RR+ ) -> X e. Fin )
33 eqid 
 |-  ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( RR^ ` X ) )
34 33 rrxtoponfi 
 |-  ( X e. Fin -> ( TopOpen ` ( RR^ ` X ) ) e. ( TopOn ` ( RR ^m X ) ) )
35 1 34 syl 
 |-  ( ph -> ( TopOpen ` ( RR^ ` X ) ) e. ( TopOn ` ( RR ^m X ) ) )
36 toponss 
 |-  ( ( ( TopOpen ` ( RR^ ` X ) ) e. ( TopOn ` ( RR ^m X ) ) /\ G e. ( TopOpen ` ( RR^ ` X ) ) ) -> G C_ ( RR ^m X ) )
37 35 3 36 syl2anc 
 |-  ( ph -> G C_ ( RR ^m X ) )
38 37 adantr 
 |-  ( ( ph /\ x e. G ) -> G C_ ( RR ^m X ) )
39 38 28 sseldd 
 |-  ( ( ph /\ x e. G ) -> x e. ( RR ^m X ) )
40 39 adantr 
 |-  ( ( ( ph /\ x e. G ) /\ e e. RR+ ) -> x e. ( RR ^m X ) )
41 simpr 
 |-  ( ( ( ph /\ x e. G ) /\ e e. RR+ ) -> e e. RR+ )
42 32 40 41 hoiqssbl 
 |-  ( ( ( ph /\ x e. G ) /\ e e. RR+ ) -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) )
43 42 3adant3 
 |-  ( ( ( ph /\ x e. G ) /\ e e. RR+ /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) -> E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) )
44 nfv 
 |-  F/ i ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G )
45 nfv 
 |-  F/ i ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) )
46 nfcv 
 |-  F/_ i x
47 nfixp1 
 |-  F/_ i X_ i e. X ( ( c ` i ) [,) ( d ` i ) )
48 46 47 nfel 
 |-  F/ i x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) )
49 nfcv 
 |-  F/_ i ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e )
50 47 49 nfss 
 |-  F/ i X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e )
51 48 50 nfan 
 |-  F/ i ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) )
52 44 45 51 nf3an 
 |-  F/ i ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) /\ ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) /\ ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) )
53 1 adantr 
 |-  ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) -> X e. Fin )
54 53 3ad2ant1 
 |-  ( ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) /\ ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) /\ ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) ) -> X e. Fin )
55 elmapi 
 |-  ( c e. ( QQ ^m X ) -> c : X --> QQ )
56 55 adantr 
 |-  ( ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) -> c : X --> QQ )
57 56 3ad2ant2 
 |-  ( ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) /\ ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) /\ ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) ) -> c : X --> QQ )
58 elmapi 
 |-  ( d e. ( QQ ^m X ) -> d : X --> QQ )
59 58 adantl 
 |-  ( ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) -> d : X --> QQ )
60 59 3ad2ant2 
 |-  ( ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) /\ ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) /\ ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) ) -> d : X --> QQ )
61 simp3r 
 |-  ( ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) /\ ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) /\ ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) ) -> X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) )
62 simp1r 
 |-  ( ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) /\ ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) /\ ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) ) -> ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G )
63 simp3l 
 |-  ( ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) /\ ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) /\ ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) ) -> x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) )
64 eqid 
 |-  ( i e. X |-> <. ( c ` i ) , ( d ` i ) >. ) = ( i e. X |-> <. ( c ` i ) , ( d ` i ) >. )
65 52 54 57 60 61 62 63 4 64 opnvonmbllem1 
 |-  ( ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) /\ ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) /\ ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) ) -> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) )
66 65 3exp 
 |-  ( ( ph /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) -> ( ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) -> ( ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) -> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) ) ) )
67 66 adantlr 
 |-  ( ( ( ph /\ x e. G ) /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) -> ( ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) -> ( ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) -> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) ) ) )
68 67 3adant2 
 |-  ( ( ( ph /\ x e. G ) /\ e e. RR+ /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) -> ( ( c e. ( QQ ^m X ) /\ d e. ( QQ ^m X ) ) -> ( ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) -> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) ) ) )
69 68 rexlimdvv 
 |-  ( ( ( ph /\ x e. G ) /\ e e. RR+ /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) -> ( E. c e. ( QQ ^m X ) E. d e. ( QQ ^m X ) ( x e. X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) /\ X_ i e. X ( ( c ` i ) [,) ( d ` i ) ) C_ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) ) -> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) ) )
70 43 69 mpd 
 |-  ( ( ( ph /\ x e. G ) /\ e e. RR+ /\ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G ) -> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) )
71 70 3exp 
 |-  ( ( ph /\ x e. G ) -> ( e e. RR+ -> ( ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G -> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) ) ) )
72 71 rexlimdv 
 |-  ( ( ph /\ x e. G ) -> ( E. e e. RR+ ( x ( ball ` ( dist ` ( RR^ ` X ) ) ) e ) C_ G -> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) ) )
73 31 72 mpd 
 |-  ( ( ph /\ x e. G ) -> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) )
74 eliun 
 |-  ( x e. U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) <-> E. h e. K x e. X_ i e. X ( ( [,) o. h ) ` i ) )
75 73 74 sylibr 
 |-  ( ( ph /\ x e. G ) -> x e. U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) )
76 75 ralrimiva 
 |-  ( ph -> A. x e. G x e. U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) )
77 dfss3 
 |-  ( G C_ U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) <-> A. x e. G x e. U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) )
78 76 77 sylibr 
 |-  ( ph -> G C_ U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) )
79 4 eleq2i 
 |-  ( h e. K <-> h e. { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G } )
80 79 biimpi 
 |-  ( h e. K -> h e. { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G } )
81 80 adantl 
 |-  ( ( ph /\ h e. K ) -> h e. { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G } )
82 rabid 
 |-  ( h e. { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G } <-> ( h e. ( ( QQ X. QQ ) ^m X ) /\ X_ i e. X ( ( [,) o. h ) ` i ) C_ G ) )
83 81 82 sylib 
 |-  ( ( ph /\ h e. K ) -> ( h e. ( ( QQ X. QQ ) ^m X ) /\ X_ i e. X ( ( [,) o. h ) ` i ) C_ G ) )
84 83 simprd 
 |-  ( ( ph /\ h e. K ) -> X_ i e. X ( ( [,) o. h ) ` i ) C_ G )
85 84 ralrimiva 
 |-  ( ph -> A. h e. K X_ i e. X ( ( [,) o. h ) ` i ) C_ G )
86 iunss 
 |-  ( U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) C_ G <-> A. h e. K X_ i e. X ( ( [,) o. h ) ` i ) C_ G )
87 85 86 sylibr 
 |-  ( ph -> U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) C_ G )
88 78 87 eqssd 
 |-  ( ph -> G = U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) )
89 1 2 dmovnsal 
 |-  ( ph -> S e. SAlg )
90 ssrab2 
 |-  { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G } C_ ( ( QQ X. QQ ) ^m X )
91 4 90 eqsstri 
 |-  K C_ ( ( QQ X. QQ ) ^m X )
92 91 a1i 
 |-  ( ph -> K C_ ( ( QQ X. QQ ) ^m X ) )
93 qct 
 |-  QQ ~<_ _om
94 93 a1i 
 |-  ( ph -> QQ ~<_ _om )
95 xpct 
 |-  ( ( QQ ~<_ _om /\ QQ ~<_ _om ) -> ( QQ X. QQ ) ~<_ _om )
96 94 94 95 syl2anc 
 |-  ( ph -> ( QQ X. QQ ) ~<_ _om )
97 96 1 mpct 
 |-  ( ph -> ( ( QQ X. QQ ) ^m X ) ~<_ _om )
98 ssct 
 |-  ( ( K C_ ( ( QQ X. QQ ) ^m X ) /\ ( ( QQ X. QQ ) ^m X ) ~<_ _om ) -> K ~<_ _om )
99 92 97 98 syl2anc 
 |-  ( ph -> K ~<_ _om )
100 reex 
 |-  RR e. _V
101 100 100 xpex 
 |-  ( RR X. RR ) e. _V
102 qssre 
 |-  QQ C_ RR
103 xpss12 
 |-  ( ( QQ C_ RR /\ QQ C_ RR ) -> ( QQ X. QQ ) C_ ( RR X. RR ) )
104 102 102 103 mp2an 
 |-  ( QQ X. QQ ) C_ ( RR X. RR )
105 mapss 
 |-  ( ( ( RR X. RR ) e. _V /\ ( QQ X. QQ ) C_ ( RR X. RR ) ) -> ( ( QQ X. QQ ) ^m X ) C_ ( ( RR X. RR ) ^m X ) )
106 101 104 105 mp2an 
 |-  ( ( QQ X. QQ ) ^m X ) C_ ( ( RR X. RR ) ^m X )
107 91 sseli 
 |-  ( h e. K -> h e. ( ( QQ X. QQ ) ^m X ) )
108 106 107 sselid 
 |-  ( h e. K -> h e. ( ( RR X. RR ) ^m X ) )
109 elmapi 
 |-  ( h e. ( ( RR X. RR ) ^m X ) -> h : X --> ( RR X. RR ) )
110 108 109 syl 
 |-  ( h e. K -> h : X --> ( RR X. RR ) )
111 110 adantl 
 |-  ( ( ph /\ h e. K ) -> h : X --> ( RR X. RR ) )
112 2fveq3 
 |-  ( k = i -> ( 1st ` ( h ` k ) ) = ( 1st ` ( h ` i ) ) )
113 112 cbvmptv 
 |-  ( k e. X |-> ( 1st ` ( h ` k ) ) ) = ( i e. X |-> ( 1st ` ( h ` i ) ) )
114 2fveq3 
 |-  ( k = i -> ( 2nd ` ( h ` k ) ) = ( 2nd ` ( h ` i ) ) )
115 114 cbvmptv 
 |-  ( k e. X |-> ( 2nd ` ( h ` k ) ) ) = ( i e. X |-> ( 2nd ` ( h ` i ) ) )
116 111 113 115 hoicoto2 
 |-  ( ( ph /\ h e. K ) -> X_ i e. X ( ( [,) o. h ) ` i ) = X_ i e. X ( ( ( k e. X |-> ( 1st ` ( h ` k ) ) ) ` i ) [,) ( ( k e. X |-> ( 2nd ` ( h ` k ) ) ) ` i ) ) )
117 1 adantr 
 |-  ( ( ph /\ h e. K ) -> X e. Fin )
118 111 ffvelcdmda 
 |-  ( ( ( ph /\ h e. K ) /\ k e. X ) -> ( h ` k ) e. ( RR X. RR ) )
119 xp1st 
 |-  ( ( h ` k ) e. ( RR X. RR ) -> ( 1st ` ( h ` k ) ) e. RR )
120 118 119 syl 
 |-  ( ( ( ph /\ h e. K ) /\ k e. X ) -> ( 1st ` ( h ` k ) ) e. RR )
121 120 fmpttd 
 |-  ( ( ph /\ h e. K ) -> ( k e. X |-> ( 1st ` ( h ` k ) ) ) : X --> RR )
122 xp2nd 
 |-  ( ( h ` k ) e. ( RR X. RR ) -> ( 2nd ` ( h ` k ) ) e. RR )
123 118 122 syl 
 |-  ( ( ( ph /\ h e. K ) /\ k e. X ) -> ( 2nd ` ( h ` k ) ) e. RR )
124 123 fmpttd 
 |-  ( ( ph /\ h e. K ) -> ( k e. X |-> ( 2nd ` ( h ` k ) ) ) : X --> RR )
125 117 2 121 124 hoimbl 
 |-  ( ( ph /\ h e. K ) -> X_ i e. X ( ( ( k e. X |-> ( 1st ` ( h ` k ) ) ) ` i ) [,) ( ( k e. X |-> ( 2nd ` ( h ` k ) ) ) ` i ) ) e. S )
126 116 125 eqeltrd 
 |-  ( ( ph /\ h e. K ) -> X_ i e. X ( ( [,) o. h ) ` i ) e. S )
127 89 99 126 saliuncl 
 |-  ( ph -> U_ h e. K X_ i e. X ( ( [,) o. h ) ` i ) e. S )
128 88 127 eqeltrd 
 |-  ( ph -> G e. S )