Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smfmullem4 Structured version   Visualization version   GIF version

Theorem smfmullem4 45589
Description: The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
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
Ref Expression
smfmullem4 (πœ‘ β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 Β· 𝐷) < 𝑅} ∈ (𝑆 β†Ύt (𝐴 ∩ 𝐢)))
Distinct variable groups:   𝐴,π‘ž,𝑒,𝑣,π‘₯   𝐡,π‘ž,𝑒,𝑣   𝐢,π‘ž,𝑒,𝑣,π‘₯   𝐷,π‘ž,𝑒,𝑣   𝐾,π‘ž,π‘₯   𝑅,π‘ž,𝑒,𝑣   𝑆,π‘ž   πœ‘,π‘ž,𝑒,𝑣
Allowed substitution hints:   πœ‘(π‘₯)   𝐡(π‘₯)   𝐷(π‘₯)   𝑅(π‘₯)   𝑆(π‘₯,𝑣,𝑒)   𝐸(π‘₯,𝑣,𝑒,π‘ž)   𝐾(𝑣,𝑒)   𝑉(π‘₯,𝑣,𝑒,π‘ž)

Proof of Theorem smfmullem4
StepHypRef Expression
1 smfmullem4.x . . . . 5 β„²π‘₯πœ‘
2 smfmullem4.r . . . . . . . . . 10 (πœ‘ β†’ 𝑅 ∈ ℝ)
323ad2ant1 1133 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 Β· 𝐷) < 𝑅) β†’ 𝑅 ∈ ℝ)
4 smfmullem4.k . . . . . . . . 9 𝐾 = {π‘ž ∈ (β„š ↑m (0...3)) ∣ βˆ€π‘’ ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝑒 Β· 𝑣) < 𝑅}
5 inss1 4228 . . . . . . . . . . . . 13 (𝐴 ∩ 𝐢) βŠ† 𝐴
65a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 ∩ 𝐢) βŠ† 𝐴)
76sselda 3982 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) β†’ π‘₯ ∈ 𝐴)
8 smfmullem4.b . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝐡 ∈ ℝ)
97, 8syldan 591 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) β†’ 𝐡 ∈ ℝ)
1093adant3 1132 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 Β· 𝐷) < 𝑅) β†’ 𝐡 ∈ ℝ)
11 elinel2 4196 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴 ∩ 𝐢) β†’ π‘₯ ∈ 𝐢)
1211adantl 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) β†’ π‘₯ ∈ 𝐢)
13 smfmullem4.d . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝐷 ∈ ℝ)
1412, 13syldan 591 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) β†’ 𝐷 ∈ ℝ)
15143adant3 1132 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 Β· 𝐷) < 𝑅) β†’ 𝐷 ∈ ℝ)
16 simp3 1138 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 Β· 𝐷) < 𝑅) β†’ (𝐡 Β· 𝐷) < 𝑅)
17 eqid 2732 . . . . . . . . 9 ((𝑅 βˆ’ (𝐡 Β· 𝐷)) / (1 + ((absβ€˜π΅) + (absβ€˜π·)))) = ((𝑅 βˆ’ (𝐡 Β· 𝐷)) / (1 + ((absβ€˜π΅) + (absβ€˜π·))))
18 eqid 2732 . . . . . . . . 9 if(1 ≀ ((𝑅 βˆ’ (𝐡 Β· 𝐷)) / (1 + ((absβ€˜π΅) + (absβ€˜π·)))), 1, ((𝑅 βˆ’ (𝐡 Β· 𝐷)) / (1 + ((absβ€˜π΅) + (absβ€˜π·))))) = if(1 ≀ ((𝑅 βˆ’ (𝐡 Β· 𝐷)) / (1 + ((absβ€˜π΅) + (absβ€˜π·)))), 1, ((𝑅 βˆ’ (𝐡 Β· 𝐷)) / (1 + ((absβ€˜π΅) + (absβ€˜π·)))))
193, 4, 10, 15, 16, 17, 18smfmullem3 45588 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 Β· 𝐷) < 𝑅) β†’ βˆƒπ‘ž ∈ 𝐾 (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))))
20 rabid 3452 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))} ↔ (π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))))
2120bicomi 223 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))) ↔ π‘₯ ∈ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))})
2221biimpi 215 . . . . . . . . . . . . . 14 ((π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))) β†’ π‘₯ ∈ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))})
2322adantll 712 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) ∧ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))) β†’ π‘₯ ∈ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))})
2423adantlr 713 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) ∧ π‘ž ∈ 𝐾) ∧ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))) β†’ π‘₯ ∈ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))})
25 smfmullem4.e . . . . . . . . . . . . . . . . 17 𝐸 = (π‘ž ∈ 𝐾 ↦ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))})
2625a1i 11 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐸 = (π‘ž ∈ 𝐾 ↦ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))}))
27 inrab 4306 . . . . . . . . . . . . . . . . . 18 ({π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ 𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))} ∩ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))}) = {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))}
28 smfmullem4.s . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑆 ∈ SAlg)
29 smfmullem4.a . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝐴 ∈ 𝑉)
3029, 6ssexd 5324 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝐴 ∩ 𝐢) ∈ V)
31 eqid 2732 . . . . . . . . . . . . . . . . . . . . 21 (𝑆 β†Ύt (𝐴 ∩ 𝐢)) = (𝑆 β†Ύt (𝐴 ∩ 𝐢))
3228, 30, 31subsalsal 45154 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝑆 β†Ύt (𝐴 ∩ 𝐢)) ∈ SAlg)
3332adantr 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (𝑆 β†Ύt (𝐴 ∩ 𝐢)) ∈ SAlg)
34 nfv 1917 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘₯ π‘ž ∈ 𝐾
351, 34nfan 1902 . . . . . . . . . . . . . . . . . . . 20 β„²π‘₯(πœ‘ ∧ π‘ž ∈ 𝐾)
3628adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ 𝑆 ∈ SAlg)
3730adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (𝐴 ∩ 𝐢) ∈ V)
389adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) β†’ 𝐡 ∈ ℝ)
39 smfmullem4.m . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ (SMblFnβ€˜π‘†))
4028, 39, 6sssmfmpt 45545 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘₯ ∈ (𝐴 ∩ 𝐢) ↦ 𝐡) ∈ (SMblFnβ€˜π‘†))
4140adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘₯ ∈ (𝐴 ∩ 𝐢) ↦ 𝐡) ∈ (SMblFnβ€˜π‘†))
42 ssrab2 4077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {π‘ž ∈ (β„š ↑m (0...3)) ∣ βˆ€π‘’ ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝑒 Β· 𝑣) < 𝑅} βŠ† (β„š ↑m (0...3))
434, 42eqsstri 4016 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐾 βŠ† (β„š ↑m (0...3))
44 reex 11203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℝ ∈ V
45 qssre 12945 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 β„š βŠ† ℝ
46 mapss 8885 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((ℝ ∈ V ∧ β„š βŠ† ℝ) β†’ (β„š ↑m (0...3)) βŠ† (ℝ ↑m (0...3)))
4744, 45, 46mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (β„š ↑m (0...3)) βŠ† (ℝ ↑m (0...3))
4843, 47sstri 3991 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐾 βŠ† (ℝ ↑m (0...3))
49 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘ž ∈ 𝐾 β†’ π‘ž ∈ 𝐾)
5048, 49sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘ž ∈ 𝐾 β†’ π‘ž ∈ (ℝ ↑m (0...3)))
5144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘ž ∈ 𝐾 β†’ ℝ ∈ V)
52 ovexd 7446 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘ž ∈ 𝐾 β†’ (0...3) ∈ V)
5351, 52elmapd 8836 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘ž ∈ 𝐾 β†’ (π‘ž ∈ (ℝ ↑m (0...3)) ↔ π‘ž:(0...3)βŸΆβ„))
5450, 53mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘ž ∈ 𝐾 β†’ π‘ž:(0...3)βŸΆβ„)
55 0z 12571 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ β„€
56 3z 12597 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 3 ∈ β„€
57 0re 11218 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 ∈ ℝ
58 3re 12294 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 ∈ ℝ
59 3pos 12319 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 < 3
6057, 58, 59ltleii 11339 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≀ 3
6155, 56, 603pm3.2i 1339 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ β„€ ∧ 3 ∈ β„€ ∧ 0 ≀ 3)
62 eluz2 12830 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 ∈ (β„€β‰₯β€˜0) ↔ (0 ∈ β„€ ∧ 3 ∈ β„€ ∧ 0 ≀ 3))
6361, 62mpbir 230 . . . . . . . . . . . . . . . . . . . . . . . . 25 3 ∈ (β„€β‰₯β€˜0)
64 eluzfz1 13510 . . . . . . . . . . . . . . . . . . . . . . . . 25 (3 ∈ (β„€β‰₯β€˜0) β†’ 0 ∈ (0...3))
6563, 64ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ (0...3)
6665a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘ž ∈ 𝐾 β†’ 0 ∈ (0...3))
6754, 66ffvelcdmd 7087 . . . . . . . . . . . . . . . . . . . . . 22 (π‘ž ∈ 𝐾 β†’ (π‘žβ€˜0) ∈ ℝ)
6867adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘žβ€˜0) ∈ ℝ)
6968rexrd 11266 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘žβ€˜0) ∈ ℝ*)
70 0le1 11739 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ≀ 1
71 1re 11216 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 ∈ ℝ
72 1lt3 12387 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 < 3
7371, 58, 72ltleii 11339 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ≀ 3
7470, 73pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ≀ 1 ∧ 1 ≀ 3)
75 1z 12594 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ β„€
76 elfz 13492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 ∈ β„€ ∧ 0 ∈ β„€ ∧ 3 ∈ β„€) β†’ (1 ∈ (0...3) ↔ (0 ≀ 1 ∧ 1 ≀ 3)))
7775, 55, 56, 76mp3an 1461 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ (0...3) ↔ (0 ≀ 1 ∧ 1 ≀ 3))
7874, 77mpbir 230 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ (0...3)
7978a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘ž ∈ 𝐾 β†’ 1 ∈ (0...3))
8054, 79ffvelcdmd 7087 . . . . . . . . . . . . . . . . . . . . . 22 (π‘ž ∈ 𝐾 β†’ (π‘žβ€˜1) ∈ ℝ)
8180adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘žβ€˜1) ∈ ℝ)
8281rexrd 11266 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘žβ€˜1) ∈ ℝ*)
8335, 36, 37, 38, 41, 69, 82smfpimioompt 45581 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ 𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))} ∈ (𝑆 β†Ύt (𝐴 ∩ 𝐢)))
8414adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) β†’ 𝐷 ∈ ℝ)
85 smfmullem4.n . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (π‘₯ ∈ 𝐢 ↦ 𝐷) ∈ (SMblFnβ€˜π‘†))
861, 12ssdf 43846 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝐴 ∩ 𝐢) βŠ† 𝐢)
8728, 85, 86sssmfmpt 45545 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘₯ ∈ (𝐴 ∩ 𝐢) ↦ 𝐷) ∈ (SMblFnβ€˜π‘†))
8887adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘₯ ∈ (𝐴 ∩ 𝐢) ↦ 𝐷) ∈ (SMblFnβ€˜π‘†))
89 0le2 12316 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ≀ 2
90 2re 12288 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℝ
91 2lt3 12386 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 < 3
9290, 58, 91ltleii 11339 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ≀ 3
9389, 92pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ≀ 2 ∧ 2 ≀ 3)
94 2z 12596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ∈ β„€
95 elfz 13492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ β„€ ∧ 0 ∈ β„€ ∧ 3 ∈ β„€) β†’ (2 ∈ (0...3) ↔ (0 ≀ 2 ∧ 2 ≀ 3)))
9694, 55, 56, 95mp3an 1461 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ (0...3) ↔ (0 ≀ 2 ∧ 2 ≀ 3))
9793, 96mpbir 230 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ (0...3)
9897a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘ž ∈ 𝐾 β†’ 2 ∈ (0...3))
9954, 98ffvelcdmd 7087 . . . . . . . . . . . . . . . . . . . . . 22 (π‘ž ∈ 𝐾 β†’ (π‘žβ€˜2) ∈ ℝ)
10099adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘žβ€˜2) ∈ ℝ)
101100rexrd 11266 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘žβ€˜2) ∈ ℝ*)
102 eluzfz2 13511 . . . . . . . . . . . . . . . . . . . . . . . . 25 (3 ∈ (β„€β‰₯β€˜0) β†’ 3 ∈ (0...3))
10363, 102ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 3 ∈ (0...3)
104103a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘ž ∈ 𝐾 β†’ 3 ∈ (0...3))
10554, 104ffvelcdmd 7087 . . . . . . . . . . . . . . . . . . . . . 22 (π‘ž ∈ 𝐾 β†’ (π‘žβ€˜3) ∈ ℝ)
106105adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘žβ€˜3) ∈ ℝ)
107106rexrd 11266 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘žβ€˜3) ∈ ℝ*)
10835, 36, 37, 84, 88, 101, 107smfpimioompt 45581 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))} ∈ (𝑆 β†Ύt (𝐴 ∩ 𝐢)))
10933, 83, 108salincld 45147 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ ({π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ 𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))} ∩ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))}) ∈ (𝑆 β†Ύt (𝐴 ∩ 𝐢)))
11027, 109eqeltrrid 2838 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))} ∈ (𝑆 β†Ύt (𝐴 ∩ 𝐢)))
111110elexd 3494 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))} ∈ V)
11226, 111fvmpt2d 7011 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (πΈβ€˜π‘ž) = {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))})
113112eqcomd 2738 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))} = (πΈβ€˜π‘ž))
114113adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) ∧ π‘ž ∈ 𝐾) β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))} = (πΈβ€˜π‘ž))
115114adantr 481 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) ∧ π‘ž ∈ 𝐾) ∧ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))) β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))} = (πΈβ€˜π‘ž))
11624, 115eleqtrd 2835 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) ∧ π‘ž ∈ 𝐾) ∧ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))) β†’ π‘₯ ∈ (πΈβ€˜π‘ž))
117116ex 413 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢)) ∧ π‘ž ∈ 𝐾) β†’ ((𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))) β†’ π‘₯ ∈ (πΈβ€˜π‘ž)))
1181173adantl3 1168 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 Β· 𝐷) < 𝑅) ∧ π‘ž ∈ 𝐾) β†’ ((𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))) β†’ π‘₯ ∈ (πΈβ€˜π‘ž)))
119118reximdva 3168 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 Β· 𝐷) < 𝑅) β†’ (βˆƒπ‘ž ∈ 𝐾 (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))) β†’ βˆƒπ‘ž ∈ 𝐾 π‘₯ ∈ (πΈβ€˜π‘ž)))
12019, 119mpd 15 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 Β· 𝐷) < 𝑅) β†’ βˆƒπ‘ž ∈ 𝐾 π‘₯ ∈ (πΈβ€˜π‘ž))
121 eliun 5001 . . . . . . 7 (π‘₯ ∈ βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž) ↔ βˆƒπ‘ž ∈ 𝐾 π‘₯ ∈ (πΈβ€˜π‘ž))
122120, 121sylibr 233 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ 𝐢) ∧ (𝐡 Β· 𝐷) < 𝑅) β†’ π‘₯ ∈ βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž))
1231223exp 1119 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (𝐴 ∩ 𝐢) β†’ ((𝐡 Β· 𝐷) < 𝑅 β†’ π‘₯ ∈ βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž))))
1241, 123ralrimi 3254 . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ (𝐴 ∩ 𝐢)((𝐡 Β· 𝐷) < 𝑅 β†’ π‘₯ ∈ βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž)))
12534nfci 2886 . . . . . 6 β„²π‘₯𝐾
126 nfrab1 3451 . . . . . . . . 9 β„²π‘₯{π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))}
127125, 126nfmpt 5255 . . . . . . . 8 β„²π‘₯(π‘ž ∈ 𝐾 ↦ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))})
12825, 127nfcxfr 2901 . . . . . . 7 β„²π‘₯𝐸
129 nfcv 2903 . . . . . . 7 β„²π‘₯π‘ž
130128, 129nffv 6901 . . . . . 6 β„²π‘₯(πΈβ€˜π‘ž)
131125, 130nfiun 5027 . . . . 5 β„²π‘₯βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž)
132131rabssf 43890 . . . 4 ({π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 Β· 𝐷) < 𝑅} βŠ† βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž) ↔ βˆ€π‘₯ ∈ (𝐴 ∩ 𝐢)((𝐡 Β· 𝐷) < 𝑅 β†’ π‘₯ ∈ βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž)))
133124, 132sylibr 233 . . 3 (πœ‘ β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 Β· 𝐷) < 𝑅} βŠ† βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž))
134 ssrab2 4077 . . . . . . 7 {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))} βŠ† (𝐴 ∩ 𝐢)
135112, 134eqsstrdi 4036 . . . . . 6 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (πΈβ€˜π‘ž) βŠ† (𝐴 ∩ 𝐢))
136 simpr 485 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (πΈβ€˜π‘ž)) β†’ π‘₯ ∈ (πΈβ€˜π‘ž))
137112adantr 481 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (πΈβ€˜π‘ž)) β†’ (πΈβ€˜π‘ž) = {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))})
138136, 137eleqtrd 2835 . . . . . . . . . . 11 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (πΈβ€˜π‘ž)) β†’ π‘₯ ∈ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))})
139 rabidim2 43873 . . . . . . . . . . 11 (π‘₯ ∈ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))} β†’ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))))
140138, 139syl 17 . . . . . . . . . 10 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (πΈβ€˜π‘ž)) β†’ (𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))))
141140simprd 496 . . . . . . . . 9 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (πΈβ€˜π‘ž)) β†’ 𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)))
142140simpld 495 . . . . . . . . . 10 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (πΈβ€˜π‘ž)) β†’ 𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)))
14349, 4eleqtrdi 2843 . . . . . . . . . . . 12 (π‘ž ∈ 𝐾 β†’ π‘ž ∈ {π‘ž ∈ (β„š ↑m (0...3)) ∣ βˆ€π‘’ ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝑒 Β· 𝑣) < 𝑅})
144 rabidim2 43873 . . . . . . . . . . . 12 (π‘ž ∈ {π‘ž ∈ (β„š ↑m (0...3)) ∣ βˆ€π‘’ ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝑒 Β· 𝑣) < 𝑅} β†’ βˆ€π‘’ ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝑒 Β· 𝑣) < 𝑅)
145143, 144syl 17 . . . . . . . . . . 11 (π‘ž ∈ 𝐾 β†’ βˆ€π‘’ ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝑒 Β· 𝑣) < 𝑅)
146145ad2antlr 725 . . . . . . . . . 10 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (πΈβ€˜π‘ž)) β†’ βˆ€π‘’ ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝑒 Β· 𝑣) < 𝑅)
147 oveq1 7418 . . . . . . . . . . . . 13 (𝑒 = 𝐡 β†’ (𝑒 Β· 𝑣) = (𝐡 Β· 𝑣))
148147breq1d 5158 . . . . . . . . . . . 12 (𝑒 = 𝐡 β†’ ((𝑒 Β· 𝑣) < 𝑅 ↔ (𝐡 Β· 𝑣) < 𝑅))
149148ralbidv 3177 . . . . . . . . . . 11 (𝑒 = 𝐡 β†’ (βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝑒 Β· 𝑣) < 𝑅 ↔ βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝐡 Β· 𝑣) < 𝑅))
150149rspcva 3610 . . . . . . . . . 10 ((𝐡 ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1)) ∧ βˆ€π‘’ ∈ ((π‘žβ€˜0)(,)(π‘žβ€˜1))βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝑒 Β· 𝑣) < 𝑅) β†’ βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝐡 Β· 𝑣) < 𝑅)
151142, 146, 150syl2anc 584 . . . . . . . . 9 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (πΈβ€˜π‘ž)) β†’ βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝐡 Β· 𝑣) < 𝑅)
152 oveq2 7419 . . . . . . . . . . 11 (𝑣 = 𝐷 β†’ (𝐡 Β· 𝑣) = (𝐡 Β· 𝐷))
153152breq1d 5158 . . . . . . . . . 10 (𝑣 = 𝐷 β†’ ((𝐡 Β· 𝑣) < 𝑅 ↔ (𝐡 Β· 𝐷) < 𝑅))
154153rspcva 3610 . . . . . . . . 9 ((𝐷 ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3)) ∧ βˆ€π‘£ ∈ ((π‘žβ€˜2)(,)(π‘žβ€˜3))(𝐡 Β· 𝑣) < 𝑅) β†’ (𝐡 Β· 𝐷) < 𝑅)
155141, 151, 154syl2anc 584 . . . . . . . 8 (((πœ‘ ∧ π‘ž ∈ 𝐾) ∧ π‘₯ ∈ (πΈβ€˜π‘ž)) β†’ (𝐡 Β· 𝐷) < 𝑅)
156155ex 413 . . . . . . 7 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (π‘₯ ∈ (πΈβ€˜π‘ž) β†’ (𝐡 Β· 𝐷) < 𝑅))
15735, 156ralrimi 3254 . . . . . 6 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ βˆ€π‘₯ ∈ (πΈβ€˜π‘ž)(𝐡 Β· 𝐷) < 𝑅)
158135, 157jca 512 . . . . 5 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ ((πΈβ€˜π‘ž) βŠ† (𝐴 ∩ 𝐢) ∧ βˆ€π‘₯ ∈ (πΈβ€˜π‘ž)(𝐡 Β· 𝐷) < 𝑅))
159 nfcv 2903 . . . . . 6 β„²π‘₯(𝐴 ∩ 𝐢)
160130, 159ssrabf 43885 . . . . 5 ((πΈβ€˜π‘ž) βŠ† {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 Β· 𝐷) < 𝑅} ↔ ((πΈβ€˜π‘ž) βŠ† (𝐴 ∩ 𝐢) ∧ βˆ€π‘₯ ∈ (πΈβ€˜π‘ž)(𝐡 Β· 𝐷) < 𝑅))
161158, 160sylibr 233 . . . 4 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (πΈβ€˜π‘ž) βŠ† {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 Β· 𝐷) < 𝑅})
162161iunssd 5053 . . 3 (πœ‘ β†’ βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž) βŠ† {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 Β· 𝐷) < 𝑅})
163133, 162eqssd 3999 . 2 (πœ‘ β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 Β· 𝐷) < 𝑅} = βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž))
164 ovex 7444 . . . . . . 7 (β„š ↑m (0...3)) ∈ V
165 ssdomg 8998 . . . . . . 7 ((β„š ↑m (0...3)) ∈ V β†’ (𝐾 βŠ† (β„š ↑m (0...3)) β†’ 𝐾 β‰Ό (β„š ↑m (0...3))))
166164, 165ax-mp 5 . . . . . 6 (𝐾 βŠ† (β„š ↑m (0...3)) β†’ 𝐾 β‰Ό (β„š ↑m (0...3)))
16743, 166ax-mp 5 . . . . 5 𝐾 β‰Ό (β„š ↑m (0...3))
168 qct 44151 . . . . . . . 8 β„š β‰Ό Ο‰
169168a1i 11 . . . . . . 7 (⊀ β†’ β„š β‰Ό Ο‰)
170 fzfid 13940 . . . . . . 7 (⊀ β†’ (0...3) ∈ Fin)
171169, 170mpct 43979 . . . . . 6 (⊀ β†’ (β„š ↑m (0...3)) β‰Ό Ο‰)
172171mptru 1548 . . . . 5 (β„š ↑m (0...3)) β‰Ό Ο‰
173 domtr 9005 . . . . 5 ((𝐾 β‰Ό (β„š ↑m (0...3)) ∧ (β„š ↑m (0...3)) β‰Ό Ο‰) β†’ 𝐾 β‰Ό Ο‰)
174167, 172, 173mp2an 690 . . . 4 𝐾 β‰Ό Ο‰
175174a1i 11 . . 3 (πœ‘ β†’ 𝐾 β‰Ό Ο‰)
176110, 25fmptd 7115 . . . 4 (πœ‘ β†’ 𝐸:𝐾⟢(𝑆 β†Ύt (𝐴 ∩ 𝐢)))
177176ffvelcdmda 7086 . . 3 ((πœ‘ ∧ π‘ž ∈ 𝐾) β†’ (πΈβ€˜π‘ž) ∈ (𝑆 β†Ύt (𝐴 ∩ 𝐢)))
17832, 175, 177saliuncl 45118 . 2 (πœ‘ β†’ βˆͺ π‘ž ∈ 𝐾 (πΈβ€˜π‘ž) ∈ (𝑆 β†Ύt (𝐴 ∩ 𝐢)))
179163, 178eqeltrd 2833 1 (πœ‘ β†’ {π‘₯ ∈ (𝐴 ∩ 𝐢) ∣ (𝐡 Β· 𝐷) < 𝑅} ∈ (𝑆 β†Ύt (𝐴 ∩ 𝐢)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βŠ€wtru 1542  β„²wnf 1785   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   ∩ cin 3947   βŠ† wss 3948  ifcif 4528  βˆͺ ciun 4997   class class class wbr 5148   ↦ cmpt 5231  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  Ο‰com 7857   ↑m cmap 8822   β‰Ό cdom 8939  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117   < clt 11250   ≀ cle 11251   βˆ’ cmin 11446   / cdiv 11873  2c2 12269  3c3 12270  β„€cz 12560  β„€β‰₯cuz 12824  β„šcq 12934  (,)cioo 13326  ...cfz 13486  abscabs 15183   β†Ύt crest 17368  SAlgcsalg 45103  SMblFncsmblfn 45490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cc 10432  ax-ac2 10460  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-omul 8473  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-acn 9939  df-ac 10113  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-n0 12475  df-z 12561  df-uz 12825  df-q 12935  df-rp 12977  df-ioo 13330  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-fl 13759  df-seq 13969  df-exp 14030  df-hash 14293  df-word 14467  df-concat 14523  df-s1 14548  df-s2 14801  df-s3 14802  df-s4 14803  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-rest 17370  df-salg 45104  df-smblfn 45491
This theorem is referenced by:  smfmul  45590
  Copyright terms: Public domain W3C validator