Metamath Proof Explorer

Definition df-ome

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 come ⊢ OutMeas
1 vx ⊢ 𝑥
2 1 cv ⊢ 𝑥
3 2 cdm ⊢ dom 𝑥
4 cc0 ⊢ 0
5 cicc ⊢ [,]
6 cpnf ⊢ +∞
7 4 6 5 co ⊢ ( 0 [,] +∞ )
8 3 7 2 wf ⊢ 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ )
9 3 cuni ⊢ ∪ dom 𝑥
10 9 cpw ⊢ 𝒫 ∪ dom 𝑥
11 3 10 wceq ⊢ dom 𝑥 = 𝒫 ∪ dom 𝑥
12 8 11 wa ⊢ ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 )
13 c0 ⊢ ∅
14 13 2 cfv ⊢ ( 𝑥 ‘ ∅ )
15 14 4 wceq ⊢ ( 𝑥 ‘ ∅ ) = 0
16 12 15 wa ⊢ ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ∧ ( 𝑥 ‘ ∅ ) = 0 )
17 vy ⊢ 𝑦
18 vz ⊢ 𝑧
19 17 cv ⊢ 𝑦
20 19 cpw ⊢ 𝒫 𝑦
21 18 cv ⊢ 𝑧
22 21 2 cfv ⊢ ( 𝑥 ‘ 𝑧 )
23 cle ⊢ ≤
24 19 2 cfv ⊢ ( 𝑥 ‘ 𝑦 )
25 22 24 23 wbr ⊢ ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 )
26 25 18 20 wral ⊢ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 )
27 26 17 10 wral ⊢ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑥 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 )
28 16 27 wa ⊢ ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑥 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) )
29 3 cpw ⊢ 𝒫 dom 𝑥
30 cdom ⊢ ≼
31 com ⊢ ω
32 19 31 30 wbr ⊢ 𝑦 ≼ ω
33 19 cuni ⊢ ∪ 𝑦
34 33 2 cfv ⊢ ( 𝑥 ‘ ∪ 𝑦 )
35 csumge0 ⊢ Σ^
36 2 19 cres ⊢ ( 𝑥 ↾ 𝑦 )
37 36 35 cfv ⊢ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) )
38 34 37 23 wbr ⊢ ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) )
39 32 38 wi ⊢ ( 𝑦 ≼ ω → ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) )
40 39 17 29 wral ⊢ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≼ ω → ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) )
41 28 40 wa ⊢ ( ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑥 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≼ ω → ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) )
42 41 1 cab ⊢ { 𝑥 ∣ ( ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑥 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≼ ω → ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) ) }
43 0 42 wceq ⊢ OutMeas = { 𝑥 ∣ ( ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥 ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑥 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑥 ‘ 𝑧 ) ≤ ( 𝑥 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≼ ω → ( 𝑥 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) ) }