omsval

Description: Value of the function mapping a content function to the corresponding outer measure. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

		Ref	Expression
	Assertion	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, +∞] <))$

Proof

Step	Hyp	Ref	Expression
1		df-oms	$⊢ toOMeas = (r \in V ⟼ (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, +∞] <)))$
2		dmeq	$⊢ r = R \to dom r = dom R$
3	2	unieqd	$⊢ r = R \to ⋃ dom r = ⋃ dom R$
4	3	pweqd	$⊢ r = R \to 𝒫 ⋃ dom r = 𝒫 ⋃ dom R$
5	2	pweqd	$⊢ r = R \to 𝒫 dom r = 𝒫 dom R$
6		rabeq	$⊢ 𝒫 dom r = 𝒫 dom R \to \{z \in 𝒫 dom r \| (a \subseteq ⋃ z \land z ≼ ω)\} = \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\}$
7	5 6	syl	$⊢ r = R \to \{z \in 𝒫 dom r \| (a \subseteq ⋃ z \land z ≼ ω)\} = \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\}$
8		simpl	$⊢ (r = R \land y \in x) \to r = R$
9	8	fveq1d	$⊢ (r = R \land y \in x) \to r (y) = R (y)$
10	9	esumeq2dv	$⊢ r = R \to \underset{y \in x}{\sum^{}} r (y) = \underset{y \in x}{\sum^{}} R (y)$
11	7 10	mpteq12dv	$⊢ r = R \to (x \in \{z \in 𝒫 dom r \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} r (y)) = (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
12	11	rneqd	$⊢ r = R \to ran (x \in \{z \in 𝒫 dom r \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} r (y)) = ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
13	12	infeq1d	$⊢ r = R \to inf (ran (x \in \{z \in 𝒫 dom r \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} r (y)) [0, +∞] <) = inf (ran (x \in \{z \in 𝒫 dom R \| (a \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) [0, +∞] <)$
14	4 13	mpteq12dv	$⊢ r = R \to (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, +∞] <)) = (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		id	$⊢ R \in V \to R \in V$
16		dmexg	$⊢ R \in V \to dom R \in V$
17		uniexg	$⊢ dom R \in V \to ⋃ dom R \in V$
18		pwexg	$⊢ ⋃ dom R \in V \to 𝒫 ⋃ dom R \in V$
19		mptexg	$⊢ 𝒫 ⋃ dom R \in V \to (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, +∞] <)) \in V$
20	16 17 18 19	4syl	$⊢ R \in V \to (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, +∞] <)) \in V$
21	1 14 15 20	fvmptd3	$⊢ 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, +∞] <))$

Metamath Proof Explorer

Theorem omsval

Proof