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 34184
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 7918 . . . . . 6 (𝑀 ran measures → dom 𝑀 ∈ V)
32uniexd 7754 . . . . 5 (𝑀 ran measures → dom 𝑀 ∈ V)
41, 3eqeltrrid 2842 . . . 4 (𝑀 ran measures → 𝑂 ∈ V)
5 rabexg 5338 . . . 4 (𝑂 ∈ V → {𝑥𝑂𝜑} ∈ V)
64, 5syl 17 . . 3 (𝑀 ran measures → {𝑥𝑂𝜑} ∈ V)
7 simpr 484 . . . . . 6 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → 𝑚 = 𝑀)
87dmeqd 5913 . . . . . . . 8 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → dom 𝑚 = dom 𝑀)
98unieqd 4927 . . . . . . 7 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → dom 𝑚 = dom 𝑀)
10 simpl 482 . . . . . . 7 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → 𝑎 = {𝑥𝑂𝜑})
119, 10difeq12d 4137 . . . . . 6 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → ( dom 𝑚𝑎) = ( dom 𝑀 ∖ {𝑥𝑂𝜑}))
127, 11fveq12d 6908 . . . . 5 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → (𝑚‘( dom 𝑚𝑎)) = (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})))
1312eqeq1d 2735 . . . 4 ((𝑎 = {𝑥𝑂𝜑} ∧ 𝑚 = 𝑀) → ((𝑚‘( dom 𝑚𝑎)) = 0 ↔ (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = 0))
14 df-ae 34181 . . . 4 a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
1513, 14brabga 5536 . . 3 (({𝑥𝑂𝜑} ∈ V ∧ 𝑀 ran measures) → ({𝑥𝑂𝜑}a.e.𝑀 ↔ (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = 0))
166, 15mpancom 687 . 2 (𝑀 ran measures → ({𝑥𝑂𝜑}a.e.𝑀 ↔ (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = 0))
171difeq1i 4132 . . . . 5 ( dom 𝑀 ∖ {𝑥𝑂𝜑}) = (𝑂 ∖ {𝑥𝑂𝜑})
18 notrab 4328 . . . . 5 (𝑂 ∖ {𝑥𝑂𝜑}) = {𝑥𝑂 ∣ ¬ 𝜑}
1917, 18eqtri 2761 . . . 4 ( dom 𝑀 ∖ {𝑥𝑂𝜑}) = {𝑥𝑂 ∣ ¬ 𝜑}
2019fveq2i 6904 . . 3 (𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = (𝑀‘{𝑥𝑂 ∣ ¬ 𝜑})
2120eqeq1i 2738 . 2 ((𝑀‘( dom 𝑀 ∖ {𝑥𝑂𝜑})) = 0 ↔ (𝑀‘{𝑥𝑂 ∣ ¬ 𝜑}) = 0)
2216, 21bitrdi 287 1 (𝑀 ran measures → ({𝑥𝑂𝜑}a.e.𝑀 ↔ (𝑀‘{𝑥𝑂 ∣ ¬ 𝜑}) = 0))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1535  wcel 2104  {crab 3432  Vcvv 3477  cdif 3960   cuni 4914   class class class wbr 5149  dom cdm 5683  ran crn 5684  cfv 6558  0cc0 11146  measurescmeas 34137  a.e.cae 34179
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-10 2137  ax-12 2173  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5430  ax-un 7747
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2711  df-cleq 2725  df-clel 2812  df-rab 3433  df-v 3479  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4915  df-br 5150  df-opab 5212  df-cnv 5691  df-dm 5693  df-rn 5694  df-iota 6510  df-fv 6566  df-ae 34181
This theorem is referenced by:  truae  34185  aean  34186
  Copyright terms: Public domain W3C validator