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 ⊢ Ⅎ 𝑥 𝜑
smfmullem4.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smfmullem4.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
smfmullem4.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
smfmullem4.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐷 ∈ ℝ )
smfmullem4.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
smfmullem4.n ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
smfmullem4.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
smfmullem4.k ⊢ 𝐾 = { 𝑞 ∈ ( ℚ ↑m ( 0 ... 3 ) ) ∣ ∀ 𝑢 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑅 }
smfmullem4.e ⊢ 𝐸 = ( 𝑞 ∈ 𝐾 ↦ { 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∣ ( 𝐵 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝐷 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) } )
Assertion smfmullem4 ( 𝜑 → { 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∣ ( 𝐵 · 𝐷 ) < 𝑅 } ∈ ( 𝑆 ↾t ( 𝐴 ∩ 𝐶 ) ) )

Proof

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