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	sselid	⊢ ( 𝑞 ∈ 𝐾 → 𝑞 ∈ ( ℝ ↑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	ffvelcdmd	⊢ ( 𝑞 ∈ 𝐾 → ( 𝑞 ‘ 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	ffvelcdmd	⊢ ( 𝑞 ∈ 𝐾 → ( 𝑞 ‘ 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	ffvelcdmd	⊢ ( 𝑞 ∈ 𝐾 → ( 𝑞 ‘ 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	ffvelcdmd	⊢ ( 𝑞 ∈ 𝐾 → ( 𝑞 ‘ 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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐾 ) → ( 𝐸 ‘ 𝑞 ) ∈ ( 𝑆 ↾t ( 𝐴 ∩ 𝐶 ) ) )
178	34 175 177	saliuncl	⊢ ( 𝜑 → ∪ 𝑞 ∈ 𝐾 ( 𝐸 ‘ 𝑞 ) ∈ ( 𝑆 ↾t ( 𝐴 ∩ 𝐶 ) ) )
179	163 178	eqeltrd	⊢ ( 𝜑 → { 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∣ ( 𝐵 · 𝐷 ) < 𝑅 } ∈ ( 𝑆 ↾t ( 𝐴 ∩ 𝐶 ) ) )