Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
0ome.2 ⊢ 𝑂 = ( 𝑥 ∈ 𝒫 𝑋 ↦ 0 )
Assertion 0ome ( 𝜑 → 𝑂 ∈ OutMeas )

Proof

Step Hyp Ref Expression
1 0ome.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 0ome.2 ⊢ 𝑂 = ( 𝑥 ∈ 𝒫 𝑋 ↦ 0 )
3 eqid ⊢ ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) = ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 )
4 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
5 4 a1i ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 0 ∈ ( 0 [,] +∞ ) )
6 3 5 fmpti ⊢ ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) : 𝒫 𝑋 ⟶ ( 0 [,] +∞ )
7 eqidd ⊢ ( 𝑥 = 𝑦 → 0 = 0 )
8 7 cbvmptv ⊢ ( 𝑥 ∈ 𝒫 𝑋 ↦ 0 ) = ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 )
9 2 8 eqtri ⊢ 𝑂 = ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 )
10 9 feq1i ⊢ ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ↔ ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) : dom 𝑂 ⟶ ( 0 [,] +∞ ) )
11 9 dmeqi ⊢ dom 𝑂 = dom ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 )
12 0re ⊢ 0 ∈ ℝ
13 12 rgenw ⊢ ∀ 𝑦 ∈ 𝒫 𝑋 0 ∈ ℝ
14 dmmptg ⊢ ( ∀ 𝑦 ∈ 𝒫 𝑋 0 ∈ ℝ → dom ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) = 𝒫 𝑋 )
15 13 14 ax-mp ⊢ dom ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) = 𝒫 𝑋
16 11 15 eqtri ⊢ dom 𝑂 = 𝒫 𝑋
17 16 feq2i ⊢ ( ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) : dom 𝑂 ⟶ ( 0 [,] +∞ ) ↔ ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
18 10 17 bitri ⊢ ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ↔ ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
19 6 18 mpbir ⊢ 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ )
20 unipw ⊢ ∪ 𝒫 𝑋 = 𝑋
21 20 pweqi ⊢ 𝒫 ∪ 𝒫 𝑋 = 𝒫 𝑋
22 21 eqcomi ⊢ 𝒫 𝑋 = 𝒫 ∪ 𝒫 𝑋
23 16 eqcomi ⊢ 𝒫 𝑋 = dom 𝑂
24 23 unieqi ⊢ ∪ 𝒫 𝑋 = ∪ dom 𝑂
25 24 pweqi ⊢ 𝒫 ∪ 𝒫 𝑋 = 𝒫 ∪ dom 𝑂
26 16 22 25 3eqtri ⊢ dom 𝑂 = 𝒫 ∪ dom 𝑂
27 19 26 pm3.2i ⊢ ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 )
28 0elpw ⊢ ∅ ∈ 𝒫 𝑋
29 eqidd ⊢ ( 𝑦 = ∅ → 0 = 0 )
30 12 elexi ⊢ 0 ∈ V
31 29 9 30 fvmpt ⊢ ( ∅ ∈ 𝒫 𝑋 → ( 𝑂 ‘ ∅ ) = 0 )
32 28 31 ax-mp ⊢ ( 𝑂 ‘ ∅ ) = 0
33 27 32 pm3.2i ⊢ ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 )
34 12 leidi ⊢ 0 ≤ 0
35 34 a1i ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → 0 ≤ 0 )
36 eqidd ⊢ ( 𝑦 = 𝑧 → 0 = 0 )
37 elpwi ⊢ ( 𝑧 ∈ 𝒫 𝑦 → 𝑧 ⊆ 𝑦 )
38 37 adantl ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → 𝑧 ⊆ 𝑦 )
39 id ⊢ ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝑦 ∈ 𝒫 ∪ dom 𝑂 )
40 22 25 eqtr2i ⊢ 𝒫 ∪ dom 𝑂 = 𝒫 𝑋
41 40 a1i ⊢ ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋 )
42 39 41 eleqtrd ⊢ ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝑦 ∈ 𝒫 𝑋 )
43 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋 )
44 42 43 syl ⊢ ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝑦 ⊆ 𝑋 )
45 44 adantr ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → 𝑦 ⊆ 𝑋 )
46 38 45 sstrd ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → 𝑧 ⊆ 𝑋 )
47 simpr ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → 𝑧 ∈ 𝒫 𝑦 )
48 elpwg ⊢ ( 𝑧 ∈ 𝒫 𝑦 → ( 𝑧 ∈ 𝒫 𝑋 ↔ 𝑧 ⊆ 𝑋 ) )
49 47 48 syl ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → ( 𝑧 ∈ 𝒫 𝑋 ↔ 𝑧 ⊆ 𝑋 ) )
50 46 49 mpbird ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → 𝑧 ∈ 𝒫 𝑋 )
51 12 a1i ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → 0 ∈ ℝ )
52 9 36 50 51 fvmptd3 ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → ( 𝑂 ‘ 𝑧 ) = 0 )
53 9 fvmpt2 ⊢ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 0 ∈ ℝ ) → ( 𝑂 ‘ 𝑦 ) = 0 )
54 42 12 53 sylancl ⊢ ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 → ( 𝑂 ‘ 𝑦 ) = 0 )
55 54 adantr ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → ( 𝑂 ‘ 𝑦 ) = 0 )
56 52 55 breq12d ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → ( ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ↔ 0 ≤ 0 ) )
57 35 56 mpbird ⊢ ( ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦 ) → ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) )
58 57 ralrimiva ⊢ ( 𝑦 ∈ 𝒫 ∪ dom 𝑂 → ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) )
59 58 rgen ⊢ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 )
60 33 59 pm3.2i ⊢ ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) )
61 34 a1i ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → 0 ≤ 0 )
62 36 cbvmptv ⊢ ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) = ( 𝑧 ∈ 𝒫 𝑋 ↦ 0 )
63 9 62 eqtri ⊢ 𝑂 = ( 𝑧 ∈ 𝒫 𝑋 ↦ 0 )
64 63 a1i ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → 𝑂 = ( 𝑧 ∈ 𝒫 𝑋 ↦ 0 ) )
65 eqidd ⊢ ( ( 𝑦 ∈ 𝒫 dom 𝑂 ∧ 𝑧 = ∪ 𝑦 ) → 0 = 0 )
66 id ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → 𝑦 ∈ 𝒫 dom 𝑂 )
67 16 pweqi ⊢ 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋
68 67 a1i ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋 )
69 66 68 eleqtrd ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → 𝑦 ∈ 𝒫 𝒫 𝑋 )
70 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝒫 𝑋 → 𝑦 ⊆ 𝒫 𝑋 )
71 69 70 syl ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → 𝑦 ⊆ 𝒫 𝑋 )
72 sspwuni ⊢ ( 𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋 )
73 71 72 sylib ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ∪ 𝑦 ⊆ 𝑋 )
74 vuniex ⊢ ∪ 𝑦 ∈ V
75 74 a1i ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ∪ 𝑦 ∈ V )
76 elpwg ⊢ ( ∪ 𝑦 ∈ V → ( ∪ 𝑦 ∈ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋 ) )
77 75 76 syl ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( ∪ 𝑦 ∈ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋 ) )
78 73 77 mpbird ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ∪ 𝑦 ∈ 𝒫 𝑋 )
79 12 a1i ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → 0 ∈ ℝ )
80 64 65 78 79 fvmptd ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( 𝑂 ‘ ∪ 𝑦 ) = 0 )
81 64 reseq1d ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( 𝑂 ↾ 𝑦 ) = ( ( 𝑧 ∈ 𝒫 𝑋 ↦ 0 ) ↾ 𝑦 ) )
82 resmpt ⊢ ( 𝑦 ⊆ 𝒫 𝑋 → ( ( 𝑧 ∈ 𝒫 𝑋 ↦ 0 ) ↾ 𝑦 ) = ( 𝑧 ∈ 𝑦 ↦ 0 ) )
83 71 82 syl ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( ( 𝑧 ∈ 𝒫 𝑋 ↦ 0 ) ↾ 𝑦 ) = ( 𝑧 ∈ 𝑦 ↦ 0 ) )
84 81 83 eqtrd ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( 𝑂 ↾ 𝑦 ) = ( 𝑧 ∈ 𝑦 ↦ 0 ) )
85 84 fveq2d ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑧 ∈ 𝑦 ↦ 0 ) ) )
86 nfv ⊢ Ⅎ 𝑧 𝑦 ∈ 𝒫 dom 𝑂
87 86 66 sge0z ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( Σ^ ‘ ( 𝑧 ∈ 𝑦 ↦ 0 ) ) = 0 )
88 85 87 eqtrd ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) = 0 )
89 80 88 breq12d ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ↔ 0 ≤ 0 ) )
90 61 89 mpbird ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) )
91 90 a1d ⊢ ( 𝑦 ∈ 𝒫 dom 𝑂 → ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) )
92 91 rgen ⊢ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) )
93 60 92 pm3.2i ⊢ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) )
94 93 a1i ⊢ ( 𝜑 → ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) )
95 9 a1i ⊢ ( 𝜑 → 𝑂 = ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) )
96 1 pwexd ⊢ ( 𝜑 → 𝒫 𝑋 ∈ V )
97 mptexg ⊢ ( 𝒫 𝑋 ∈ V → ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) ∈ V )
98 96 97 syl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝒫 𝑋 ↦ 0 ) ∈ V )
99 95 98 eqeltrd ⊢ ( 𝜑 → 𝑂 ∈ V )
100 isome ⊢ ( 𝑂 ∈ V → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) ) )
101 99 100 syl ⊢ ( 𝜑 → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑧 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) ) )
102 94 101 mpbird ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )