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 ⁡ M x ≼ ω ∧ Disj y ∈ x y → 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 ≼ ω ∧ Disj y ∈ x y → z ⁡ ⋃ x = sum^ ⁡ z ↾ x ↔ x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x
17 11 16 raleqbidv ⊢ z = M → ∀ x ∈ 𝒫 dom ⁡ z x ≼ ω ∧ Disj y ∈ x y → z ⁡ ⋃ x = sum^ ⁡ z ↾ x ↔ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x
18 10 17 anbi12d ⊢ z = M → z : dom ⁡ z ⟶ 0 +∞ ∧ dom ⁡ z ∈ SAlg ∧ z ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ z x ≼ ω ∧ Disj y ∈ x y → z ⁡ ⋃ x = sum^ ⁡ z ↾ x ↔ M : dom ⁡ M ⟶ 0 +∞ ∧ dom ⁡ M ∈ SAlg ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x
19 df-mea ⊢ Meas = z | z : dom ⁡ z ⟶ 0 +∞ ∧ dom ⁡ z ∈ SAlg ∧ z ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ z x ≼ ω ∧ Disj y ∈ x y → z ⁡ ⋃ x = sum^ ⁡ z ↾ x
20 18 19 elab2g ⊢ M ∈ V → M ∈ Meas ↔ M : dom ⁡ M ⟶ 0 +∞ ∧ dom ⁡ M ∈ SAlg ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → 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 ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x
22 21 ad2antrr ⊢ M : dom ⁡ M ⟶ 0 +∞ ∧ dom ⁡ M ∈ SAlg ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x → M ∈ Meas ↔ M : dom ⁡ M ⟶ 0 +∞ ∧ dom ⁡ M ∈ SAlg ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x
23 22 ibir ⊢ M : dom ⁡ M ⟶ 0 +∞ ∧ dom ⁡ M ∈ SAlg ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → 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 ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x
25 1 23 24 pm5.21nii ⊢ M ∈ Meas ↔ M : dom ⁡ M ⟶ 0 +∞ ∧ dom ⁡ M ∈ SAlg ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x