omessle

Description: The outer measure of a set is greater than or equal to the measure of a subset, Definition 113A (ii) of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omessle.o	$⊢ φ \to O \in OutMeas$
	omessle.x	$⊢ X = ⋃ dom O$
	omessle.b	$⊢ φ \to B \subseteq X$
	omessle.a	$⊢ φ \to A \subseteq B$
Assertion	omessle	$⊢ φ \to O (A) \leq O (B)$

Proof

Step	Hyp	Ref	Expression
1		omessle.o	$⊢ φ \to O \in OutMeas$
2		omessle.x	$⊢ X = ⋃ dom O$
3		omessle.b	$⊢ φ \to B \subseteq X$
4		omessle.a	$⊢ φ \to A \subseteq B$
5	1 2	unidmex	$⊢ φ \to X \in V$
6	5 3	ssexd	$⊢ φ \to B \in V$
7	6 4	ssexd	$⊢ φ \to A \in V$
8		elpwg	$⊢ A \in V \to (A \in 𝒫 B \leftrightarrow A \subseteq B)$
9	7 8	syl	$⊢ φ \to (A \in 𝒫 B \leftrightarrow A \subseteq B)$
10	4 9	mpbird	$⊢ φ \to A \in 𝒫 B$
11	3 2	sseqtrdi	$⊢ φ \to B \subseteq ⋃ dom O$
12		elpwg	$⊢ B \in V \to (B \in 𝒫 ⋃ dom O \leftrightarrow B \subseteq ⋃ dom O)$
13	6 12	syl	$⊢ φ \to (B \in 𝒫 ⋃ dom O \leftrightarrow B \subseteq ⋃ dom O)$
14	11 13	mpbird	$⊢ φ \to B \in 𝒫 ⋃ dom O$
15		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}))))$
16	1 15	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}))))$
17	1 16	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})))$
18	17	simplrd	$⊢ φ \to \forall y \in 𝒫 ⋃ dom O \forall z \in 𝒫 y O (z) \leq O (y)$
19		pweq	$⊢ y = B \to 𝒫 y = 𝒫 B$
20	19	raleqdv	$⊢ y = B \to (\forall z \in 𝒫 y O (z) \leq O (y) \leftrightarrow \forall z \in 𝒫 B O (z) \leq O (y))$
21		fveq2	$⊢ y = B \to O (y) = O (B)$
22	21	breq2d	$⊢ y = B \to (O (z) \leq O (y) \leftrightarrow O (z) \leq O (B))$
23	22	ralbidv	$⊢ y = B \to (\forall z \in 𝒫 B O (z) \leq O (y) \leftrightarrow \forall z \in 𝒫 B O (z) \leq O (B))$
24	20 23	bitrd	$⊢ y = B \to (\forall z \in 𝒫 y O (z) \leq O (y) \leftrightarrow \forall z \in 𝒫 B O (z) \leq O (B))$
25	24	rspcva	$⊢ (B \in 𝒫 ⋃ dom O \land \forall y \in 𝒫 ⋃ dom O \forall z \in 𝒫 y O (z) \leq O (y)) \to \forall z \in 𝒫 B O (z) \leq O (B)$
26	14 18 25	syl2anc	$⊢ φ \to \forall z \in 𝒫 B O (z) \leq O (B)$
27		fveq2	$⊢ z = A \to O (z) = O (A)$
28	27	breq1d	$⊢ z = A \to (O (z) \leq O (B) \leftrightarrow O (A) \leq O (B))$
29	28	rspcva	$⊢ (A \in 𝒫 B \land \forall z \in 𝒫 B O (z) \leq O (B)) \to O (A) \leq O (B)$
30	10 26 29	syl2anc	$⊢ φ \to O (A) \leq O (B)$

Metamath Proof Explorer

Theorem omessle

Proof