![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > isanmbfm | Structured version Visualization version GIF version |
Description: The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
Ref | Expression |
---|---|
mbfmf.1 | ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) |
mbfmf.2 | ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra) |
mbfmf.3 | ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇)) |
Ref | Expression |
---|---|
isanmbfm | ⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mbfmf.1 | . . 3 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) | |
2 | mbfmf.2 | . . 3 ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra) | |
3 | mbfmf.3 | . . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇)) | |
4 | 1, 2 | ismbfm 31119 | . . . 4 ⊢ (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹 ∈ (∪ 𝑇 ↑𝑚 ∪ 𝑆) ∧ ∀𝑥 ∈ 𝑇 (◡𝐹 “ 𝑥) ∈ 𝑆))) |
5 | 3, 4 | mpbid 233 | . . 3 ⊢ (𝜑 → (𝐹 ∈ (∪ 𝑇 ↑𝑚 ∪ 𝑆) ∧ ∀𝑥 ∈ 𝑇 (◡𝐹 “ 𝑥) ∈ 𝑆)) |
6 | unieq 4755 | . . . . . . 7 ⊢ (𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆) | |
7 | 6 | oveq2d 7035 | . . . . . 6 ⊢ (𝑠 = 𝑆 → (∪ 𝑡 ↑𝑚 ∪ 𝑠) = (∪ 𝑡 ↑𝑚 ∪ 𝑆)) |
8 | 7 | eleq2d 2867 | . . . . 5 ⊢ (𝑠 = 𝑆 → (𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑠) ↔ 𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑆))) |
9 | eleq2 2870 | . . . . . 6 ⊢ (𝑠 = 𝑆 → ((◡𝐹 “ 𝑥) ∈ 𝑠 ↔ (◡𝐹 “ 𝑥) ∈ 𝑆)) | |
10 | 9 | ralbidv 3163 | . . . . 5 ⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑠 ↔ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑆)) |
11 | 8, 10 | anbi12d 630 | . . . 4 ⊢ (𝑠 = 𝑆 → ((𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑠) ∧ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑠) ↔ (𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑆) ∧ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑆))) |
12 | unieq 4755 | . . . . . . 7 ⊢ (𝑡 = 𝑇 → ∪ 𝑡 = ∪ 𝑇) | |
13 | 12 | oveq1d 7034 | . . . . . 6 ⊢ (𝑡 = 𝑇 → (∪ 𝑡 ↑𝑚 ∪ 𝑆) = (∪ 𝑇 ↑𝑚 ∪ 𝑆)) |
14 | 13 | eleq2d 2867 | . . . . 5 ⊢ (𝑡 = 𝑇 → (𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑆) ↔ 𝐹 ∈ (∪ 𝑇 ↑𝑚 ∪ 𝑆))) |
15 | raleq 3364 | . . . . 5 ⊢ (𝑡 = 𝑇 → (∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑆 ↔ ∀𝑥 ∈ 𝑇 (◡𝐹 “ 𝑥) ∈ 𝑆)) | |
16 | 14, 15 | anbi12d 630 | . . . 4 ⊢ (𝑡 = 𝑇 → ((𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑆) ∧ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑆) ↔ (𝐹 ∈ (∪ 𝑇 ↑𝑚 ∪ 𝑆) ∧ ∀𝑥 ∈ 𝑇 (◡𝐹 “ 𝑥) ∈ 𝑆))) |
17 | 11, 16 | rspc2ev 3572 | . . 3 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ (𝐹 ∈ (∪ 𝑇 ↑𝑚 ∪ 𝑆) ∧ ∀𝑥 ∈ 𝑇 (◡𝐹 “ 𝑥) ∈ 𝑆)) → ∃𝑠 ∈ ∪ ran sigAlgebra∃𝑡 ∈ ∪ ran sigAlgebra(𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑠) ∧ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑠)) |
18 | 1, 2, 5, 17 | syl3anc 1364 | . 2 ⊢ (𝜑 → ∃𝑠 ∈ ∪ ran sigAlgebra∃𝑡 ∈ ∪ ran sigAlgebra(𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑠) ∧ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑠)) |
19 | elunirnmbfm 31120 | . 2 ⊢ (𝐹 ∈ ∪ ran MblFnM ↔ ∃𝑠 ∈ ∪ ran sigAlgebra∃𝑡 ∈ ∪ ran sigAlgebra(𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑠) ∧ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑠)) | |
20 | 18, 19 | sylibr 235 | 1 ⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2080 ∀wral 3104 ∃wrex 3105 ∪ cuni 4747 ◡ccnv 5445 ran crn 5447 “ cima 5449 (class class class)co 7019 ↑𝑚 cmap 8259 sigAlgebracsiga 30976 MblFnMcmbfm 31117 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-ral 3109 df-rex 3110 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-iun 4829 df-br 4965 df-opab 5027 df-mpt 5044 df-id 5351 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-fv 6236 df-ov 7022 df-oprab 7023 df-mpo 7024 df-1st 7548 df-2nd 7549 df-mbfm 31118 |
This theorem is referenced by: mbfmbfm 31125 orvcval4 31327 |
Copyright terms: Public domain | W3C validator |