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