![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mbfid | Structured version Visualization version GIF version |
Description: The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
Ref | Expression |
---|---|
mbfid | ⊢ (𝐴 ∈ dom vol → ( I ↾ 𝐴) ∈ MblFn) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvresima 6187 | . . . . 5 ⊢ (◡( I ↾ 𝐴) “ 𝑥) = ((◡ I “ 𝑥) ∩ 𝐴) | |
2 | cnvi 6099 | . . . . . . . 8 ⊢ ◡ I = I | |
3 | 2 | imaeq1i 6015 | . . . . . . 7 ⊢ (◡ I “ 𝑥) = ( I “ 𝑥) |
4 | imai 6031 | . . . . . . 7 ⊢ ( I “ 𝑥) = 𝑥 | |
5 | 3, 4 | eqtri 2759 | . . . . . 6 ⊢ (◡ I “ 𝑥) = 𝑥 |
6 | 5 | ineq1i 4173 | . . . . 5 ⊢ ((◡ I “ 𝑥) ∩ 𝐴) = (𝑥 ∩ 𝐴) |
7 | 1, 6 | eqtri 2759 | . . . 4 ⊢ (◡( I ↾ 𝐴) “ 𝑥) = (𝑥 ∩ 𝐴) |
8 | ioof 13374 | . . . . . . 7 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ | |
9 | ffn 6673 | . . . . . . 7 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*)) | |
10 | ovelrn 7535 | . . . . . . 7 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑥 ∈ ran (,) ↔ ∃𝑦 ∈ ℝ* ∃𝑧 ∈ ℝ* 𝑥 = (𝑦(,)𝑧))) | |
11 | 8, 9, 10 | mp2b 10 | . . . . . 6 ⊢ (𝑥 ∈ ran (,) ↔ ∃𝑦 ∈ ℝ* ∃𝑧 ∈ ℝ* 𝑥 = (𝑦(,)𝑧)) |
12 | id 22 | . . . . . . . . 9 ⊢ (𝑥 = (𝑦(,)𝑧) → 𝑥 = (𝑦(,)𝑧)) | |
13 | ioombl 24966 | . . . . . . . . 9 ⊢ (𝑦(,)𝑧) ∈ dom vol | |
14 | 12, 13 | eqeltrdi 2840 | . . . . . . . 8 ⊢ (𝑥 = (𝑦(,)𝑧) → 𝑥 ∈ dom vol) |
15 | 14 | a1i 11 | . . . . . . 7 ⊢ ((𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → (𝑥 = (𝑦(,)𝑧) → 𝑥 ∈ dom vol)) |
16 | 15 | rexlimivv 3192 | . . . . . 6 ⊢ (∃𝑦 ∈ ℝ* ∃𝑧 ∈ ℝ* 𝑥 = (𝑦(,)𝑧) → 𝑥 ∈ dom vol) |
17 | 11, 16 | sylbi 216 | . . . . 5 ⊢ (𝑥 ∈ ran (,) → 𝑥 ∈ dom vol) |
18 | id 22 | . . . . 5 ⊢ (𝐴 ∈ dom vol → 𝐴 ∈ dom vol) | |
19 | inmbl 24943 | . . . . 5 ⊢ ((𝑥 ∈ dom vol ∧ 𝐴 ∈ dom vol) → (𝑥 ∩ 𝐴) ∈ dom vol) | |
20 | 17, 18, 19 | syl2anr 597 | . . . 4 ⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ ran (,)) → (𝑥 ∩ 𝐴) ∈ dom vol) |
21 | 7, 20 | eqeltrid 2836 | . . 3 ⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ ran (,)) → (◡( I ↾ 𝐴) “ 𝑥) ∈ dom vol) |
22 | 21 | ralrimiva 3139 | . 2 ⊢ (𝐴 ∈ dom vol → ∀𝑥 ∈ ran (,)(◡( I ↾ 𝐴) “ 𝑥) ∈ dom vol) |
23 | f1oi 6827 | . . . . 5 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
24 | f1of 6789 | . . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) | |
25 | 23, 24 | ax-mp 5 | . . . 4 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴 |
26 | mblss 24932 | . . . 4 ⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ) | |
27 | fss 6690 | . . . 4 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ ℝ) → ( I ↾ 𝐴):𝐴⟶ℝ) | |
28 | 25, 26, 27 | sylancr 587 | . . 3 ⊢ (𝐴 ∈ dom vol → ( I ↾ 𝐴):𝐴⟶ℝ) |
29 | ismbf 25029 | . . 3 ⊢ (( I ↾ 𝐴):𝐴⟶ℝ → (( I ↾ 𝐴) ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡( I ↾ 𝐴) “ 𝑥) ∈ dom vol)) | |
30 | 28, 29 | syl 17 | . 2 ⊢ (𝐴 ∈ dom vol → (( I ↾ 𝐴) ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡( I ↾ 𝐴) “ 𝑥) ∈ dom vol)) |
31 | 22, 30 | mpbird 256 | 1 ⊢ (𝐴 ∈ dom vol → ( I ↾ 𝐴) ∈ MblFn) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3060 ∃wrex 3069 ∩ cin 3912 ⊆ wss 3913 𝒫 cpw 4565 I cid 5535 × cxp 5636 ◡ccnv 5637 dom cdm 5638 ran crn 5639 ↾ cres 5640 “ cima 5641 Fn wfn 6496 ⟶wf 6497 –1-1-onto→wf1o 6500 (class class class)co 7362 ℝcr 11059 ℝ*cxr 11197 (,)cioo 13274 volcvol 24864 MblFncmbf 25015 |
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 2702 ax-rep 5247 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-inf2 9586 ax-cnex 11116 ax-resscn 11117 ax-1cn 11118 ax-icn 11119 ax-addcl 11120 ax-addrcl 11121 ax-mulcl 11122 ax-mulrcl 11123 ax-mulcom 11124 ax-addass 11125 ax-mulass 11126 ax-distr 11127 ax-i2m1 11128 ax-1ne0 11129 ax-1rid 11130 ax-rnegex 11131 ax-rrecex 11132 ax-cnre 11133 ax-pre-lttri 11134 ax-pre-lttrn 11135 ax-pre-ltadd 11136 ax-pre-mulgt0 11137 ax-pre-sup 11138 |
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 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3448 df-sbc 3743 df-csb 3859 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3932 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-int 4913 df-iun 4961 df-br 5111 df-opab 5173 df-mpt 5194 df-tr 5228 df-id 5536 df-eprel 5542 df-po 5550 df-so 5551 df-fr 5593 df-se 5594 df-we 5595 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6258 df-ord 6325 df-on 6326 df-lim 6327 df-suc 6328 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-isom 6510 df-riota 7318 df-ov 7365 df-oprab 7366 df-mpo 7367 df-of 7622 df-om 7808 df-1st 7926 df-2nd 7927 df-frecs 8217 df-wrecs 8248 df-recs 8322 df-rdg 8361 df-1o 8417 df-2o 8418 df-er 8655 df-map 8774 df-pm 8775 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-sup 9387 df-inf 9388 df-oi 9455 df-dju 9846 df-card 9884 df-pnf 11200 df-mnf 11201 df-xr 11202 df-ltxr 11203 df-le 11204 df-sub 11396 df-neg 11397 df-div 11822 df-nn 12163 df-2 12225 df-3 12226 df-n0 12423 df-z 12509 df-uz 12773 df-q 12883 df-rp 12925 df-xadd 13043 df-ioo 13278 df-ico 13280 df-icc 13281 df-fz 13435 df-fzo 13578 df-fl 13707 df-seq 13917 df-exp 13978 df-hash 14241 df-cj 14996 df-re 14997 df-im 14998 df-sqrt 15132 df-abs 15133 df-clim 15382 df-rlim 15383 df-sum 15583 df-xmet 20826 df-met 20827 df-ovol 24865 df-vol 24866 df-mbf 25020 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |