isome

Description: Express the predicate " O is an outer measure." Definition 113A of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	isome	$⊢ O \in V \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}))))$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ x = O \to x = O$
2		dmeq	$⊢ x = O \to dom x = dom O$
3	1 2	feq12d	$⊢ x = O \to (x : dom x ⟶ [0, +∞] \leftrightarrow O : dom O ⟶ [0, +∞])$
4	2	unieqd	$⊢ x = O \to ⋃ dom x = ⋃ dom O$
5	4	pweqd	$⊢ x = O \to 𝒫 ⋃ dom x = 𝒫 ⋃ dom O$
6	2 5	eqeq12d	$⊢ x = O \to (dom x = 𝒫 ⋃ dom x \leftrightarrow dom O = 𝒫 ⋃ dom O)$
7	3 6	anbi12d	$⊢ x = O \to ((x : dom x ⟶ [0, +∞] \land dom x = 𝒫 ⋃ dom x) \leftrightarrow (O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O))$
8		fveq1	$⊢ x = O \to x (\emptyset) = O (\emptyset)$
9	8	eqeq1d	$⊢ x = O \to (x (\emptyset) = 0 \leftrightarrow O (\emptyset) = 0)$
10	7 9	anbi12d	$⊢ x = O \to (((x : dom x ⟶ [0, +∞] \land dom x = 𝒫 ⋃ dom x) \land x (\emptyset) = 0) \leftrightarrow ((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0))$
11		fveq1	$⊢ x = O \to x (z) = O (z)$
12		fveq1	$⊢ x = O \to x (y) = O (y)$
13	11 12	breq12d	$⊢ x = O \to (x (z) \leq x (y) \leftrightarrow O (z) \leq O (y))$
14	13	ralbidv	$⊢ x = O \to (\forall z \in 𝒫 y x (z) \leq x (y) \leftrightarrow \forall z \in 𝒫 y O (z) \leq O (y))$
15	5 14	raleqbidv	$⊢ x = O \to (\forall y \in 𝒫 ⋃ dom x \forall z \in 𝒫 y x (z) \leq x (y) \leftrightarrow \forall y \in 𝒫 ⋃ dom O \forall z \in 𝒫 y O (z) \leq O (y))$
16	10 15	anbi12d	$⊢ x = O \to ((((x : dom x ⟶ [0, +∞] \land dom x = 𝒫 ⋃ dom x) \land x (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom x \forall z \in 𝒫 y x (z) \leq x (y)) \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)))$
17	2	pweqd	$⊢ x = O \to 𝒫 dom x = 𝒫 dom O$
18		fveq1	$⊢ x = O \to x (⋃ y) = O (⋃ y)$
19		reseq1	$⊢ x = O \to {x ↾}_{y} = {O ↾}_{y}$
20	19	fveq2d	$⊢ x = O \to sum^({x ↾}_{y}) = sum^({O ↾}_{y})$
21	18 20	breq12d	$⊢ x = O \to (x (⋃ y) \leq sum^({x ↾}_{y}) \leftrightarrow O (⋃ y) \leq sum^({O ↾}_{y}))$
22	21	imbi2d	$⊢ x = O \to ((y ≼ ω \to x (⋃ y) \leq sum^({x ↾}_{y})) \leftrightarrow (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y})))$
23	17 22	raleqbidv	$⊢ x = O \to (\forall y \in 𝒫 dom x (y ≼ ω \to x (⋃ y) \leq sum^({x ↾}_{y})) \leftrightarrow \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y})))$
24	16 23	anbi12d	$⊢ x = O \to (((((x : dom x ⟶ [0, +∞] \land dom x = 𝒫 ⋃ dom x) \land x (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom x \forall z \in 𝒫 y x (z) \leq x (y)) \land \forall y \in 𝒫 dom x (y ≼ ω \to x (⋃ y) \leq sum^({x ↾}_{y}))) \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}))))$
25		df-ome	$⊢ OutMeas = \{x \| ((((x : dom x ⟶ [0, +∞] \land dom x = 𝒫 ⋃ dom x) \land x (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom x \forall z \in 𝒫 y x (z) \leq x (y)) \land \forall y \in 𝒫 dom x (y ≼ ω \to x (⋃ y) \leq sum^({x ↾}_{y})))\}$
26	24 25	elab2g	$⊢ O \in V \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}))))$

Metamath Proof Explorer

Theorem isome

Proof