0ome

Description: The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	0ome.1	$⊢ φ \to X \in V$
	0ome.2	$⊢ O = (x \in 𝒫 X ⟼ 0)$
Assertion	0ome	$⊢ φ \to O \in OutMeas$

Proof

Step	Hyp	Ref	Expression
1		0ome.1	$⊢ φ \to X \in V$
2		0ome.2	$⊢ O = (x \in 𝒫 X ⟼ 0)$
3		eqid	$⊢ (y \in 𝒫 X ⟼ 0) = (y \in 𝒫 X ⟼ 0)$
4		0e0iccpnf	$⊢ 0 \in [0, +∞]$
5	4	a1i	$⊢ y \in 𝒫 X \to 0 \in [0, +∞]$
6	3 5	fmpti	$⊢ (y \in 𝒫 X ⟼ 0) : 𝒫 X ⟶ [0, +∞]$
7		eqidd	$⊢ x = y \to 0 = 0$
8	7	cbvmptv	$⊢ (x \in 𝒫 X ⟼ 0) = (y \in 𝒫 X ⟼ 0)$
9	2 8	eqtri	$⊢ O = (y \in 𝒫 X ⟼ 0)$
10	9	feq1i	$⊢ O : dom O ⟶ [0, +∞] \leftrightarrow (y \in 𝒫 X ⟼ 0) : dom O ⟶ [0, +∞]$
11	9	dmeqi	$⊢ dom O = dom (y \in 𝒫 X ⟼ 0)$
12		0re	$⊢ 0 \in ℝ$
13	12	rgenw	$⊢ \forall y \in 𝒫 X 0 \in ℝ$
14		dmmptg	$⊢ \forall y \in 𝒫 X 0 \in ℝ \to dom (y \in 𝒫 X ⟼ 0) = 𝒫 X$
15	13 14	ax-mp	$⊢ dom (y \in 𝒫 X ⟼ 0) = 𝒫 X$
16	11 15	eqtri	$⊢ dom O = 𝒫 X$
17	16	feq2i	$⊢ (y \in 𝒫 X ⟼ 0) : dom O ⟶ [0, +∞] \leftrightarrow (y \in 𝒫 X ⟼ 0) : 𝒫 X ⟶ [0, +∞]$
18	10 17	bitri	$⊢ O : dom O ⟶ [0, +∞] \leftrightarrow (y \in 𝒫 X ⟼ 0) : 𝒫 X ⟶ [0, +∞]$
19	6 18	mpbir	$⊢ O : dom O ⟶ [0, +∞]$
20		unipw	$⊢ ⋃ 𝒫 X = X$
21	20	pweqi	$⊢ 𝒫 ⋃ 𝒫 X = 𝒫 X$
22	21	eqcomi	$⊢ 𝒫 X = 𝒫 ⋃ 𝒫 X$
23	16	eqcomi	$⊢ 𝒫 X = dom O$
24	23	unieqi	$⊢ ⋃ 𝒫 X = ⋃ dom O$
25	24	pweqi	$⊢ 𝒫 ⋃ 𝒫 X = 𝒫 ⋃ dom O$
26	16 22 25	3eqtri	$⊢ dom O = 𝒫 ⋃ dom O$
27	19 26	pm3.2i	$⊢ (O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O)$
28		0elpw	$⊢ \emptyset \in 𝒫 X$
29		eqidd	$⊢ y = \emptyset \to 0 = 0$
30	12	elexi	$⊢ 0 \in V$
31	29 9 30	fvmpt	$⊢ \emptyset \in 𝒫 X \to O (\emptyset) = 0$
32	28 31	ax-mp	$⊢ O (\emptyset) = 0$
33	27 32	pm3.2i	$⊢ ((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0)$
34	12	leidi	$⊢ 0 \leq 0$
35	34	a1i	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to 0 \leq 0$
36		eqidd	$⊢ y = z \to 0 = 0$
37		elpwi	$⊢ z \in 𝒫 y \to z \subseteq y$
38	37	adantl	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to z \subseteq y$
39		id	$⊢ y \in 𝒫 ⋃ dom O \to y \in 𝒫 ⋃ dom O$
40	22 25	eqtr2i	$⊢ 𝒫 ⋃ dom O = 𝒫 X$
41	40	a1i	$⊢ y \in 𝒫 ⋃ dom O \to 𝒫 ⋃ dom O = 𝒫 X$
42	39 41	eleqtrd	$⊢ y \in 𝒫 ⋃ dom O \to y \in 𝒫 X$
43		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
44	42 43	syl	$⊢ y \in 𝒫 ⋃ dom O \to y \subseteq X$
45	44	adantr	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to y \subseteq X$
46	38 45	sstrd	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to z \subseteq X$
47		simpr	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to z \in 𝒫 y$
48		elpwg	$⊢ z \in 𝒫 y \to (z \in 𝒫 X \leftrightarrow z \subseteq X)$
49	47 48	syl	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to (z \in 𝒫 X \leftrightarrow z \subseteq X)$
50	46 49	mpbird	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to z \in 𝒫 X$
51	12	a1i	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to 0 \in ℝ$
52	9 36 50 51	fvmptd3	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to O (z) = 0$
53	9	fvmpt2	$⊢ (y \in 𝒫 X \land 0 \in ℝ) \to O (y) = 0$
54	42 12 53	sylancl	$⊢ y \in 𝒫 ⋃ dom O \to O (y) = 0$
55	54	adantr	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to O (y) = 0$
56	52 55	breq12d	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to (O (z) \leq O (y) \leftrightarrow 0 \leq 0)$
57	35 56	mpbird	$⊢ (y \in 𝒫 ⋃ dom O \land z \in 𝒫 y) \to O (z) \leq O (y)$
58	57	ralrimiva	$⊢ y \in 𝒫 ⋃ dom O \to \forall z \in 𝒫 y O (z) \leq O (y)$
59	58	rgen	$⊢ \forall y \in 𝒫 ⋃ dom O \forall z \in 𝒫 y O (z) \leq O (y)$
60	33 59	pm3.2i	$⊢ (((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))$
61	34	a1i	$⊢ y \in 𝒫 dom O \to 0 \leq 0$
62	36	cbvmptv	$⊢ (y \in 𝒫 X ⟼ 0) = (z \in 𝒫 X ⟼ 0)$
63	9 62	eqtri	$⊢ O = (z \in 𝒫 X ⟼ 0)$
64	63	a1i	$⊢ y \in 𝒫 dom O \to O = (z \in 𝒫 X ⟼ 0)$
65		eqidd	$⊢ (y \in 𝒫 dom O \land z = ⋃ y) \to 0 = 0$
66		id	$⊢ y \in 𝒫 dom O \to y \in 𝒫 dom O$
67	16	pweqi	$⊢ 𝒫 dom O = 𝒫 𝒫 X$
68	67	a1i	$⊢ y \in 𝒫 dom O \to 𝒫 dom O = 𝒫 𝒫 X$
69	66 68	eleqtrd	$⊢ y \in 𝒫 dom O \to y \in 𝒫 𝒫 X$
70		elpwi	$⊢ y \in 𝒫 𝒫 X \to y \subseteq 𝒫 X$
71	69 70	syl	$⊢ y \in 𝒫 dom O \to y \subseteq 𝒫 X$
72		sspwuni	$⊢ y \subseteq 𝒫 X \leftrightarrow ⋃ y \subseteq X$
73	71 72	sylib	$⊢ y \in 𝒫 dom O \to ⋃ y \subseteq X$
74		vuniex	$⊢ ⋃ y \in V$
75	74	a1i	$⊢ y \in 𝒫 dom O \to ⋃ y \in V$
76		elpwg	$⊢ ⋃ y \in V \to (⋃ y \in 𝒫 X \leftrightarrow ⋃ y \subseteq X)$
77	75 76	syl	$⊢ y \in 𝒫 dom O \to (⋃ y \in 𝒫 X \leftrightarrow ⋃ y \subseteq X)$
78	73 77	mpbird	$⊢ y \in 𝒫 dom O \to ⋃ y \in 𝒫 X$
79	12	a1i	$⊢ y \in 𝒫 dom O \to 0 \in ℝ$
80	64 65 78 79	fvmptd	$⊢ y \in 𝒫 dom O \to O (⋃ y) = 0$
81	64	reseq1d	$⊢ y \in 𝒫 dom O \to {O ↾}_{y} = {(z \in 𝒫 X ⟼ 0) ↾}_{y}$
82		resmpt	$⊢ y \subseteq 𝒫 X \to {(z \in 𝒫 X ⟼ 0) ↾}_{y} = (z \in y ⟼ 0)$
83	71 82	syl	$⊢ y \in 𝒫 dom O \to {(z \in 𝒫 X ⟼ 0) ↾}_{y} = (z \in y ⟼ 0)$
84	81 83	eqtrd	$⊢ y \in 𝒫 dom O \to {O ↾}_{y} = (z \in y ⟼ 0)$
85	84	fveq2d	$⊢ y \in 𝒫 dom O \to sum^({O ↾}_{y}) = sum^((z \in y ⟼ 0))$
86		nfv	$⊢ Ⅎ z y \in 𝒫 dom O$
87	86 66	sge0z	$⊢ y \in 𝒫 dom O \to sum^((z \in y ⟼ 0)) = 0$
88	85 87	eqtrd	$⊢ y \in 𝒫 dom O \to sum^({O ↾}_{y}) = 0$
89	80 88	breq12d	$⊢ y \in 𝒫 dom O \to (O (⋃ y) \leq sum^({O ↾}_{y}) \leftrightarrow 0 \leq 0)$
90	61 89	mpbird	$⊢ y \in 𝒫 dom O \to O (⋃ y) \leq sum^({O ↾}_{y})$
91	90	a1d	$⊢ y \in 𝒫 dom O \to (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y}))$
92	91	rgen	$⊢ \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y}))$
93	60 92	pm3.2i	$⊢ ((((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})))$
94	93	a1i	$⊢ φ \to ((((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})))$
95	9	a1i	$⊢ φ \to O = (y \in 𝒫 X ⟼ 0)$
96	1	pwexd	$⊢ φ \to 𝒫 X \in V$
97		mptexg	$⊢ 𝒫 X \in V \to (y \in 𝒫 X ⟼ 0) \in V$
98	96 97	syl	$⊢ φ \to (y \in 𝒫 X ⟼ 0) \in V$
99	95 98	eqeltrd	$⊢ φ \to O \in V$
100		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}))))$
101	99 100	syl	$⊢ φ \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}))))$
102	94 101	mpbird	$⊢ φ \to O \in OutMeas$

Metamath Proof Explorer

Theorem 0ome

Proof