![]() |
Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > salpreimalegt | Structured version Visualization version GIF version |
Description: If all the preimages of right-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of left-open, unbounded above intervals, belong to the sigma-algebra. (ii) implies (iii) in Proposition 121B of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
salpreimalegt.x | ⊢ Ⅎ𝑥𝜑 |
salpreimalegt.a | ⊢ Ⅎ𝑎𝜑 |
salpreimalegt.s | ⊢ (𝜑 → 𝑆 ∈ SAlg) |
salpreimalegt.u | ⊢ 𝐴 = ∪ 𝑆 |
salpreimalegt.b | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) |
salpreimalegt.p | ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎} ∈ 𝑆) |
salpreimalegt.c | ⊢ (𝜑 → 𝐶 ∈ ℝ) |
Ref | Expression |
---|---|
salpreimalegt | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} ∈ 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | salpreimalegt.u | . . . . . 6 ⊢ 𝐴 = ∪ 𝑆 | |
2 | 1 | eqcomi 2807 | . . . . 5 ⊢ ∪ 𝑆 = 𝐴 |
3 | 2 | a1i 11 | . . . 4 ⊢ (𝜑 → ∪ 𝑆 = 𝐴) |
4 | 3 | difeq1d 4049 | . . 3 ⊢ (𝜑 → (∪ 𝑆 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) = (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) |
5 | salpreimalegt.x | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
6 | salpreimalegt.b | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) | |
7 | salpreimalegt.c | . . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ) | |
8 | 7 | rexrd 10680 | . . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ*) |
9 | 5, 6, 8 | preimalegt 43338 | . . 3 ⊢ (𝜑 → (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) |
10 | 4, 9 | eqtr2d 2834 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} = (∪ 𝑆 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) |
11 | salpreimalegt.s | . . 3 ⊢ (𝜑 → 𝑆 ∈ SAlg) | |
12 | 7 | ancli 552 | . . . 4 ⊢ (𝜑 → (𝜑 ∧ 𝐶 ∈ ℝ)) |
13 | salpreimalegt.a | . . . . . . 7 ⊢ Ⅎ𝑎𝜑 | |
14 | nfv 1915 | . . . . . . 7 ⊢ Ⅎ𝑎 𝐶 ∈ ℝ | |
15 | 13, 14 | nfan 1900 | . . . . . 6 ⊢ Ⅎ𝑎(𝜑 ∧ 𝐶 ∈ ℝ) |
16 | nfv 1915 | . . . . . 6 ⊢ Ⅎ𝑎{𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ∈ 𝑆 | |
17 | 15, 16 | nfim 1897 | . . . . 5 ⊢ Ⅎ𝑎((𝜑 ∧ 𝐶 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ∈ 𝑆) |
18 | eleq1 2877 | . . . . . . 7 ⊢ (𝑎 = 𝐶 → (𝑎 ∈ ℝ ↔ 𝐶 ∈ ℝ)) | |
19 | 18 | anbi2d 631 | . . . . . 6 ⊢ (𝑎 = 𝐶 → ((𝜑 ∧ 𝑎 ∈ ℝ) ↔ (𝜑 ∧ 𝐶 ∈ ℝ))) |
20 | breq2 5034 | . . . . . . . 8 ⊢ (𝑎 = 𝐶 → (𝐵 ≤ 𝑎 ↔ 𝐵 ≤ 𝐶)) | |
21 | 20 | rabbidv 3427 | . . . . . . 7 ⊢ (𝑎 = 𝐶 → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎} = {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
22 | 21 | eleq1d 2874 | . . . . . 6 ⊢ (𝑎 = 𝐶 → ({𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎} ∈ 𝑆 ↔ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ∈ 𝑆)) |
23 | 19, 22 | imbi12d 348 | . . . . 5 ⊢ (𝑎 = 𝐶 → (((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎} ∈ 𝑆) ↔ ((𝜑 ∧ 𝐶 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ∈ 𝑆))) |
24 | salpreimalegt.p | . . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎} ∈ 𝑆) | |
25 | 17, 23, 24 | vtoclg1f 3514 | . . . 4 ⊢ (𝐶 ∈ ℝ → ((𝜑 ∧ 𝐶 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ∈ 𝑆)) |
26 | 7, 12, 25 | sylc 65 | . . 3 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ∈ 𝑆) |
27 | 11, 26 | saldifcld 42987 | . 2 ⊢ (𝜑 → (∪ 𝑆 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ∈ 𝑆) |
28 | 10, 27 | eqeltrd 2890 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} ∈ 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 Ⅎwnf 1785 ∈ wcel 2111 {crab 3110 ∖ cdif 3878 ∪ cuni 4800 class class class wbr 5030 ℝcr 10525 ℝ*cxr 10663 < clt 10664 ≤ cle 10665 SAlgcsalg 42950 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-xp 5525 df-cnv 5527 df-xr 10668 df-le 10670 df-salg 42951 |
This theorem is referenced by: salpreimalelt 43363 issmfgt 43390 |
Copyright terms: Public domain | W3C validator |