omscl

Description: A closure lemma for the constructed outer measure. (Contributed by Thierry Arnoux, 17-Sep-2019)

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

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		simp2	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \to R : Q ⟶ [0, +∞]$
3	2	ad2antrr	$⊢ (((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to R : Q ⟶ [0, +∞]$
4		ssrab2	$⊢ \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \subseteq 𝒫 dom R$
5		simpr	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \to x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}$
6	4 5	sselid	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \to x \in 𝒫 dom R$
7		fdm	$⊢ R : Q ⟶ [0, +∞] \to dom R = Q$
8	7	pweqd	$⊢ R : Q ⟶ [0, +∞] \to 𝒫 dom R = 𝒫 Q$
9	2 8	syl	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \to 𝒫 dom R = 𝒫 Q$
10	9	adantr	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \to 𝒫 dom R = 𝒫 Q$
11	6 10	eleqtrd	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \to x \in 𝒫 Q$
12		elpwi	$⊢ x \in 𝒫 Q \to x \subseteq Q$
13	11 12	syl	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \to x \subseteq Q$
14	13	sselda	$⊢ (((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to y \in Q$
15	3 14	ffvelcdmd	$⊢ (((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \land y \in x) \to R (y) \in [0, +∞]$
16	15	ralrimiva	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \to \forall y \in x R (y) \in [0, +∞]$
17		nfcv	$⊢ \underline{Ⅎ} y x$
18	17	esumcl	$⊢ (x \in V \land \forall y \in x R (y) \in [0, +∞]) \to \underset{y \in x}{\sum^{*}} R (y) \in [0, +∞]$
19	1 16 18	sylancr	$⊢ ((Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \land x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\}) \to \underset{y \in x}{\sum^{*}} R (y) \in [0, +∞]$
20	19	ralrimiva	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \to \forall x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{y \in x}{\sum^{*}} R (y) \in [0, +∞]$
21		eqid	$⊢ (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))$
22	21	rnmptss	$⊢ \forall x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{y \in x}{\sum^{}} R (y) \in [0, +∞] \to ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \subseteq [0, +∞]$
23	20 22	syl	$⊢ (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, +∞]$

Metamath Proof Explorer

Theorem omscl

Proof