Metamath Proof Explorer


Theorem smfmullem4

Description: The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfmullem4.x
|- F/ x ph
smfmullem4.s
|- ( ph -> S e. SAlg )
smfmullem4.a
|- ( ph -> A e. V )
smfmullem4.b
|- ( ( ph /\ x e. A ) -> B e. RR )
smfmullem4.d
|- ( ( ph /\ x e. C ) -> D e. RR )
smfmullem4.m
|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smfmullem4.n
|- ( ph -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
smfmullem4.r
|- ( ph -> R e. RR )
smfmullem4.k
|- K = { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R }
smfmullem4.e
|- E = ( q e. K |-> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
Assertion smfmullem4
|- ( ph -> { x e. ( A i^i C ) | ( B x. D ) < R } e. ( S |`t ( A i^i C ) ) )

Proof

Step Hyp Ref Expression
1 smfmullem4.x
 |-  F/ x ph
2 smfmullem4.s
 |-  ( ph -> S e. SAlg )
3 smfmullem4.a
 |-  ( ph -> A e. V )
4 smfmullem4.b
 |-  ( ( ph /\ x e. A ) -> B e. RR )
5 smfmullem4.d
 |-  ( ( ph /\ x e. C ) -> D e. RR )
6 smfmullem4.m
 |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
7 smfmullem4.n
 |-  ( ph -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
8 smfmullem4.r
 |-  ( ph -> R e. RR )
9 smfmullem4.k
 |-  K = { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R }
10 smfmullem4.e
 |-  E = ( q e. K |-> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
11 8 3ad2ant1
 |-  ( ( ph /\ x e. ( A i^i C ) /\ ( B x. D ) < R ) -> R e. RR )
12 inss1
 |-  ( A i^i C ) C_ A
13 12 a1i
 |-  ( ph -> ( A i^i C ) C_ A )
14 13 sselda
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> x e. A )
15 14 4 syldan
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> B e. RR )
16 15 3adant3
 |-  ( ( ph /\ x e. ( A i^i C ) /\ ( B x. D ) < R ) -> B e. RR )
17 elinel2
 |-  ( x e. ( A i^i C ) -> x e. C )
18 17 adantl
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> x e. C )
19 18 5 syldan
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> D e. RR )
20 19 3adant3
 |-  ( ( ph /\ x e. ( A i^i C ) /\ ( B x. D ) < R ) -> D e. RR )
21 simp3
 |-  ( ( ph /\ x e. ( A i^i C ) /\ ( B x. D ) < R ) -> ( B x. D ) < R )
22 eqid
 |-  ( ( R - ( B x. D ) ) / ( 1 + ( ( abs ` B ) + ( abs ` D ) ) ) ) = ( ( R - ( B x. D ) ) / ( 1 + ( ( abs ` B ) + ( abs ` D ) ) ) )
23 eqid
 |-  if ( 1 <_ ( ( R - ( B x. D ) ) / ( 1 + ( ( abs ` B ) + ( abs ` D ) ) ) ) , 1 , ( ( R - ( B x. D ) ) / ( 1 + ( ( abs ` B ) + ( abs ` D ) ) ) ) ) = if ( 1 <_ ( ( R - ( B x. D ) ) / ( 1 + ( ( abs ` B ) + ( abs ` D ) ) ) ) , 1 , ( ( R - ( B x. D ) ) / ( 1 + ( ( abs ` B ) + ( abs ` D ) ) ) ) )
24 11 9 16 20 21 22 23 smfmullem3
 |-  ( ( ph /\ x e. ( A i^i C ) /\ ( B x. D ) < R ) -> E. q e. K ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )
25 rabid
 |-  ( x e. { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } <-> ( x e. ( A i^i C ) /\ ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) )
26 25 bicomi
 |-  ( ( x e. ( A i^i C ) /\ ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) <-> x e. { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
27 26 biimpi
 |-  ( ( x e. ( A i^i C ) /\ ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) -> x e. { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
28 27 adantll
 |-  ( ( ( ph /\ x e. ( A i^i C ) ) /\ ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) -> x e. { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
29 28 adantlr
 |-  ( ( ( ( ph /\ x e. ( A i^i C ) ) /\ q e. K ) /\ ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) -> x e. { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
30 10 a1i
 |-  ( ph -> E = ( q e. K |-> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } ) )
31 inrab
 |-  ( { x e. ( A i^i C ) | B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) } i^i { x e. ( A i^i C ) | D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) } ) = { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) }
32 3 13 ssexd
 |-  ( ph -> ( A i^i C ) e. _V )
33 eqid
 |-  ( S |`t ( A i^i C ) ) = ( S |`t ( A i^i C ) )
34 2 32 33 subsalsal
 |-  ( ph -> ( S |`t ( A i^i C ) ) e. SAlg )
35 34 adantr
 |-  ( ( ph /\ q e. K ) -> ( S |`t ( A i^i C ) ) e. SAlg )
36 nfv
 |-  F/ x q e. K
37 1 36 nfan
 |-  F/ x ( ph /\ q e. K )
38 2 adantr
 |-  ( ( ph /\ q e. K ) -> S e. SAlg )
39 32 adantr
 |-  ( ( ph /\ q e. K ) -> ( A i^i C ) e. _V )
40 15 adantlr
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( A i^i C ) ) -> B e. RR )
41 2 6 13 sssmfmpt
 |-  ( ph -> ( x e. ( A i^i C ) |-> B ) e. ( SMblFn ` S ) )
42 41 adantr
 |-  ( ( ph /\ q e. K ) -> ( x e. ( A i^i C ) |-> B ) e. ( SMblFn ` S ) )
43 ssrab2
 |-  { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R } C_ ( QQ ^m ( 0 ... 3 ) )
44 9 43 eqsstri
 |-  K C_ ( QQ ^m ( 0 ... 3 ) )
45 reex
 |-  RR e. _V
46 qssre
 |-  QQ C_ RR
47 mapss
 |-  ( ( RR e. _V /\ QQ C_ RR ) -> ( QQ ^m ( 0 ... 3 ) ) C_ ( RR ^m ( 0 ... 3 ) ) )
48 45 46 47 mp2an
 |-  ( QQ ^m ( 0 ... 3 ) ) C_ ( RR ^m ( 0 ... 3 ) )
49 44 48 sstri
 |-  K C_ ( RR ^m ( 0 ... 3 ) )
50 id
 |-  ( q e. K -> q e. K )
51 49 50 sselid
 |-  ( q e. K -> q e. ( RR ^m ( 0 ... 3 ) ) )
52 45 a1i
 |-  ( q e. K -> RR e. _V )
53 ovexd
 |-  ( q e. K -> ( 0 ... 3 ) e. _V )
54 52 53 elmapd
 |-  ( q e. K -> ( q e. ( RR ^m ( 0 ... 3 ) ) <-> q : ( 0 ... 3 ) --> RR ) )
55 51 54 mpbid
 |-  ( q e. K -> q : ( 0 ... 3 ) --> RR )
56 0z
 |-  0 e. ZZ
57 3z
 |-  3 e. ZZ
58 0re
 |-  0 e. RR
59 3re
 |-  3 e. RR
60 3pos
 |-  0 < 3
61 58 59 60 ltleii
 |-  0 <_ 3
62 56 57 61 3pm3.2i
 |-  ( 0 e. ZZ /\ 3 e. ZZ /\ 0 <_ 3 )
63 eluz2
 |-  ( 3 e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ 3 e. ZZ /\ 0 <_ 3 ) )
64 62 63 mpbir
 |-  3 e. ( ZZ>= ` 0 )
65 eluzfz1
 |-  ( 3 e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... 3 ) )
66 64 65 ax-mp
 |-  0 e. ( 0 ... 3 )
67 66 a1i
 |-  ( q e. K -> 0 e. ( 0 ... 3 ) )
68 55 67 ffvelrnd
 |-  ( q e. K -> ( q ` 0 ) e. RR )
69 68 adantl
 |-  ( ( ph /\ q e. K ) -> ( q ` 0 ) e. RR )
70 69 rexrd
 |-  ( ( ph /\ q e. K ) -> ( q ` 0 ) e. RR* )
71 0le1
 |-  0 <_ 1
72 1re
 |-  1 e. RR
73 1lt3
 |-  1 < 3
74 72 59 73 ltleii
 |-  1 <_ 3
75 71 74 pm3.2i
 |-  ( 0 <_ 1 /\ 1 <_ 3 )
76 1z
 |-  1 e. ZZ
77 elfz
 |-  ( ( 1 e. ZZ /\ 0 e. ZZ /\ 3 e. ZZ ) -> ( 1 e. ( 0 ... 3 ) <-> ( 0 <_ 1 /\ 1 <_ 3 ) ) )
78 76 56 57 77 mp3an
 |-  ( 1 e. ( 0 ... 3 ) <-> ( 0 <_ 1 /\ 1 <_ 3 ) )
79 75 78 mpbir
 |-  1 e. ( 0 ... 3 )
80 79 a1i
 |-  ( q e. K -> 1 e. ( 0 ... 3 ) )
81 55 80 ffvelrnd
 |-  ( q e. K -> ( q ` 1 ) e. RR )
82 81 adantl
 |-  ( ( ph /\ q e. K ) -> ( q ` 1 ) e. RR )
83 82 rexrd
 |-  ( ( ph /\ q e. K ) -> ( q ` 1 ) e. RR* )
84 37 38 39 40 42 70 83 smfpimioompt
 |-  ( ( ph /\ q e. K ) -> { x e. ( A i^i C ) | B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) } e. ( S |`t ( A i^i C ) ) )
85 19 adantlr
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( A i^i C ) ) -> D e. RR )
86 1 18 ssdf
 |-  ( ph -> ( A i^i C ) C_ C )
87 2 7 86 sssmfmpt
 |-  ( ph -> ( x e. ( A i^i C ) |-> D ) e. ( SMblFn ` S ) )
88 87 adantr
 |-  ( ( ph /\ q e. K ) -> ( x e. ( A i^i C ) |-> D ) e. ( SMblFn ` S ) )
89 0le2
 |-  0 <_ 2
90 2re
 |-  2 e. RR
91 2lt3
 |-  2 < 3
92 90 59 91 ltleii
 |-  2 <_ 3
93 89 92 pm3.2i
 |-  ( 0 <_ 2 /\ 2 <_ 3 )
94 2z
 |-  2 e. ZZ
95 elfz
 |-  ( ( 2 e. ZZ /\ 0 e. ZZ /\ 3 e. ZZ ) -> ( 2 e. ( 0 ... 3 ) <-> ( 0 <_ 2 /\ 2 <_ 3 ) ) )
96 94 56 57 95 mp3an
 |-  ( 2 e. ( 0 ... 3 ) <-> ( 0 <_ 2 /\ 2 <_ 3 ) )
97 93 96 mpbir
 |-  2 e. ( 0 ... 3 )
98 97 a1i
 |-  ( q e. K -> 2 e. ( 0 ... 3 ) )
99 55 98 ffvelrnd
 |-  ( q e. K -> ( q ` 2 ) e. RR )
100 99 adantl
 |-  ( ( ph /\ q e. K ) -> ( q ` 2 ) e. RR )
101 100 rexrd
 |-  ( ( ph /\ q e. K ) -> ( q ` 2 ) e. RR* )
102 eluzfz2
 |-  ( 3 e. ( ZZ>= ` 0 ) -> 3 e. ( 0 ... 3 ) )
103 64 102 ax-mp
 |-  3 e. ( 0 ... 3 )
104 103 a1i
 |-  ( q e. K -> 3 e. ( 0 ... 3 ) )
105 55 104 ffvelrnd
 |-  ( q e. K -> ( q ` 3 ) e. RR )
106 105 adantl
 |-  ( ( ph /\ q e. K ) -> ( q ` 3 ) e. RR )
107 106 rexrd
 |-  ( ( ph /\ q e. K ) -> ( q ` 3 ) e. RR* )
108 37 38 39 85 88 101 107 smfpimioompt
 |-  ( ( ph /\ q e. K ) -> { x e. ( A i^i C ) | D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) } e. ( S |`t ( A i^i C ) ) )
109 35 84 108 salincld
 |-  ( ( ph /\ q e. K ) -> ( { x e. ( A i^i C ) | B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) } i^i { x e. ( A i^i C ) | D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) } ) e. ( S |`t ( A i^i C ) ) )
110 31 109 eqeltrrid
 |-  ( ( ph /\ q e. K ) -> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } e. ( S |`t ( A i^i C ) ) )
111 110 elexd
 |-  ( ( ph /\ q e. K ) -> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } e. _V )
112 30 111 fvmpt2d
 |-  ( ( ph /\ q e. K ) -> ( E ` q ) = { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
113 112 eqcomd
 |-  ( ( ph /\ q e. K ) -> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } = ( E ` q ) )
114 113 adantlr
 |-  ( ( ( ph /\ x e. ( A i^i C ) ) /\ q e. K ) -> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } = ( E ` q ) )
115 114 adantr
 |-  ( ( ( ( ph /\ x e. ( A i^i C ) ) /\ q e. K ) /\ ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) -> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } = ( E ` q ) )
116 29 115 eleqtrd
 |-  ( ( ( ( ph /\ x e. ( A i^i C ) ) /\ q e. K ) /\ ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) -> x e. ( E ` q ) )
117 116 ex
 |-  ( ( ( ph /\ x e. ( A i^i C ) ) /\ q e. K ) -> ( ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) -> x e. ( E ` q ) ) )
118 117 3adantl3
 |-  ( ( ( ph /\ x e. ( A i^i C ) /\ ( B x. D ) < R ) /\ q e. K ) -> ( ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) -> x e. ( E ` q ) ) )
119 118 reximdva
 |-  ( ( ph /\ x e. ( A i^i C ) /\ ( B x. D ) < R ) -> ( E. q e. K ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) -> E. q e. K x e. ( E ` q ) ) )
120 24 119 mpd
 |-  ( ( ph /\ x e. ( A i^i C ) /\ ( B x. D ) < R ) -> E. q e. K x e. ( E ` q ) )
121 eliun
 |-  ( x e. U_ q e. K ( E ` q ) <-> E. q e. K x e. ( E ` q ) )
122 120 121 sylibr
 |-  ( ( ph /\ x e. ( A i^i C ) /\ ( B x. D ) < R ) -> x e. U_ q e. K ( E ` q ) )
123 122 3exp
 |-  ( ph -> ( x e. ( A i^i C ) -> ( ( B x. D ) < R -> x e. U_ q e. K ( E ` q ) ) ) )
124 1 123 ralrimi
 |-  ( ph -> A. x e. ( A i^i C ) ( ( B x. D ) < R -> x e. U_ q e. K ( E ` q ) ) )
125 36 nfci
 |-  F/_ x K
126 nfrab1
 |-  F/_ x { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) }
127 125 126 nfmpt
 |-  F/_ x ( q e. K |-> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
128 10 127 nfcxfr
 |-  F/_ x E
129 nfcv
 |-  F/_ x q
130 128 129 nffv
 |-  F/_ x ( E ` q )
131 125 130 nfiun
 |-  F/_ x U_ q e. K ( E ` q )
132 131 rabssf
 |-  ( { x e. ( A i^i C ) | ( B x. D ) < R } C_ U_ q e. K ( E ` q ) <-> A. x e. ( A i^i C ) ( ( B x. D ) < R -> x e. U_ q e. K ( E ` q ) ) )
133 124 132 sylibr
 |-  ( ph -> { x e. ( A i^i C ) | ( B x. D ) < R } C_ U_ q e. K ( E ` q ) )
134 ssrab2
 |-  { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } C_ ( A i^i C )
135 112 134 eqsstrdi
 |-  ( ( ph /\ q e. K ) -> ( E ` q ) C_ ( A i^i C ) )
136 simpr
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( E ` q ) ) -> x e. ( E ` q ) )
137 112 adantr
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( E ` q ) ) -> ( E ` q ) = { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
138 136 137 eleqtrd
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( E ` q ) ) -> x e. { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
139 rabidim2
 |-  ( x e. { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } -> ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )
140 138 139 syl
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( E ` q ) ) -> ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )
141 140 simprd
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( E ` q ) ) -> D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) )
142 140 simpld
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( E ` q ) ) -> B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) )
143 50 9 eleqtrdi
 |-  ( q e. K -> q e. { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R } )
144 rabidim2
 |-  ( q e. { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R } -> A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R )
145 143 144 syl
 |-  ( q e. K -> A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R )
146 145 ad2antlr
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( E ` q ) ) -> A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R )
147 oveq1
 |-  ( u = B -> ( u x. v ) = ( B x. v ) )
148 147 breq1d
 |-  ( u = B -> ( ( u x. v ) < R <-> ( B x. v ) < R ) )
149 148 ralbidv
 |-  ( u = B -> ( A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R <-> A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( B x. v ) < R ) )
150 149 rspcva
 |-  ( ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R ) -> A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( B x. v ) < R )
151 142 146 150 syl2anc
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( E ` q ) ) -> A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( B x. v ) < R )
152 oveq2
 |-  ( v = D -> ( B x. v ) = ( B x. D ) )
153 152 breq1d
 |-  ( v = D -> ( ( B x. v ) < R <-> ( B x. D ) < R ) )
154 153 rspcva
 |-  ( ( D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) /\ A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( B x. v ) < R ) -> ( B x. D ) < R )
155 141 151 154 syl2anc
 |-  ( ( ( ph /\ q e. K ) /\ x e. ( E ` q ) ) -> ( B x. D ) < R )
156 155 ex
 |-  ( ( ph /\ q e. K ) -> ( x e. ( E ` q ) -> ( B x. D ) < R ) )
157 37 156 ralrimi
 |-  ( ( ph /\ q e. K ) -> A. x e. ( E ` q ) ( B x. D ) < R )
158 135 157 jca
 |-  ( ( ph /\ q e. K ) -> ( ( E ` q ) C_ ( A i^i C ) /\ A. x e. ( E ` q ) ( B x. D ) < R ) )
159 nfcv
 |-  F/_ x ( A i^i C )
160 130 159 ssrabf
 |-  ( ( E ` q ) C_ { x e. ( A i^i C ) | ( B x. D ) < R } <-> ( ( E ` q ) C_ ( A i^i C ) /\ A. x e. ( E ` q ) ( B x. D ) < R ) )
161 158 160 sylibr
 |-  ( ( ph /\ q e. K ) -> ( E ` q ) C_ { x e. ( A i^i C ) | ( B x. D ) < R } )
162 161 iunssd
 |-  ( ph -> U_ q e. K ( E ` q ) C_ { x e. ( A i^i C ) | ( B x. D ) < R } )
163 133 162 eqssd
 |-  ( ph -> { x e. ( A i^i C ) | ( B x. D ) < R } = U_ q e. K ( E ` q ) )
164 ovex
 |-  ( QQ ^m ( 0 ... 3 ) ) e. _V
165 ssdomg
 |-  ( ( QQ ^m ( 0 ... 3 ) ) e. _V -> ( K C_ ( QQ ^m ( 0 ... 3 ) ) -> K ~<_ ( QQ ^m ( 0 ... 3 ) ) ) )
166 164 165 ax-mp
 |-  ( K C_ ( QQ ^m ( 0 ... 3 ) ) -> K ~<_ ( QQ ^m ( 0 ... 3 ) ) )
167 44 166 ax-mp
 |-  K ~<_ ( QQ ^m ( 0 ... 3 ) )
168 qct
 |-  QQ ~<_ _om
169 168 a1i
 |-  ( T. -> QQ ~<_ _om )
170 fzfid
 |-  ( T. -> ( 0 ... 3 ) e. Fin )
171 169 170 mpct
 |-  ( T. -> ( QQ ^m ( 0 ... 3 ) ) ~<_ _om )
172 171 mptru
 |-  ( QQ ^m ( 0 ... 3 ) ) ~<_ _om
173 domtr
 |-  ( ( K ~<_ ( QQ ^m ( 0 ... 3 ) ) /\ ( QQ ^m ( 0 ... 3 ) ) ~<_ _om ) -> K ~<_ _om )
174 167 172 173 mp2an
 |-  K ~<_ _om
175 174 a1i
 |-  ( ph -> K ~<_ _om )
176 110 10 fmptd
 |-  ( ph -> E : K --> ( S |`t ( A i^i C ) ) )
177 176 ffvelrnda
 |-  ( ( ph /\ q e. K ) -> ( E ` q ) e. ( S |`t ( A i^i C ) ) )
178 34 175 177 saliuncl
 |-  ( ph -> U_ q e. K ( E ` q ) e. ( S |`t ( A i^i C ) ) )
179 163 178 eqeltrd
 |-  ( ph -> { x e. ( A i^i C ) | ( B x. D ) < R } e. ( S |`t ( A i^i C ) ) )