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 ffvelrnda
 |-  ( ( ( 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 )