Metamath Proof Explorer

Theorem ismea

Description: Express the predicate " M is a measure." Definition 112A of Fremlin1 p. 14. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion ismea ⊢M∈Meas↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x

Proof

Step Hyp Ref Expression
1 id ⊢M∈Meas→M∈Meas
2 fex ⊢M:dom⁡M⟶0+∞∧dom⁡M∈SAlg→M∈V
3 id ⊢z=M→z=M
4 dmeq ⊢z=M→dom⁡z=dom⁡M
5 3 4 feq12d ⊢z=M→z:dom⁡z⟶0+∞↔M:dom⁡M⟶0+∞
6 4 eleq1d ⊢z=M→dom⁡z∈SAlg↔dom⁡M∈SAlg
7 5 6 anbi12d ⊢z=M→z:dom⁡z⟶0+∞∧dom⁡z∈SAlg↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg
8 fveq1 ⊢z=M→z⁡∅=M⁡∅
9 8 eqeq1d ⊢z=M→z⁡∅=0↔M⁡∅=0
10 7 9 anbi12d ⊢z=M→z:dom⁡z⟶0+∞∧dom⁡z∈SAlg∧z⁡∅=0↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0
11 4 pweqd ⊢z=M→𝒫dom⁡z=𝒫dom⁡M
12 fveq1 ⊢z=M→z⁡⋃x=M⁡⋃x
13 reseq1 ⊢z=M→z↾x=M↾x
14 13 fveq2d ⊢z=M→sum^⁡z↾x=sum^⁡M↾x
15 12 14 eqeq12d ⊢z=M→z⁡⋃x=sum^⁡z↾x↔M⁡⋃x=sum^⁡M↾x
16 15 imbi2d ⊢z=M→x≼ω∧Disjy∈xy→z⁡⋃x=sum^⁡z↾x↔x≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x
17 11 16 raleqbidv ⊢z=M→∀x∈𝒫dom⁡zx≼ω∧Disjy∈xy→z⁡⋃x=sum^⁡z↾x↔∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x
18 10 17 anbi12d ⊢z=M→z:dom⁡z⟶0+∞∧dom⁡z∈SAlg∧z⁡∅=0∧∀x∈𝒫dom⁡zx≼ω∧Disjy∈xy→z⁡⋃x=sum^⁡z↾x↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x
19 df-mea ⊢Meas=z|z:dom⁡z⟶0+∞∧dom⁡z∈SAlg∧z⁡∅=0∧∀x∈𝒫dom⁡zx≼ω∧Disjy∈xy→z⁡⋃x=sum^⁡z↾x
20 18 19 elab2g ⊢M∈V→M∈Meas↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x
21 2 20 syl ⊢M:dom⁡M⟶0+∞∧dom⁡M∈SAlg→M∈Meas↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x
22 21 ad2antrr ⊢M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x→M∈Meas↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x
23 22 ibir ⊢M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x→M∈Meas
24 18 19 elab2g ⊢M∈Meas→M∈Meas↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x
25 1 23 24 pm5.21nii ⊢M∈Meas↔M:dom⁡M⟶0+∞∧dom⁡M∈SAlg∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=sum^⁡M↾x