Proof of Theorem smfmullem4
| Step | Hyp | Ref
| Expression |
| 1 | | smfmullem4.x |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
| 2 | | smfmullem4.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ℝ) |
| 3 | 2 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝑅 ∈ ℝ) |
| 4 | | smfmullem4.k |
. . . . . . . . 9
⊢ 𝐾 = {𝑞 ∈ (ℚ ↑m (0...3))
∣ ∀𝑢 ∈
((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} |
| 5 | | inss1 4237 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ 𝐶) ⊆ 𝐴 |
| 6 | 5 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ 𝐴) |
| 7 | 6 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐴) |
| 8 | | smfmullem4.b |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| 9 | 7, 8 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ ℝ) |
| 10 | 9 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝐵 ∈ ℝ) |
| 11 | | elinel2 4202 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ 𝐶) |
| 12 | 11 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐶) |
| 13 | | smfmullem4.d |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ) |
| 14 | 12, 13 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐷 ∈ ℝ) |
| 15 | 14 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝐷 ∈ ℝ) |
| 16 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → (𝐵 · 𝐷) < 𝑅) |
| 17 | | eqid 2737 |
. . . . . . . . 9
⊢ ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))) = ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))) |
| 18 | | eqid 2737 |
. . . . . . . . 9
⊢ if(1 ≤
((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))), 1, ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷))))) = if(1 ≤ ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))), 1, ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷))))) |
| 19 | 3, 4, 10, 15, 16, 17, 18 | smfmullem3 46808 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → ∃𝑞 ∈ 𝐾 (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) |
| 20 | | rabid 3458 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))))) |
| 21 | 20 | bicomi 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) ↔ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
| 22 | 21 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
| 23 | 22 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
| 24 | 23 | adantlr 715 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
| 25 | | smfmullem4.e |
. . . . . . . . . . . . . . . . 17
⊢ 𝐸 = (𝑞 ∈ 𝐾 ↦ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
| 26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 = (𝑞 ∈ 𝐾 ↦ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})) |
| 27 | | inrab 4316 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))} ∩ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))}) = {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} |
| 28 | | smfmullem4.s |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 29 | | smfmullem4.a |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 30 | 29, 6 | ssexd 5324 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐴 ∩ 𝐶) ∈ V) |
| 31 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ↾t (𝐴 ∩ 𝐶)) = (𝑆 ↾t (𝐴 ∩ 𝐶)) |
| 32 | 28, 30, 31 | subsalsal 46374 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑆 ↾t (𝐴 ∩ 𝐶)) ∈ SAlg) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑆 ↾t (𝐴 ∩ 𝐶)) ∈ SAlg) |
| 34 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥 𝑞 ∈ 𝐾 |
| 35 | 1, 34 | nfan 1899 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝜑 ∧ 𝑞 ∈ 𝐾) |
| 36 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → 𝑆 ∈ SAlg) |
| 37 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐴 ∩ 𝐶) ∈ V) |
| 38 | 9 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ ℝ) |
| 39 | | smfmullem4.m |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
| 40 | 28, 39, 6 | sssmfmpt 46765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
| 41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
| 42 | | ssrab2 4080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ {𝑞 ∈ (ℚ
↑m (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} ⊆ (ℚ ↑m
(0...3)) |
| 43 | 4, 42 | eqsstri 4030 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐾 ⊆ (ℚ
↑m (0...3)) |
| 44 | | reex 11246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ℝ
∈ V |
| 45 | | qssre 13001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ℚ
⊆ ℝ |
| 46 | | mapss 8929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℝ
∈ V ∧ ℚ ⊆ ℝ) → (ℚ ↑m
(0...3)) ⊆ (ℝ ↑m (0...3))) |
| 47 | 44, 45, 46 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℚ
↑m (0...3)) ⊆ (ℝ ↑m
(0...3)) |
| 48 | 43, 47 | sstri 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐾 ⊆ (ℝ
↑m (0...3)) |
| 49 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝐾 → 𝑞 ∈ 𝐾) |
| 50 | 48, 49 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑞 ∈ 𝐾 → 𝑞 ∈ (ℝ ↑m
(0...3))) |
| 51 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝐾 → ℝ ∈ V) |
| 52 | | ovexd 7466 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝐾 → (0...3) ∈ V) |
| 53 | 51, 52 | elmapd 8880 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑞 ∈ 𝐾 → (𝑞 ∈ (ℝ ↑m (0...3))
↔ 𝑞:(0...3)⟶ℝ)) |
| 54 | 50, 53 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 𝑞:(0...3)⟶ℝ) |
| 55 | | 0z 12624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℤ |
| 56 | | 3z 12650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 3 ∈
ℤ |
| 57 | | 0re 11263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
ℝ |
| 58 | | 3re 12346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 3 ∈
ℝ |
| 59 | | 3pos 12371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 <
3 |
| 60 | 57, 58, 59 | ltleii 11384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ≤
3 |
| 61 | 55, 56, 60 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 ∈
ℤ ∧ 3 ∈ ℤ ∧ 0 ≤ 3) |
| 62 | | eluz2 12884 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (3 ∈
(ℤ≥‘0) ↔ (0 ∈ ℤ ∧ 3 ∈
ℤ ∧ 0 ≤ 3)) |
| 63 | 61, 62 | mpbir 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 3 ∈
(ℤ≥‘0) |
| 64 | | eluzfz1 13571 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (3 ∈
(ℤ≥‘0) → 0 ∈ (0...3)) |
| 65 | 63, 64 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
(0...3) |
| 66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 0 ∈ (0...3)) |
| 67 | 54, 66 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ 𝐾 → (𝑞‘0) ∈ ℝ) |
| 68 | 67 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘0) ∈ ℝ) |
| 69 | 68 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘0) ∈
ℝ*) |
| 70 | | 0le1 11786 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ≤
1 |
| 71 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 1 ∈
ℝ |
| 72 | | 1lt3 12439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 1 <
3 |
| 73 | 71, 58, 72 | ltleii 11384 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ≤
3 |
| 74 | 70, 73 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ≤ 1
∧ 1 ≤ 3) |
| 75 | | 1z 12647 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℤ |
| 76 | | elfz 13553 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((1
∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ) → (1 ∈
(0...3) ↔ (0 ≤ 1 ∧ 1 ≤ 3))) |
| 77 | 75, 55, 56, 76 | mp3an 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
(0...3) ↔ (0 ≤ 1 ∧ 1 ≤ 3)) |
| 78 | 74, 77 | mpbir 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
(0...3) |
| 79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 1 ∈ (0...3)) |
| 80 | 54, 79 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ 𝐾 → (𝑞‘1) ∈ ℝ) |
| 81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘1) ∈ ℝ) |
| 82 | 81 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘1) ∈
ℝ*) |
| 83 | 35, 36, 37, 38, 41, 69, 82 | smfpimioompt 46801 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
| 84 | 14 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐷 ∈ ℝ) |
| 85 | | smfmullem4.n |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐷) ∈ (SMblFn‘𝑆)) |
| 86 | 1, 12 | ssdf 45080 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ 𝐶) |
| 87 | 28, 85, 86 | sssmfmpt 46765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐷) ∈ (SMblFn‘𝑆)) |
| 88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐷) ∈ (SMblFn‘𝑆)) |
| 89 | | 0le2 12368 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ≤
2 |
| 90 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℝ |
| 91 | | 2lt3 12438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 <
3 |
| 92 | 90, 58, 91 | ltleii 11384 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ≤
3 |
| 93 | 89, 92 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ≤ 2
∧ 2 ≤ 3) |
| 94 | | 2z 12649 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℤ |
| 95 | | elfz 13553 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2
∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ) → (2 ∈
(0...3) ↔ (0 ≤ 2 ∧ 2 ≤ 3))) |
| 96 | 94, 55, 56, 95 | mp3an 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 ∈
(0...3) ↔ (0 ≤ 2 ∧ 2 ≤ 3)) |
| 97 | 93, 96 | mpbir 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
(0...3) |
| 98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 2 ∈ (0...3)) |
| 99 | 54, 98 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ 𝐾 → (𝑞‘2) ∈ ℝ) |
| 100 | 99 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘2) ∈ ℝ) |
| 101 | 100 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘2) ∈
ℝ*) |
| 102 | | eluzfz2 13572 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (3 ∈
(ℤ≥‘0) → 3 ∈ (0...3)) |
| 103 | 63, 102 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 ∈
(0...3) |
| 104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 3 ∈ (0...3)) |
| 105 | 54, 104 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ 𝐾 → (𝑞‘3) ∈ ℝ) |
| 106 | 105 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘3) ∈ ℝ) |
| 107 | 106 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘3) ∈
ℝ*) |
| 108 | 35, 36, 37, 84, 88, 101, 107 | smfpimioompt 46801 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
| 109 | 33, 83, 108 | salincld 46367 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))} ∩ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))}) ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
| 110 | 27, 109 | eqeltrrid 2846 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
| 111 | 110 | elexd 3504 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ∈ V) |
| 112 | 26, 111 | fvmpt2d 7029 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐸‘𝑞) = {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
| 113 | 112 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} = (𝐸‘𝑞)) |
| 114 | 113 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} = (𝐸‘𝑞)) |
| 115 | 114 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} = (𝐸‘𝑞)) |
| 116 | 24, 115 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ (𝐸‘𝑞)) |
| 117 | 116 | ex 412 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) → ((𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) → 𝑥 ∈ (𝐸‘𝑞))) |
| 118 | 117 | 3adantl3 1169 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) ∧ 𝑞 ∈ 𝐾) → ((𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) → 𝑥 ∈ (𝐸‘𝑞))) |
| 119 | 118 | reximdva 3168 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → (∃𝑞 ∈ 𝐾 (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) → ∃𝑞 ∈ 𝐾 𝑥 ∈ (𝐸‘𝑞))) |
| 120 | 19, 119 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → ∃𝑞 ∈ 𝐾 𝑥 ∈ (𝐸‘𝑞)) |
| 121 | | eliun 4995 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) ↔ ∃𝑞 ∈ 𝐾 𝑥 ∈ (𝐸‘𝑞)) |
| 122 | 120, 121 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝑥 ∈ ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞)) |
| 123 | 122 | 3exp 1120 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐵 · 𝐷) < 𝑅 → 𝑥 ∈ ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞)))) |
| 124 | 1, 123 | ralrimi 3257 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝐴 ∩ 𝐶)((𝐵 · 𝐷) < 𝑅 → 𝑥 ∈ ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞))) |
| 125 | 34 | nfci 2893 |
. . . . . 6
⊢
Ⅎ𝑥𝐾 |
| 126 | | nfrab1 3457 |
. . . . . . . . 9
⊢
Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} |
| 127 | 125, 126 | nfmpt 5249 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑞 ∈ 𝐾 ↦ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
| 128 | 25, 127 | nfcxfr 2903 |
. . . . . . 7
⊢
Ⅎ𝑥𝐸 |
| 129 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑞 |
| 130 | 128, 129 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑥(𝐸‘𝑞) |
| 131 | 125, 130 | nfiun 5023 |
. . . . 5
⊢
Ⅎ𝑥∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) |
| 132 | 131 | rabssf 45124 |
. . . 4
⊢ ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ⊆ ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)((𝐵 · 𝐷) < 𝑅 → 𝑥 ∈ ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞))) |
| 133 | 124, 132 | sylibr 234 |
. . 3
⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ⊆ ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞)) |
| 134 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ⊆ (𝐴 ∩ 𝐶) |
| 135 | 112, 134 | eqsstrdi 4028 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐸‘𝑞) ⊆ (𝐴 ∩ 𝐶)) |
| 136 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → 𝑥 ∈ (𝐸‘𝑞)) |
| 137 | 112 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → (𝐸‘𝑞) = {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
| 138 | 136, 137 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
| 139 | | rabidim2 45107 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} → (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) |
| 140 | 138, 139 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) |
| 141 | 140 | simprd 495 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) |
| 142 | 140 | simpld 494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))) |
| 143 | 49, 4 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ 𝐾 → 𝑞 ∈ {𝑞 ∈ (ℚ ↑m (0...3))
∣ ∀𝑢 ∈
((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅}) |
| 144 | | rabidim2 45107 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ {𝑞 ∈ (ℚ ↑m (0...3))
∣ ∀𝑢 ∈
((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} → ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅) |
| 145 | 143, 144 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ 𝐾 → ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅) |
| 146 | 145 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅) |
| 147 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝐵 → (𝑢 · 𝑣) = (𝐵 · 𝑣)) |
| 148 | 147 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝐵 → ((𝑢 · 𝑣) < 𝑅 ↔ (𝐵 · 𝑣) < 𝑅)) |
| 149 | 148 | ralbidv 3178 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝐵 → (∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅 ↔ ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅)) |
| 150 | 149 | rspcva 3620 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅) → ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅) |
| 151 | 142, 146,
150 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅) |
| 152 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐷 → (𝐵 · 𝑣) = (𝐵 · 𝐷)) |
| 153 | 152 | breq1d 5153 |
. . . . . . . . . 10
⊢ (𝑣 = 𝐷 → ((𝐵 · 𝑣) < 𝑅 ↔ (𝐵 · 𝐷) < 𝑅)) |
| 154 | 153 | rspcva 3620 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)) ∧ ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅) → (𝐵 · 𝐷) < 𝑅) |
| 155 | 141, 151,
154 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → (𝐵 · 𝐷) < 𝑅) |
| 156 | 155 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑥 ∈ (𝐸‘𝑞) → (𝐵 · 𝐷) < 𝑅)) |
| 157 | 35, 156 | ralrimi 3257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → ∀𝑥 ∈ (𝐸‘𝑞)(𝐵 · 𝐷) < 𝑅) |
| 158 | 135, 157 | jca 511 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → ((𝐸‘𝑞) ⊆ (𝐴 ∩ 𝐶) ∧ ∀𝑥 ∈ (𝐸‘𝑞)(𝐵 · 𝐷) < 𝑅)) |
| 159 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥(𝐴 ∩ 𝐶) |
| 160 | 130, 159 | ssrabf 45119 |
. . . . 5
⊢ ((𝐸‘𝑞) ⊆ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ↔ ((𝐸‘𝑞) ⊆ (𝐴 ∩ 𝐶) ∧ ∀𝑥 ∈ (𝐸‘𝑞)(𝐵 · 𝐷) < 𝑅)) |
| 161 | 158, 160 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐸‘𝑞) ⊆ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅}) |
| 162 | 161 | iunssd 5050 |
. . 3
⊢ (𝜑 → ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) ⊆ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅}) |
| 163 | 133, 162 | eqssd 4001 |
. 2
⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} = ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞)) |
| 164 | | ovex 7464 |
. . . . . . 7
⊢ (ℚ
↑m (0...3)) ∈ V |
| 165 | | ssdomg 9040 |
. . . . . . 7
⊢ ((ℚ
↑m (0...3)) ∈ V → (𝐾 ⊆ (ℚ ↑m
(0...3)) → 𝐾 ≼
(ℚ ↑m (0...3)))) |
| 166 | 164, 165 | ax-mp 5 |
. . . . . 6
⊢ (𝐾 ⊆ (ℚ
↑m (0...3)) → 𝐾 ≼ (ℚ ↑m
(0...3))) |
| 167 | 43, 166 | ax-mp 5 |
. . . . 5
⊢ 𝐾 ≼ (ℚ
↑m (0...3)) |
| 168 | | qct 45373 |
. . . . . . . 8
⊢ ℚ
≼ ω |
| 169 | 168 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ℚ ≼ ω) |
| 170 | | fzfid 14014 |
. . . . . . 7
⊢ (⊤
→ (0...3) ∈ Fin) |
| 171 | 169, 170 | mpct 45206 |
. . . . . 6
⊢ (⊤
→ (ℚ ↑m (0...3)) ≼ ω) |
| 172 | 171 | mptru 1547 |
. . . . 5
⊢ (ℚ
↑m (0...3)) ≼ ω |
| 173 | | domtr 9047 |
. . . . 5
⊢ ((𝐾 ≼ (ℚ
↑m (0...3)) ∧ (ℚ ↑m (0...3)) ≼
ω) → 𝐾 ≼
ω) |
| 174 | 167, 172,
173 | mp2an 692 |
. . . 4
⊢ 𝐾 ≼
ω |
| 175 | 174 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐾 ≼ ω) |
| 176 | 110, 25 | fmptd 7134 |
. . . 4
⊢ (𝜑 → 𝐸:𝐾⟶(𝑆 ↾t (𝐴 ∩ 𝐶))) |
| 177 | 176 | ffvelcdmda 7104 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐸‘𝑞) ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
| 178 | 32, 175, 177 | saliuncl 46338 |
. 2
⊢ (𝜑 → ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
| 179 | 163, 178 | eqeltrd 2841 |
1
⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |