Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  braew Structured version   Visualization version   GIF version

Theorem braew 31400
Description: 'almost everywhere' relation for a measure 𝑀 and a property 𝜑 (Contributed by Thierry Arnoux, 20-Oct-2017.)
Hypothesis
Ref Expression
braew.1 dom 𝑀 = 𝑂
Assertion
Ref Expression
braew (𝑀 ran measures → ({𝑥𝑂𝜑}a.e.𝑀 ↔ (𝑀‘{𝑥𝑂 ∣ ¬ 𝜑}) = 0))
Distinct variable group:   𝑥,𝑂
Allowed substitution hints:   𝜑(𝑥)   𝑀(𝑥)

Proof of Theorem braew
Dummy variables 𝑚 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 braew.1 . . . . 5 dom 𝑀 = 𝑂
2 dmexg 7602 . . . . . 6 (𝑀 ran measures → dom 𝑀 ∈ V)
32uniexd 7457 . . . . 5 (𝑀 ran measures → dom 𝑀 ∈ V)
41, 3eqeltrrid 2915 . . . 4 (𝑀 ran measures → 𝑂 ∈ V)
5 rabexg 5225 . . . 4 (𝑂 ∈ V → {𝑥𝑂𝜑} ∈ V)
64, 5syl 17 . . 3 (𝑀 ran measures → {𝑥𝑂𝜑} ∈ V)
7 simpr 485 . . . . . 6 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → 𝑚 = 𝑀)
87dmeqd 5767 . . . . . . . 8 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → dom 𝑚 = dom 𝑀)
98unieqd 4840 . . . . . . 7 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → dom 𝑚 = dom 𝑀)
10 simpl 483 . . . . . . 7 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → 𝑎 = {𝑥𝑂𝜑})
119, 10difeq12d 4097 . . . . . 6 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → ( dom 𝑚𝑎) = ( dom 𝑀 ∖ {𝑥𝑂𝜑}))
127, 11fveq12d 6670 . . . . 5 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → (𝑚‘( dom 𝑚𝑎)) = (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})))
1312eqeq1d 2820 . . . 4 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → ((𝑚‘( dom 𝑚𝑎)) = 0 ↔ (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = 0))
14 df-ae 31397 . . . 4 a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
1513, 14brabga 5412 . . 3 (({𝑥𝑂𝜑} ∈ V ∧ 𝑀 ran measures) → ({𝑥𝑂𝜑}a.e.𝑀 ↔ (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = 0))
166, 15mpancom 684 . 2 (𝑀 ran measures → ({𝑥𝑂𝜑}a.e.𝑀 ↔ (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = 0))
171difeq1i 4092 . . . . 5 ( dom 𝑀 ∖ {𝑥𝑂𝜑}) = (𝑂 ∖ {𝑥𝑂𝜑})
18 notrab 4277 . . . . 5 (𝑂 ∖ {𝑥𝑂𝜑}) = {𝑥𝑂 ∣ ¬ 𝜑}
1917, 18eqtri 2841 . . . 4 ( dom 𝑀 ∖ {𝑥𝑂𝜑}) = {𝑥𝑂 ∣ ¬ 𝜑}
2019fveq2i 6666 . . 3 (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = (𝑀‘{𝑥𝑂 ∣ ¬ 𝜑})
2120eqeq1i 2823 . 2 ((𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = 0 ↔ (𝑀‘{𝑥𝑂 ∣ ¬ 𝜑}) = 0)
2216, 21syl6bb 288 1 (𝑀 ran measures → ({𝑥𝑂𝜑}a.e.𝑀 ↔ (𝑀‘{𝑥𝑂 ∣ ¬ 𝜑}) = 0))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  {crab 3139  Vcvv 3492  cdif 3930   cuni 4830   class class class wbr 5057  dom cdm 5548  ran crn 5549  cfv 6348  0cc0 10525  measurescmeas 31353  a.e.cae 31395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-cnv 5556  df-dm 5558  df-rn 5559  df-iota 6307  df-fv 6356  df-ae 31397
This theorem is referenced by:  truae  31401  aean  31402
  Copyright terms: Public domain W3C validator