ome0

Description: The outer measure of the empty set is 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypothesis	ome0.1	$⊢ φ \to O \in OutMeas$
	Assertion	ome0	$⊢ φ \to O (\emptyset) = 0$

Step	Hyp	Ref	Expression
1		ome0.1	$⊢ φ \to O \in OutMeas$
2		isome	$⊢ O \in OutMeas \to (O \in OutMeas \leftrightarrow ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall x \in 𝒫 ⋃ dom O \forall y \in 𝒫 x O (y) \leq O (x)) \land \forall x \in 𝒫 dom O (x ≼ ω \to O (⋃ x) \leq sum^({O ↾}_{x}))))$
3	1 2	syl	$⊢ φ \to (O \in OutMeas \leftrightarrow ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall x \in 𝒫 ⋃ dom O \forall y \in 𝒫 x O (y) \leq O (x)) \land \forall x \in 𝒫 dom O (x ≼ ω \to O (⋃ x) \leq sum^({O ↾}_{x}))))$
4	1 3	mpbid	$⊢ φ \to ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall x \in 𝒫 ⋃ dom O \forall y \in 𝒫 x O (y) \leq O (x)) \land \forall x \in 𝒫 dom O (x ≼ ω \to O (⋃ x) \leq sum^({O ↾}_{x})))$
5	4	simplld	$⊢ φ \to ((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0)$
6	5	simprd	$⊢ φ \to O (\emptyset) = 0$

Metamath Proof Explorer