| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝑋 ↦ 0) = (𝑦 ∈ 𝒫 𝑋 ↦ 0) | 
| 2 |  | 0e0iccpnf 13500 | . . . . . . . . . 10
⊢ 0 ∈
(0[,]+∞) | 
| 3 | 2 | a1i 11 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝑋 → 0 ∈
(0[,]+∞)) | 
| 4 | 1, 3 | fmpti 7131 | . . . . . . . 8
⊢ (𝑦 ∈ 𝒫 𝑋 ↦ 0):𝒫 𝑋⟶(0[,]+∞) | 
| 5 |  | 0ome.2 | . . . . . . . . . . 11
⊢ 𝑂 = (𝑥 ∈ 𝒫 𝑋 ↦ 0) | 
| 6 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 0 = 0) | 
| 7 | 6 | cbvmptv 5254 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑋 ↦ 0) = (𝑦 ∈ 𝒫 𝑋 ↦ 0) | 
| 8 | 5, 7 | eqtri 2764 | . . . . . . . . . 10
⊢ 𝑂 = (𝑦 ∈ 𝒫 𝑋 ↦ 0) | 
| 9 | 8 | feq1i 6726 | . . . . . . . . 9
⊢ (𝑂:dom 𝑂⟶(0[,]+∞) ↔ (𝑦 ∈ 𝒫 𝑋 ↦ 0):dom 𝑂⟶(0[,]+∞)) | 
| 10 | 8 | dmeqi 5914 | . . . . . . . . . . 11
⊢ dom 𝑂 = dom (𝑦 ∈ 𝒫 𝑋 ↦ 0) | 
| 11 |  | 0re 11264 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℝ | 
| 12 | 11 | rgenw 3064 | . . . . . . . . . . . 12
⊢
∀𝑦 ∈
𝒫 𝑋0 ∈
ℝ | 
| 13 |  | dmmptg 6261 | . . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝒫 𝑋0 ∈ ℝ
→ dom (𝑦 ∈
𝒫 𝑋 ↦ 0) =
𝒫 𝑋) | 
| 14 | 12, 13 | ax-mp 5 | . . . . . . . . . . 11
⊢ dom
(𝑦 ∈ 𝒫 𝑋 ↦ 0) = 𝒫 𝑋 | 
| 15 | 10, 14 | eqtri 2764 | . . . . . . . . . 10
⊢ dom 𝑂 = 𝒫 𝑋 | 
| 16 | 15 | feq2i 6727 | . . . . . . . . 9
⊢ ((𝑦 ∈ 𝒫 𝑋 ↦ 0):dom 𝑂⟶(0[,]+∞) ↔
(𝑦 ∈ 𝒫 𝑋 ↦ 0):𝒫 𝑋⟶(0[,]+∞)) | 
| 17 | 9, 16 | bitri 275 | . . . . . . . 8
⊢ (𝑂:dom 𝑂⟶(0[,]+∞) ↔ (𝑦 ∈ 𝒫 𝑋 ↦ 0):𝒫 𝑋⟶(0[,]+∞)) | 
| 18 | 4, 17 | mpbir 231 | . . . . . . 7
⊢ 𝑂:dom 𝑂⟶(0[,]+∞) | 
| 19 |  | unipw 5454 | . . . . . . . . . 10
⊢ ∪ 𝒫 𝑋 = 𝑋 | 
| 20 | 19 | pweqi 4615 | . . . . . . . . 9
⊢ 𝒫
∪ 𝒫 𝑋 = 𝒫 𝑋 | 
| 21 | 20 | eqcomi 2745 | . . . . . . . 8
⊢ 𝒫
𝑋 = 𝒫 ∪ 𝒫 𝑋 | 
| 22 | 15 | eqcomi 2745 | . . . . . . . . . 10
⊢ 𝒫
𝑋 = dom 𝑂 | 
| 23 | 22 | unieqi 4918 | . . . . . . . . 9
⊢ ∪ 𝒫 𝑋 = ∪ dom 𝑂 | 
| 24 | 23 | pweqi 4615 | . . . . . . . 8
⊢ 𝒫
∪ 𝒫 𝑋 = 𝒫 ∪
dom 𝑂 | 
| 25 | 15, 21, 24 | 3eqtri 2768 | . . . . . . 7
⊢ dom 𝑂 = 𝒫 ∪ dom 𝑂 | 
| 26 | 18, 25 | pm3.2i 470 | . . . . . 6
⊢ (𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) | 
| 27 |  | 0elpw 5355 | . . . . . . 7
⊢ ∅
∈ 𝒫 𝑋 | 
| 28 |  | eqidd 2737 | . . . . . . . 8
⊢ (𝑦 = ∅ → 0 =
0) | 
| 29 | 11 | elexi 3502 | . . . . . . . 8
⊢ 0 ∈
V | 
| 30 | 28, 8, 29 | fvmpt 7015 | . . . . . . 7
⊢ (∅
∈ 𝒫 𝑋 →
(𝑂‘∅) =
0) | 
| 31 | 27, 30 | ax-mp 5 | . . . . . 6
⊢ (𝑂‘∅) =
0 | 
| 32 | 26, 31 | pm3.2i 470 | . . . . 5
⊢ ((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) | 
| 33 | 11 | leidi 11798 | . . . . . . . . 9
⊢ 0 ≤
0 | 
| 34 | 33 | a1i 11 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 0 ≤ 0) | 
| 35 |  | eqidd 2737 | . . . . . . . . . 10
⊢ (𝑦 = 𝑧 → 0 = 0) | 
| 36 |  | elpwi 4606 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝒫 𝑦 → 𝑧 ⊆ 𝑦) | 
| 37 | 36 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑧 ⊆ 𝑦) | 
| 38 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝑦 ∈ 𝒫 ∪ dom 𝑂) | 
| 39 | 21, 24 | eqtr2i 2765 | . . . . . . . . . . . . . . . 16
⊢ 𝒫
∪ dom 𝑂 = 𝒫 𝑋 | 
| 40 | 39 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋) | 
| 41 | 38, 40 | eleqtrd 2842 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝑦 ∈ 𝒫 𝑋) | 
| 42 |  | elpwi 4606 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) | 
| 43 | 41, 42 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → 𝑦 ⊆ 𝑋) | 
| 44 | 43 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑦 ⊆ 𝑋) | 
| 45 | 37, 44 | sstrd 3993 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑧 ⊆ 𝑋) | 
| 46 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑧 ∈ 𝒫 𝑦) | 
| 47 |  | elpwg 4602 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝒫 𝑦 → (𝑧 ∈ 𝒫 𝑋 ↔ 𝑧 ⊆ 𝑋)) | 
| 48 | 46, 47 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → (𝑧 ∈ 𝒫 𝑋 ↔ 𝑧 ⊆ 𝑋)) | 
| 49 | 45, 48 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 𝑧 ∈ 𝒫 𝑋) | 
| 50 | 11 | a1i 11 | . . . . . . . . . 10
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → 0 ∈ ℝ) | 
| 51 | 8, 35, 49, 50 | fvmptd3 7038 | . . . . . . . . 9
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → (𝑂‘𝑧) = 0) | 
| 52 | 8 | fvmpt2 7026 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝒫 𝑋 ∧ 0 ∈ ℝ) →
(𝑂‘𝑦) = 0) | 
| 53 | 41, 11, 52 | sylancl 586 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → (𝑂‘𝑦) = 0) | 
| 54 | 53 | adantr 480 | . . . . . . . . 9
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → (𝑂‘𝑦) = 0) | 
| 55 | 51, 54 | breq12d 5155 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → ((𝑂‘𝑧) ≤ (𝑂‘𝑦) ↔ 0 ≤ 0)) | 
| 56 | 34, 55 | mpbird 257 | . . . . . . 7
⊢ ((𝑦 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑧 ∈ 𝒫 𝑦) → (𝑂‘𝑧) ≤ (𝑂‘𝑦)) | 
| 57 | 56 | ralrimiva 3145 | . . . . . 6
⊢ (𝑦 ∈ 𝒫 ∪ dom 𝑂 → ∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) | 
| 58 | 57 | rgen 3062 | . . . . 5
⊢
∀𝑦 ∈
𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦) | 
| 59 | 32, 58 | pm3.2i 470 | . . . 4
⊢ (((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) | 
| 60 | 33 | a1i 11 | . . . . . . 7
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 0 ≤
0) | 
| 61 | 35 | cbvmptv 5254 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 𝑋 ↦ 0) = (𝑧 ∈ 𝒫 𝑋 ↦ 0) | 
| 62 | 8, 61 | eqtri 2764 | . . . . . . . . . 10
⊢ 𝑂 = (𝑧 ∈ 𝒫 𝑋 ↦ 0) | 
| 63 | 62 | a1i 11 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝑂 = (𝑧 ∈ 𝒫 𝑋 ↦ 0)) | 
| 64 |  | eqidd 2737 | . . . . . . . . 9
⊢ ((𝑦 ∈ 𝒫 dom 𝑂 ∧ 𝑧 = ∪ 𝑦) → 0 = 0) | 
| 65 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝑦 ∈ 𝒫 dom 𝑂) | 
| 66 | 15 | pweqi 4615 | . . . . . . . . . . . . . 14
⊢ 𝒫
dom 𝑂 = 𝒫 𝒫
𝑋 | 
| 67 | 66 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋) | 
| 68 | 65, 67 | eleqtrd 2842 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝑦 ∈ 𝒫 𝒫 𝑋) | 
| 69 |  | elpwi 4606 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 → 𝑦 ⊆ 𝒫 𝑋) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 𝑦 ⊆ 𝒫 𝑋) | 
| 71 |  | sspwuni 5099 | . . . . . . . . . . 11
⊢ (𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦
⊆ 𝑋) | 
| 72 | 70, 71 | sylib 218 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ∪ 𝑦
⊆ 𝑋) | 
| 73 |  | vuniex 7760 | . . . . . . . . . . . 12
⊢ ∪ 𝑦
∈ V | 
| 74 | 73 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ∪ 𝑦
∈ V) | 
| 75 |  | elpwg 4602 | . . . . . . . . . . 11
⊢ (∪ 𝑦
∈ V → (∪ 𝑦 ∈ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋)) | 
| 76 | 74, 75 | syl 17 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (∪ 𝑦
∈ 𝒫 𝑋 ↔
∪ 𝑦 ⊆ 𝑋)) | 
| 77 | 72, 76 | mpbird 257 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ∪ 𝑦
∈ 𝒫 𝑋) | 
| 78 | 11 | a1i 11 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → 0 ∈
ℝ) | 
| 79 | 63, 64, 77, 78 | fvmptd 7022 | . . . . . . . 8
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑂‘∪ 𝑦) = 0) | 
| 80 | 63 | reseq1d 5995 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑂 ↾ 𝑦) = ((𝑧 ∈ 𝒫 𝑋 ↦ 0) ↾ 𝑦)) | 
| 81 |  | resmpt 6054 | . . . . . . . . . . . 12
⊢ (𝑦 ⊆ 𝒫 𝑋 → ((𝑧 ∈ 𝒫 𝑋 ↦ 0) ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ 0)) | 
| 82 | 70, 81 | syl 17 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ((𝑧 ∈ 𝒫 𝑋 ↦ 0) ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ 0)) | 
| 83 | 80, 82 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑂 ↾ 𝑦) = (𝑧 ∈ 𝑦 ↦ 0)) | 
| 84 | 83 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 dom 𝑂 →
(Σ^‘(𝑂 ↾ 𝑦)) =
(Σ^‘(𝑧 ∈ 𝑦 ↦ 0))) | 
| 85 |  | nfv 1913 | . . . . . . . . . 10
⊢
Ⅎ𝑧 𝑦 ∈ 𝒫 dom 𝑂 | 
| 86 | 85, 65 | sge0z 46395 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 dom 𝑂 →
(Σ^‘(𝑧 ∈ 𝑦 ↦ 0)) = 0) | 
| 87 | 84, 86 | eqtrd 2776 | . . . . . . . 8
⊢ (𝑦 ∈ 𝒫 dom 𝑂 →
(Σ^‘(𝑂 ↾ 𝑦)) = 0) | 
| 88 | 79, 87 | breq12d 5155 | . . . . . . 7
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → ((𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)) ↔ 0 ≤ 0)) | 
| 89 | 60, 88 | mpbird 257 | . . . . . 6
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))) | 
| 90 | 89 | a1d 25 | . . . . 5
⊢ (𝑦 ∈ 𝒫 dom 𝑂 → (𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))) | 
| 91 | 90 | rgen 3062 | . . . 4
⊢
∀𝑦 ∈
𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦)
≤ (Σ^‘(𝑂 ↾ 𝑦))) | 
| 92 | 59, 91 | pm3.2i 470 | . . 3
⊢ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))) | 
| 93 | 92 | a1i 11 | . 2
⊢ (𝜑 → ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))))) | 
| 94 | 8 | a1i 11 | . . . 4
⊢ (𝜑 → 𝑂 = (𝑦 ∈ 𝒫 𝑋 ↦ 0)) | 
| 95 |  | 0ome.1 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 96 | 95 | pwexd 5378 | . . . . 5
⊢ (𝜑 → 𝒫 𝑋 ∈ V) | 
| 97 |  | mptexg 7242 | . . . . 5
⊢
(𝒫 𝑋 ∈
V → (𝑦 ∈
𝒫 𝑋 ↦ 0)
∈ V) | 
| 98 | 96, 97 | syl 17 | . . . 4
⊢ (𝜑 → (𝑦 ∈ 𝒫 𝑋 ↦ 0) ∈ V) | 
| 99 | 94, 98 | eqeltrd 2840 | . . 3
⊢ (𝜑 → 𝑂 ∈ V) | 
| 100 |  | isome 46514 | . . 3
⊢ (𝑂 ∈ V → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) | 
| 101 | 99, 100 | syl 17 | . 2
⊢ (𝜑 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) | 
| 102 | 93, 101 | mpbird 257 | 1
⊢ (𝜑 → 𝑂 ∈ OutMeas) |