MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunmbl2 Structured version   Visualization version   GIF version

Theorem iunmbl2 24139
Description: The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.)
Assertion
Ref Expression
iunmbl2 ((𝐴 ≼ ℕ ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) → 𝑛𝐴 𝐵 ∈ dom vol)
Distinct variable group:   𝐴,𝑛
Allowed substitution hint:   𝐵(𝑛)

Proof of Theorem iunmbl2
Dummy variables 𝑓 𝑘 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdom2 8514 . . 3 (𝐴 ≼ ℕ ↔ (𝐴 ≺ ℕ ∨ 𝐴 ≈ ℕ))
2 nnenom 13331 . . . . . 6 ℕ ≈ ω
3 sdomentr 8627 . . . . . 6 ((𝐴 ≺ ℕ ∧ ℕ ≈ ω) → 𝐴 ≺ ω)
42, 3mpan2 690 . . . . 5 (𝐴 ≺ ℕ → 𝐴 ≺ ω)
5 isfinite 9091 . . . . . 6 (𝐴 ∈ Fin ↔ 𝐴 ≺ ω)
6 finiunmbl 24126 . . . . . . 7 ((𝐴 ∈ Fin ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) → 𝑛𝐴 𝐵 ∈ dom vol)
76ex 416 . . . . . 6 (𝐴 ∈ Fin → (∀𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol))
85, 7sylbir 238 . . . . 5 (𝐴 ≺ ω → (∀𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol))
94, 8syl 17 . . . 4 (𝐴 ≺ ℕ → (∀𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol))
10 bren 8493 . . . . 5 (𝐴 ≈ ℕ ↔ ∃𝑓 𝑓:𝐴1-1-onto→ℕ)
11 nfv 1916 . . . . . . . . . . . . 13 𝑛 𝑓:𝐴1-1-onto→ℕ
12 nfcv 2974 . . . . . . . . . . . . . 14 𝑛
13 nfcsb1v 3881 . . . . . . . . . . . . . . 15 𝑛(𝑓𝑘) / 𝑛𝐵
1413nfcri 2968 . . . . . . . . . . . . . 14 𝑛 𝑥(𝑓𝑘) / 𝑛𝐵
1512, 14nfrex 3295 . . . . . . . . . . . . 13 𝑛𝑘 ∈ ℕ 𝑥(𝑓𝑘) / 𝑛𝐵
16 f1of 6588 . . . . . . . . . . . . . . . . 17 (𝑓:𝐴1-1-onto→ℕ → 𝑓:𝐴⟶ℕ)
1716ffvelrnda 6824 . . . . . . . . . . . . . . . 16 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑛𝐴) → (𝑓𝑛) ∈ ℕ)
18173adant3 1129 . . . . . . . . . . . . . . 15 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑛𝐴𝑥𝐵) → (𝑓𝑛) ∈ ℕ)
19 simp3 1135 . . . . . . . . . . . . . . . 16 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑛𝐴𝑥𝐵) → 𝑥𝐵)
20 f1ocnvfv1 7007 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑛𝐴) → (𝑓‘(𝑓𝑛)) = 𝑛)
21203adant3 1129 . . . . . . . . . . . . . . . . . 18 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑛𝐴𝑥𝐵) → (𝑓‘(𝑓𝑛)) = 𝑛)
2221eqcomd 2827 . . . . . . . . . . . . . . . . 17 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑛𝐴𝑥𝐵) → 𝑛 = (𝑓‘(𝑓𝑛)))
23 csbeq1a 3871 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑓‘(𝑓𝑛)) → 𝐵 = (𝑓‘(𝑓𝑛)) / 𝑛𝐵)
2422, 23syl 17 . . . . . . . . . . . . . . . 16 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑛𝐴𝑥𝐵) → 𝐵 = (𝑓‘(𝑓𝑛)) / 𝑛𝐵)
2519, 24eleqtrd 2914 . . . . . . . . . . . . . . 15 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑛𝐴𝑥𝐵) → 𝑥(𝑓‘(𝑓𝑛)) / 𝑛𝐵)
26 fveq2 6643 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑓𝑛) → (𝑓𝑘) = (𝑓‘(𝑓𝑛)))
2726csbeq1d 3861 . . . . . . . . . . . . . . . . 17 (𝑘 = (𝑓𝑛) → (𝑓𝑘) / 𝑛𝐵 = (𝑓‘(𝑓𝑛)) / 𝑛𝐵)
2827eleq2d 2897 . . . . . . . . . . . . . . . 16 (𝑘 = (𝑓𝑛) → (𝑥(𝑓𝑘) / 𝑛𝐵𝑥(𝑓‘(𝑓𝑛)) / 𝑛𝐵))
2928rspcev 3600 . . . . . . . . . . . . . . 15 (((𝑓𝑛) ∈ ℕ ∧ 𝑥(𝑓‘(𝑓𝑛)) / 𝑛𝐵) → ∃𝑘 ∈ ℕ 𝑥(𝑓𝑘) / 𝑛𝐵)
3018, 25, 29syl2anc 587 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑛𝐴𝑥𝐵) → ∃𝑘 ∈ ℕ 𝑥(𝑓𝑘) / 𝑛𝐵)
31303exp 1116 . . . . . . . . . . . . 13 (𝑓:𝐴1-1-onto→ℕ → (𝑛𝐴 → (𝑥𝐵 → ∃𝑘 ∈ ℕ 𝑥(𝑓𝑘) / 𝑛𝐵)))
3211, 15, 31rexlimd 3303 . . . . . . . . . . . 12 (𝑓:𝐴1-1-onto→ℕ → (∃𝑛𝐴 𝑥𝐵 → ∃𝑘 ∈ ℕ 𝑥(𝑓𝑘) / 𝑛𝐵))
33 f1ocnvdm 7015 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) → (𝑓𝑘) ∈ 𝐴)
34 csbeq1a 3871 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑓𝑘) → 𝐵 = (𝑓𝑘) / 𝑛𝐵)
3534eleq2d 2897 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑓𝑘) → (𝑥𝐵𝑥(𝑓𝑘) / 𝑛𝐵))
3614, 35rspce 3589 . . . . . . . . . . . . . . 15 (((𝑓𝑘) ∈ 𝐴𝑥(𝑓𝑘) / 𝑛𝐵) → ∃𝑛𝐴 𝑥𝐵)
3736ex 416 . . . . . . . . . . . . . 14 ((𝑓𝑘) ∈ 𝐴 → (𝑥(𝑓𝑘) / 𝑛𝐵 → ∃𝑛𝐴 𝑥𝐵))
3833, 37syl 17 . . . . . . . . . . . . 13 ((𝑓:𝐴1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) → (𝑥(𝑓𝑘) / 𝑛𝐵 → ∃𝑛𝐴 𝑥𝐵))
3938rexlimdva 3270 . . . . . . . . . . . 12 (𝑓:𝐴1-1-onto→ℕ → (∃𝑘 ∈ ℕ 𝑥(𝑓𝑘) / 𝑛𝐵 → ∃𝑛𝐴 𝑥𝐵))
4032, 39impbid 215 . . . . . . . . . . 11 (𝑓:𝐴1-1-onto→ℕ → (∃𝑛𝐴 𝑥𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥(𝑓𝑘) / 𝑛𝐵))
41 eliun 4896 . . . . . . . . . . 11 (𝑥 𝑛𝐴 𝐵 ↔ ∃𝑛𝐴 𝑥𝐵)
42 eliun 4896 . . . . . . . . . . 11 (𝑥 𝑘 ∈ ℕ (𝑓𝑘) / 𝑛𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥(𝑓𝑘) / 𝑛𝐵)
4340, 41, 423bitr4g 317 . . . . . . . . . 10 (𝑓:𝐴1-1-onto→ℕ → (𝑥 𝑛𝐴 𝐵𝑥 𝑘 ∈ ℕ (𝑓𝑘) / 𝑛𝐵))
4443eqrdv 2819 . . . . . . . . 9 (𝑓:𝐴1-1-onto→ℕ → 𝑛𝐴 𝐵 = 𝑘 ∈ ℕ (𝑓𝑘) / 𝑛𝐵)
4544adantr 484 . . . . . . . 8 ((𝑓:𝐴1-1-onto→ℕ ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) → 𝑛𝐴 𝐵 = 𝑘 ∈ ℕ (𝑓𝑘) / 𝑛𝐵)
46 rspcsbela 4360 . . . . . . . . . . . 12 (((𝑓𝑘) ∈ 𝐴 ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) → (𝑓𝑘) / 𝑛𝐵 ∈ dom vol)
4733, 46sylan 583 . . . . . . . . . . 11 (((𝑓:𝐴1-1-onto→ℕ ∧ 𝑘 ∈ ℕ) ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) → (𝑓𝑘) / 𝑛𝐵 ∈ dom vol)
4847an32s 651 . . . . . . . . . 10 (((𝑓:𝐴1-1-onto→ℕ ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ ℕ) → (𝑓𝑘) / 𝑛𝐵 ∈ dom vol)
4948ralrimiva 3170 . . . . . . . . 9 ((𝑓:𝐴1-1-onto→ℕ ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) → ∀𝑘 ∈ ℕ (𝑓𝑘) / 𝑛𝐵 ∈ dom vol)
50 iunmbl 24135 . . . . . . . . 9 (∀𝑘 ∈ ℕ (𝑓𝑘) / 𝑛𝐵 ∈ dom vol → 𝑘 ∈ ℕ (𝑓𝑘) / 𝑛𝐵 ∈ dom vol)
5149, 50syl 17 . . . . . . . 8 ((𝑓:𝐴1-1-onto→ℕ ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) → 𝑘 ∈ ℕ (𝑓𝑘) / 𝑛𝐵 ∈ dom vol)
5245, 51eqeltrd 2912 . . . . . . 7 ((𝑓:𝐴1-1-onto→ℕ ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) → 𝑛𝐴 𝐵 ∈ dom vol)
5352ex 416 . . . . . 6 (𝑓:𝐴1-1-onto→ℕ → (∀𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol))
5453exlimiv 1932 . . . . 5 (∃𝑓 𝑓:𝐴1-1-onto→ℕ → (∀𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol))
5510, 54sylbi 220 . . . 4 (𝐴 ≈ ℕ → (∀𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol))
569, 55jaoi 854 . . 3 ((𝐴 ≺ ℕ ∨ 𝐴 ≈ ℕ) → (∀𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol))
571, 56sylbi 220 . 2 (𝐴 ≼ ℕ → (∀𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol))
5857imp 410 1 ((𝐴 ≼ ℕ ∧ ∀𝑛𝐴 𝐵 ∈ dom vol) → 𝑛𝐴 𝐵 ∈ dom vol)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wo 844  w3a 1084   = wceq 1538  wex 1781  wcel 2115  wral 3126  wrex 3127  csb 3857   ciun 4892   class class class wbr 5039  ccnv 5527  dom cdm 5528  1-1-ontowf1o 6327  cfv 6328  ωcom 7555  cen 8481  cdom 8482  csdm 8483  Fincfn 8484  cn 11615  volcvol 24045
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-inf2 9080  ax-cc 9834  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591  ax-pre-sup 10592
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-disj 5005  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-of 7384  df-om 7556  df-1st 7664  df-2nd 7665  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-2o 8078  df-oadd 8081  df-er 8264  df-map 8383  df-pm 8384  df-en 8485  df-dom 8486  df-sdom 8487  df-fin 8488  df-sup 8882  df-inf 8883  df-oi 8950  df-dju 9306  df-card 9344  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-div 11275  df-nn 11616  df-2 11678  df-3 11679  df-n0 11876  df-z 11960  df-uz 12222  df-q 12327  df-rp 12368  df-xadd 12486  df-ioo 12720  df-ico 12722  df-icc 12723  df-fz 12876  df-fzo 13017  df-fl 13145  df-seq 13353  df-exp 13414  df-hash 13675  df-cj 14437  df-re 14438  df-im 14439  df-sqrt 14573  df-abs 14574  df-clim 14824  df-rlim 14825  df-sum 15022  df-xmet 20513  df-met 20514  df-ovol 24046  df-vol 24047
This theorem is referenced by:  opnmblALT  24185  mbfimaopnlem  24237  mbfaddlem  24242  mbfsup  24246  dmvlsiga  31395
  Copyright terms: Public domain W3C validator