omsf

Description: A constructed outer measure is a function. (Contributed by Thierry Arnoux, 17-Sep-2019) (Revised by AV, 4-Oct-2020)

		Ref	Expression
	Assertion	omsf	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
2		xrltso	$⊢ < Or ℝ^{*}$
3		soss	$⊢ [0, +∞] \subseteq ℝ^{} \to (< Or ℝ^{} \to < Or [0, +∞])$
4	1 2 3	mp2	$⊢ < Or [0, +∞]$
5	4	a1i	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to < Or [0, +∞]$
6		omscl	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land a \in 𝒫 ⋃ dom R) \to ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) \subseteq [0, +∞]$
7	6	3expa	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) \subseteq [0, +∞]$
8		xrge0infss	$⊢ ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \subseteq [0, +∞] \to \exists t \in [0, +∞] (\forall w \in ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \neg w < t \land \forall w \in [0, +∞] (t < w \to \exists s \in ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) s < w))$
9	7 8	syl	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to \exists t \in [0, +∞] (\forall w \in ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \neg w < t \land \forall w \in [0, +∞] (t < w \to \exists s \in ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) s < w))$
10	5 9	infcl	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to inf (ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <) \in [0, +∞]$
11		fex	$⊢ (R : Q ⟶ [0, +∞] \land Q \in V) \to R \in V$
12	11	ancoms	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to R \in V$
13		omsval	$⊢ R \in V \to toOMeas (R) = (a \in 𝒫 ⋃ dom R ⟼ inf (ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <))$
14	12 13	syl	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to toOMeas (R) = (a \in 𝒫 ⋃ dom R ⟼ inf (ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <))$
15		simpll	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to Q \in V$
16		simplr	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to R : Q ⟶ [0, +∞]$
17		simpr	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to a \in 𝒫 ⋃ dom R$
18		fdm	$⊢ R : Q ⟶ [0, +∞] \to dom R = Q$
19	18	unieqd	$⊢ R : Q ⟶ [0, +∞] \to ⋃ dom R = ⋃ Q$
20	19	pweqd	$⊢ R : Q ⟶ [0, +∞] \to 𝒫 ⋃ dom R = 𝒫 ⋃ Q$
21	20	ad2antlr	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to 𝒫 ⋃ dom R = 𝒫 ⋃ Q$
22	17 21	eleqtrd	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to a \in 𝒫 ⋃ Q$
23		elpwi	$⊢ a \in 𝒫 ⋃ Q \to a \subseteq ⋃ Q$
24	22 23	syl	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to a \subseteq ⋃ Q$
25		omsfval	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land a \subseteq ⋃ Q) \to toOMeas (R) (a) = inf (ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <)$
26	15 16 24 25	syl3anc	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to toOMeas (R) (a) = inf (ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <)$
27	26 10	eqeltrd	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞]) \land a \in 𝒫 ⋃ dom R) \to toOMeas (R) (a) \in [0, +∞]$
28	10 14 27	fmpt2d	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$

Metamath Proof Explorer

Theorem omsf

Proof