isomennd

Description: Sufficient condition to prove that O is an outer measure. Definition 113A of Fremlin1 p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	isomennd.x	$⊢ φ \to X \in V$
	isomennd.o	$⊢ φ \to O : 𝒫 X ⟶ [0, +∞]$
	isomennd.o0	$⊢ φ \to O (\emptyset) = 0$
	isomennd.le	$⊢ (φ \land x \subseteq X \land y \subseteq x) \to O (y) \leq O (x)$
	isomennd.sa	$⊢ (φ \land a : ℕ ⟶ 𝒫 X) \to O (⋃_{n \in ℕ} a (n)) \leq sum^((n \in ℕ ⟼ O (a (n))))$
Assertion	isomennd	$⊢ φ \to O \in OutMeas$

Proof

Step	Hyp	Ref	Expression
1		isomennd.x	$⊢ φ \to X \in V$
2		isomennd.o	$⊢ φ \to O : 𝒫 X ⟶ [0, +∞]$
3		isomennd.o0	$⊢ φ \to O (\emptyset) = 0$
4		isomennd.le	$⊢ (φ \land x \subseteq X \land y \subseteq x) \to O (y) \leq O (x)$
5		isomennd.sa	$⊢ (φ \land a : ℕ ⟶ 𝒫 X) \to O (⋃_{n \in ℕ} a (n)) \leq sum^((n \in ℕ ⟼ O (a (n))))$
6		id	$⊢ O : 𝒫 X ⟶ [0, +∞] \to O : 𝒫 X ⟶ [0, +∞]$
7		fdm	$⊢ O : 𝒫 X ⟶ [0, +∞] \to dom O = 𝒫 X$
8	7	feq2d	$⊢ O : 𝒫 X ⟶ [0, +∞] \to (O : dom O ⟶ [0, +∞] \leftrightarrow O : 𝒫 X ⟶ [0, +∞])$
9	6 8	mpbird	$⊢ O : 𝒫 X ⟶ [0, +∞] \to O : dom O ⟶ [0, +∞]$
10	2 9	syl	$⊢ φ \to O : dom O ⟶ [0, +∞]$
11		unipw	$⊢ ⋃ 𝒫 X = X$
12	11	pweqi	$⊢ 𝒫 ⋃ 𝒫 X = 𝒫 X$
13	12	a1i	$⊢ φ \to 𝒫 ⋃ 𝒫 X = 𝒫 X$
14	2 7	syl	$⊢ φ \to dom O = 𝒫 X$
15	14	unieqd	$⊢ φ \to ⋃ dom O = ⋃ 𝒫 X$
16	15	pweqd	$⊢ φ \to 𝒫 ⋃ dom O = 𝒫 ⋃ 𝒫 X$
17	13 16 14	3eqtr4rd	$⊢ φ \to dom O = 𝒫 ⋃ dom O$
18	10 17 3	jca31	$⊢ φ \to ((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0)$
19		simpl	$⊢ (φ \land (x \in 𝒫 ⋃ dom O \land y \in 𝒫 x)) \to φ$
20		simpr	$⊢ (φ \land x \in 𝒫 ⋃ dom O) \to x \in 𝒫 ⋃ dom O$
21	16 13	eqtrd	$⊢ φ \to 𝒫 ⋃ dom O = 𝒫 X$
22	21	adantr	$⊢ (φ \land x \in 𝒫 ⋃ dom O) \to 𝒫 ⋃ dom O = 𝒫 X$
23	20 22	eleqtrd	$⊢ (φ \land x \in 𝒫 ⋃ dom O) \to x \in 𝒫 X$
24		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
25	23 24	syl	$⊢ (φ \land x \in 𝒫 ⋃ dom O) \to x \subseteq X$
26	25	adantrr	$⊢ (φ \land (x \in 𝒫 ⋃ dom O \land y \in 𝒫 x)) \to x \subseteq X$
27		elpwi	$⊢ y \in 𝒫 x \to y \subseteq x$
28	27	adantl	$⊢ (x \in 𝒫 ⋃ dom O \land y \in 𝒫 x) \to y \subseteq x$
29	28	adantl	$⊢ (φ \land (x \in 𝒫 ⋃ dom O \land y \in 𝒫 x)) \to y \subseteq x$
30	19 26 29 4	syl3anc	$⊢ (φ \land (x \in 𝒫 ⋃ dom O \land y \in 𝒫 x)) \to O (y) \leq O (x)$
31	30	ralrimivva	$⊢ φ \to \forall x \in 𝒫 ⋃ dom O \forall y \in 𝒫 x O (y) \leq O (x)$
32		0le0	$⊢ 0 \leq 0$
33	32	a1i	$⊢ (φ \land x = \emptyset) \to 0 \leq 0$
34		unieq	$⊢ x = \emptyset \to ⋃ x = ⋃ \emptyset$
35		uni0	$⊢ ⋃ \emptyset = \emptyset$
36	35	a1i	$⊢ x = \emptyset \to ⋃ \emptyset = \emptyset$
37	34 36	eqtrd	$⊢ x = \emptyset \to ⋃ x = \emptyset$
38	37	fveq2d	$⊢ x = \emptyset \to O (⋃ x) = O (\emptyset)$
39	38	adantl	$⊢ (φ \land x = \emptyset) \to O (⋃ x) = O (\emptyset)$
40	3	adantr	$⊢ (φ \land x = \emptyset) \to O (\emptyset) = 0$
41	39 40	eqtrd	$⊢ (φ \land x = \emptyset) \to O (⋃ x) = 0$
42		reseq2	$⊢ x = \emptyset \to {O ↾}_{x} = {O ↾}_{\emptyset}$
43		res0	$⊢ {O ↾}_{\emptyset} = \emptyset$
44	43	a1i	$⊢ x = \emptyset \to {O ↾}_{\emptyset} = \emptyset$
45	42 44	eqtrd	$⊢ x = \emptyset \to {O ↾}_{x} = \emptyset$
46	45	fveq2d	$⊢ x = \emptyset \to sum^({O ↾}_{x}) = sum^(\emptyset)$
47		sge00	$⊢ sum^(\emptyset) = 0$
48	47	a1i	$⊢ x = \emptyset \to sum^(\emptyset) = 0$
49	46 48	eqtrd	$⊢ x = \emptyset \to sum^({O ↾}_{x}) = 0$
50	49	adantl	$⊢ (φ \land x = \emptyset) \to sum^({O ↾}_{x}) = 0$
51	41 50	breq12d	$⊢ (φ \land x = \emptyset) \to (O (⋃ x) \leq sum^({O ↾}_{x}) \leftrightarrow 0 \leq 0)$
52	33 51	mpbird	$⊢ (φ \land x = \emptyset) \to O (⋃ x) \leq sum^({O ↾}_{x})$
53	52	ad4ant14	$⊢ (((φ \land x \in 𝒫 dom O) \land x ≼ ω) \land x = \emptyset) \to O (⋃ x) \leq sum^({O ↾}_{x})$
54		simpl	$⊢ (((φ \land x \in 𝒫 dom O) \land x ≼ ω) \land \neg x = \emptyset) \to ((φ \land x \in 𝒫 dom O) \land x ≼ ω)$
55		neqne	$⊢ \neg x = \emptyset \to x \neq \emptyset$
56	55	adantl	$⊢ (((φ \land x \in 𝒫 dom O) \land x ≼ ω) \land \neg x = \emptyset) \to x \neq \emptyset$
57		ssnnf1octb	$⊢ (x ≼ ω \land x \neq \emptyset) \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x)$
58	57	adantll	$⊢ (((φ \land x \in 𝒫 dom O) \land x ≼ ω) \land x \neq \emptyset) \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x)$
59	2	ad2antrr	$⊢ ((φ \land x \in 𝒫 dom O) \land (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x)) \to O : 𝒫 X ⟶ [0, +∞]$
60	3	ad2antrr	$⊢ ((φ \land x \in 𝒫 dom O) \land (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x)) \to O (\emptyset) = 0$
61		simpr	$⊢ (φ \land x \in 𝒫 dom O) \to x \in 𝒫 dom O$
62	14	pweqd	$⊢ φ \to 𝒫 dom O = 𝒫 𝒫 X$
63	62	adantr	$⊢ (φ \land x \in 𝒫 dom O) \to 𝒫 dom O = 𝒫 𝒫 X$
64	61 63	eleqtrd	$⊢ (φ \land x \in 𝒫 dom O) \to x \in 𝒫 𝒫 X$
65		elpwi	$⊢ x \in 𝒫 𝒫 X \to x \subseteq 𝒫 X$
66	64 65	syl	$⊢ (φ \land x \in 𝒫 dom O) \to x \subseteq 𝒫 X$
67	66	adantr	$⊢ ((φ \land x \in 𝒫 dom O) \land (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x)) \to x \subseteq 𝒫 X$
68		simpl	$⊢ (φ \land x \in 𝒫 dom O) \to φ$
69	68 5	sylan	$⊢ ((φ \land x \in 𝒫 dom O) \land a : ℕ ⟶ 𝒫 X) \to O (⋃_{n \in ℕ} a (n)) \leq sum^((n \in ℕ ⟼ O (a (n))))$
70	69	adantlr	$⊢ (((φ \land x \in 𝒫 dom O) \land (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x)) \land a : ℕ ⟶ 𝒫 X) \to O (⋃_{n \in ℕ} a (n)) \leq sum^((n \in ℕ ⟼ O (a (n))))$
71		simprl	$⊢ ((φ \land x \in 𝒫 dom O) \land (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x)) \to dom f \subseteq ℕ$
72		simprr	$⊢ ((φ \land x \in 𝒫 dom O) \land (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x)) \to f : dom f \underset{1-1 onto}{⟶} x$
73		eleq1w	$⊢ m = n \to (m \in dom f \leftrightarrow n \in dom f)$
74		fveq2	$⊢ m = n \to f (m) = f (n)$
75	73 74	ifbieq1d	$⊢ m = n \to if (m \in dom f, f (m), \emptyset) = if (n \in dom f, f (n), \emptyset)$
76	75	cbvmptv	$⊢ (m \in ℕ ⟼ if (m \in dom f, f (m), \emptyset)) = (n \in ℕ ⟼ if (n \in dom f, f (n), \emptyset))$
77	59 60 67 70 71 72 76	isomenndlem	$⊢ ((φ \land x \in 𝒫 dom O) \land (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x)) \to O (⋃ x) \leq sum^({O ↾}_{x})$
78	77	ex	$⊢ (φ \land x \in 𝒫 dom O) \to ((dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x) \to O (⋃ x) \leq sum^({O ↾}_{x}))$
79	78	ad2antrr	$⊢ (((φ \land x \in 𝒫 dom O) \land x ≼ ω) \land x \neq \emptyset) \to ((dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x) \to O (⋃ x) \leq sum^({O ↾}_{x}))$
80	79	exlimdv	$⊢ (((φ \land x \in 𝒫 dom O) \land x ≼ ω) \land x \neq \emptyset) \to (\exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} x) \to O (⋃ x) \leq sum^({O ↾}_{x}))$
81	58 80	mpd	$⊢ (((φ \land x \in 𝒫 dom O) \land x ≼ ω) \land x \neq \emptyset) \to O (⋃ x) \leq sum^({O ↾}_{x})$
82	54 56 81	syl2anc	$⊢ (((φ \land x \in 𝒫 dom O) \land x ≼ ω) \land \neg x = \emptyset) \to O (⋃ x) \leq sum^({O ↾}_{x})$
83	53 82	pm2.61dan	$⊢ ((φ \land x \in 𝒫 dom O) \land x ≼ ω) \to O (⋃ x) \leq sum^({O ↾}_{x})$
84	83	ex	$⊢ (φ \land x \in 𝒫 dom O) \to (x ≼ ω \to O (⋃ x) \leq sum^({O ↾}_{x}))$
85	84	ralrimiva	$⊢ φ \to \forall x \in 𝒫 dom O (x ≼ ω \to O (⋃ x) \leq sum^({O ↾}_{x}))$
86	18 31 85	jca31	$⊢ φ \to ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall x \in 𝒫 ⋃ dom O \forall y \in 𝒫 x O (y) \leq O (x)) \land \forall x \in 𝒫 dom O (x ≼ ω \to O (⋃ x) \leq sum^({O ↾}_{x})))$
87	1	pwexd	$⊢ φ \to 𝒫 X \in V$
88		fex	$⊢ (O : 𝒫 X ⟶ [0, +∞] \land 𝒫 X \in V) \to O \in V$
89	2 87 88	syl2anc	$⊢ φ \to O \in V$
90		isome	$⊢ O \in V \to (O \in OutMeas \leftrightarrow ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall x \in 𝒫 ⋃ dom O \forall y \in 𝒫 x O (y) \leq O (x)) \land \forall x \in 𝒫 dom O (x ≼ ω \to O (⋃ x) \leq sum^({O ↾}_{x}))))$
91	89 90	syl	$⊢ φ \to (O \in OutMeas \leftrightarrow ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall x \in 𝒫 ⋃ dom O \forall y \in 𝒫 x O (y) \leq O (x)) \land \forall x \in 𝒫 dom O (x ≼ ω \to O (⋃ x) \leq sum^({O ↾}_{x}))))$
92	86 91	mpbird	$⊢ φ \to O \in OutMeas$

Metamath Proof Explorer

Theorem isomennd

Proof