Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
isomennd.o ⊢ ( 𝜑 → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
isomennd.o0 ⊢ ( 𝜑 → ( 𝑂 ‘ ∅ ) = 0 )
isomennd.le ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝑂 ‘ 𝑦 ) ≤ ( 𝑂 ‘ 𝑥 ) )
isomennd.sa ⊢ ( ( 𝜑 ∧ 𝑎 : ℕ ⟶ 𝒫 𝑋 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) )
Assertion isomennd ( 𝜑 → 𝑂 ∈ OutMeas )

Proof

Step Hyp Ref Expression
1 isomennd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 isomennd.o ⊢ ( 𝜑 → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
3 isomennd.o0 ⊢ ( 𝜑 → ( 𝑂 ‘ ∅ ) = 0 )
4 isomennd.le ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝑂 ‘ 𝑦 ) ≤ ( 𝑂 ‘ 𝑥 ) )
5 isomennd.sa ⊢ ( ( 𝜑 ∧ 𝑎 : ℕ ⟶ 𝒫 𝑋 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) )
6 id ⊢ ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
7 fdm ⊢ ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) → dom 𝑂 = 𝒫 𝑋 )
8 7 feq2d ⊢ ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) → ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ↔ 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) ) )
9 6 8 mpbird ⊢ ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) → 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) )
10 2 9 syl ⊢ ( 𝜑 → 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) )
11 unipw ⊢ ∪ 𝒫 𝑋 = 𝑋
12 11 pweqi ⊢ 𝒫 ∪ 𝒫 𝑋 = 𝒫 𝑋
13 12 a1i ⊢ ( 𝜑 → 𝒫 ∪ 𝒫 𝑋 = 𝒫 𝑋 )
14 2 7 syl ⊢ ( 𝜑 → dom 𝑂 = 𝒫 𝑋 )
15 14 unieqd ⊢ ( 𝜑 → ∪ dom 𝑂 = ∪ 𝒫 𝑋 )
16 15 pweqd ⊢ ( 𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 ∪ 𝒫 𝑋 )
17 13 16 14 3eqtr4rd ⊢ ( 𝜑 → dom 𝑂 = 𝒫 ∪ dom 𝑂 )
18 10 17 3 jca31 ⊢ ( 𝜑 → ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) )
19 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥 ) ) → 𝜑 )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑥 ∈ 𝒫 ∪ dom 𝑂 )
21 16 13 eqtrd ⊢ ( 𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ) → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋 )
23 20 22 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑥 ∈ 𝒫 𝑋 )
24 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑥 ⊆ 𝑋 )
26 25 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥 ) ) → 𝑥 ⊆ 𝑋 )
27 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ⊆ 𝑥 )
28 27 adantl ⊢ ( ( 𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥 ) → 𝑦 ⊆ 𝑥 )
29 28 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥 ) ) → 𝑦 ⊆ 𝑥 )
30 19 26 29 4 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥 ) ) → ( 𝑂 ‘ 𝑦 ) ≤ ( 𝑂 ‘ 𝑥 ) )
31 30 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑂 ‘ 𝑦 ) ≤ ( 𝑂 ‘ 𝑥 ) )
32 0le0 ⊢ 0 ≤ 0
33 32 a1i ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → 0 ≤ 0 )
34 unieq ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∪ ∅ )
35 uni0 ⊢ ∪ ∅ = ∅
36 35 a1i ⊢ ( 𝑥 = ∅ → ∪ ∅ = ∅ )
37 34 36 eqtrd ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∅ )
38 37 fveq2d ⊢ ( 𝑥 = ∅ → ( 𝑂 ‘ ∪ 𝑥 ) = ( 𝑂 ‘ ∅ ) )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( 𝑂 ‘ ∪ 𝑥 ) = ( 𝑂 ‘ ∅ ) )
40 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( 𝑂 ‘ ∅ ) = 0 )
41 39 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( 𝑂 ‘ ∪ 𝑥 ) = 0 )
42 reseq2 ⊢ ( 𝑥 = ∅ → ( 𝑂 ↾ 𝑥 ) = ( 𝑂 ↾ ∅ ) )
43 res0 ⊢ ( 𝑂 ↾ ∅ ) = ∅
44 43 a1i ⊢ ( 𝑥 = ∅ → ( 𝑂 ↾ ∅ ) = ∅ )
45 42 44 eqtrd ⊢ ( 𝑥 = ∅ → ( 𝑂 ↾ 𝑥 ) = ∅ )
46 45 fveq2d ⊢ ( 𝑥 = ∅ → ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) = ( Σ^ ‘ ∅ ) )
47 sge00 ⊢ ( Σ^ ‘ ∅ ) = 0
48 47 a1i ⊢ ( 𝑥 = ∅ → ( Σ^ ‘ ∅ ) = 0 )
49 46 48 eqtrd ⊢ ( 𝑥 = ∅ → ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) = 0 )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) = 0 )
51 41 50 breq12d ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) ↔ 0 ≤ 0 ) )
52 33 51 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) )
53 52 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 = ∅ ) → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) )
54 simpl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) ∧ ¬ 𝑥 = ∅ ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) )
55 neqne ⊢ ( ¬ 𝑥 = ∅ → 𝑥 ≠ ∅ )
56 55 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) ∧ ¬ 𝑥 = ∅ ) → 𝑥 ≠ ∅ )
57 ssnnf1octb ⊢ ( ( 𝑥 ≼ ω ∧ 𝑥 ≠ ∅ ) → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) )
58 57 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) )
59 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) ) → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
60 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) ) → ( 𝑂 ‘ ∅ ) = 0 )
61 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) → 𝑥 ∈ 𝒫 dom 𝑂 )
62 14 pweqd ⊢ ( 𝜑 → 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋 )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) → 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋 )
64 61 63 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) → 𝑥 ∈ 𝒫 𝒫 𝑋 )
65 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝒫 𝑋 → 𝑥 ⊆ 𝒫 𝑋 )
66 64 65 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) → 𝑥 ⊆ 𝒫 𝑋 )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) ) → 𝑥 ⊆ 𝒫 𝑋 )
68 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) → 𝜑 )
69 68 5 sylan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑎 : ℕ ⟶ 𝒫 𝑋 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) )
70 69 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) ) ∧ 𝑎 : ℕ ⟶ 𝒫 𝑋 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) )
71 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) ) → dom 𝑓 ⊆ ℕ )
72 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) ) → 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 )
73 eleq1w ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ∈ dom 𝑓 ↔ 𝑛 ∈ dom 𝑓 ) )
74 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑓 ‘ 𝑚 ) = ( 𝑓 ‘ 𝑛 ) )
75 73 74 ifbieq1d ⊢ ( 𝑚 = 𝑛 → if ( 𝑚 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑚 ) , ∅ ) = if ( 𝑛 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑛 ) , ∅ ) )
76 75 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑚 ) , ∅ ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑛 ) , ∅ ) )
77 59 60 67 70 71 72 76 isomenndlem ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) ) → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) )
78 77 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) → ( ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) ) )
79 78 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ( ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) ) )
80 79 exlimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ( ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝑥 ) → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) ) )
81 58 80 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) )
82 54 56 81 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) ∧ ¬ 𝑥 = ∅ ) → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) )
83 53 82 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) ∧ 𝑥 ≼ ω ) → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) )
84 83 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂 ) → ( 𝑥 ≼ ω → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) ) )
85 84 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 dom 𝑂 ( 𝑥 ≼ ω → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) ) )
86 18 31 85 jca31 ⊢ ( 𝜑 → ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑂 ‘ 𝑦 ) ≤ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑂 ( 𝑥 ≼ ω → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) ) ) )
87 1 pwexd ⊢ ( 𝜑 → 𝒫 𝑋 ∈ V )
88 2 87 fexd ⊢ ( 𝜑 → 𝑂 ∈ V )
89 isome ⊢ ( 𝑂 ∈ V → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑂 ‘ 𝑦 ) ≤ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑂 ( 𝑥 ≼ ω → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) ) ) ) )
90 88 89 syl ⊢ ( 𝜑 → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑂 ‘ 𝑦 ) ≤ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑂 ( 𝑥 ≼ ω → ( 𝑂 ‘ ∪ 𝑥 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑥 ) ) ) ) ) )
91 86 90 mpbird ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )