Metamath Proof Explorer

Theorem omef

Description: An outer measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypotheses	omef.o	$⊢ φ \to O \in OutMeas$
		omef.x	$⊢ X = ⋃ dom O$
	Assertion	omef	$⊢ φ \to O : 𝒫 X ⟶ [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		omef.o	$⊢ φ \to O \in OutMeas$
2		omef.x	$⊢ X = ⋃ dom O$
3		isome	$⊢ O \in OutMeas \to (O \in OutMeas \leftrightarrow ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom O \forall z \in 𝒫 y O (z) \leq O (y)) \land \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y}))))$
4	1 3	syl	$⊢ φ \to (O \in OutMeas \leftrightarrow ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom O \forall z \in 𝒫 y O (z) \leq O (y)) \land \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y}))))$
5	1 4	mpbid	$⊢ φ \to ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom O \forall z \in 𝒫 y O (z) \leq O (y)) \land \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y})))$
6	5	simplld	$⊢ φ \to ((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0)$
7	6	simplld	$⊢ φ \to O : dom O ⟶ [0, +∞]$
8	2	pweqi	$⊢ 𝒫 X = 𝒫 ⋃ dom O$
9		simp-4r	$⊢ ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom O \forall z \in 𝒫 y O (z) \leq O (y)) \land \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y}))) \to dom O = 𝒫 ⋃ dom O$
10	5 9	syl	$⊢ φ \to dom O = 𝒫 ⋃ dom O$
11	8 10	eqtr4id	$⊢ φ \to 𝒫 X = dom O$
12	11	feq2d	$⊢ φ \to (O : 𝒫 X ⟶ [0, +∞] \leftrightarrow O : dom O ⟶ [0, +∞])$
13	7 12	mpbird	$⊢ φ \to O : 𝒫 X ⟶ [0, +∞]$