Definition df-ome 39380

Description: Define the class of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Assertion

Ref	Expression
df-ome	⊢ OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦))))}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ome

Step	Hyp	Ref	Expression
1		come 39379	. 2 class OutMeas
2		vx	. . . . . . . . . 10 setvar 𝑥
3	2	cv 1474	. . . . . . . . 9 class 𝑥
4	3	cdm 5038	. . . . . . . 8 class dom 𝑥
5		cc0 9815	. . . . . . . . 9 class 0
6		cpnf 9950	. . . . . . . . 9 class +∞
7		cicc 12049	. . . . . . . . 9 class [,]
8	5, 6, 7	co 6549	. . . . . . . 8 class (0[,]+∞)
9	4, 8, 3	wf 5800	. . . . . . 7 wff 𝑥:dom 𝑥⟶(0[,]+∞)
10	4	cuni 4372	. . . . . . . . 9 class ∪ dom 𝑥
11	10	cpw 4108	. . . . . . . 8 class 𝒫 ∪ dom 𝑥
12	4, 11	wceq 1475	. . . . . . 7 wff dom 𝑥 = 𝒫 ∪ dom 𝑥
13	9, 12	wa 383	. . . . . 6 wff (𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥)
14		c0 3874	. . . . . . . 8 class ∅
15	14, 3	cfv 5804	. . . . . . 7 class (𝑥‘∅)
16	15, 5	wceq 1475	. . . . . 6 wff (𝑥‘∅) = 0
17	13, 16	wa 383	. . . . 5 wff ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0)
18		vz	. . . . . . . . . 10 setvar 𝑧
19	18	cv 1474	. . . . . . . . 9 class 𝑧
20	19, 3	cfv 5804	. . . . . . . 8 class (𝑥‘𝑧)
21		vy	. . . . . . . . . 10 setvar 𝑦
22	21	cv 1474	. . . . . . . . 9 class 𝑦
23	22, 3	cfv 5804	. . . . . . . 8 class (𝑥‘𝑦)
24		cle 9954	. . . . . . . 8 class ≤
25	20, 23, 24	wbr 4583	. . . . . . 7 wff (𝑥‘𝑧) ≤ (𝑥‘𝑦)
26	22	cpw 4108	. . . . . . 7 class 𝒫 𝑦
27	25, 18, 26	wral 2896	. . . . . 6 wff ∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)
28	27, 21, 11	wral 2896	. . . . 5 wff ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)
29	17, 28	wa 383	. . . 4 wff (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦))
30		com 6957	. . . . . . 7 class ω
31		cdom 7839	. . . . . . 7 class ≼
32	22, 30, 31	wbr 4583	. . . . . 6 wff 𝑦 ≼ ω
33	22	cuni 4372	. . . . . . . 8 class ∪ 𝑦
34	33, 3	cfv 5804	. . . . . . 7 class (𝑥‘∪ 𝑦)
35	3, 22	cres 5040	. . . . . . . 8 class (𝑥 ↾ 𝑦)
36		csumge0 39255	. . . . . . . 8 class Σ^
37	35, 36	cfv 5804	. . . . . . 7 class (Σ^‘(𝑥 ↾ 𝑦))
38	34, 37, 24	wbr 4583	. . . . . 6 wff (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦))
39	32, 38	wi 4	. . . . 5 wff (𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦)))
40	4	cpw 4108	. . . . 5 class 𝒫 dom 𝑥
41	39, 21, 40	wral 2896	. . . 4 wff ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦)))
42	29, 41	wa 383	. . 3 wff ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦))))
43	42, 2	cab 2596	. 2 class {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦))))}
44	1, 43	wceq 1475	1 wff OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦))))}

This definition is referenced by:  isome  39384