| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . . . . 7
⊢ (𝑥 = 𝑂 → 𝑥 = 𝑂) | 
| 2 |  | dmeq 5913 | . . . . . . 7
⊢ (𝑥 = 𝑂 → dom 𝑥 = dom 𝑂) | 
| 3 | 1, 2 | feq12d 6723 | . . . . . 6
⊢ (𝑥 = 𝑂 → (𝑥:dom 𝑥⟶(0[,]+∞) ↔ 𝑂:dom 𝑂⟶(0[,]+∞))) | 
| 4 | 2 | unieqd 4919 | . . . . . . . 8
⊢ (𝑥 = 𝑂 → ∪ dom
𝑥 = ∪ dom 𝑂) | 
| 5 | 4 | pweqd 4616 | . . . . . . 7
⊢ (𝑥 = 𝑂 → 𝒫 ∪ dom 𝑥 = 𝒫 ∪ dom
𝑂) | 
| 6 | 2, 5 | eqeq12d 2752 | . . . . . 6
⊢ (𝑥 = 𝑂 → (dom 𝑥 = 𝒫 ∪ dom
𝑥 ↔ dom 𝑂 = 𝒫 ∪ dom 𝑂)) | 
| 7 | 3, 6 | anbi12d 632 | . . . . 5
⊢ (𝑥 = 𝑂 → ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ↔ (𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂))) | 
| 8 |  | fveq1 6904 | . . . . . 6
⊢ (𝑥 = 𝑂 → (𝑥‘∅) = (𝑂‘∅)) | 
| 9 | 8 | eqeq1d 2738 | . . . . 5
⊢ (𝑥 = 𝑂 → ((𝑥‘∅) = 0 ↔ (𝑂‘∅) = 0)) | 
| 10 | 7, 9 | anbi12d 632 | . . . 4
⊢ (𝑥 = 𝑂 → (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ↔ ((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0))) | 
| 11 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑥 = 𝑂 → (𝑥‘𝑧) = (𝑂‘𝑧)) | 
| 12 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑥 = 𝑂 → (𝑥‘𝑦) = (𝑂‘𝑦)) | 
| 13 | 11, 12 | breq12d 5155 | . . . . . 6
⊢ (𝑥 = 𝑂 → ((𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ (𝑂‘𝑧) ≤ (𝑂‘𝑦))) | 
| 14 | 13 | ralbidv 3177 | . . . . 5
⊢ (𝑥 = 𝑂 → (∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ ∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦))) | 
| 15 | 5, 14 | raleqbidv 3345 | . . . 4
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦))) | 
| 16 | 10, 15 | anbi12d 632 | . . 3
⊢ (𝑥 = 𝑂 → ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ↔ (((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)))) | 
| 17 | 2 | pweqd 4616 | . . . 4
⊢ (𝑥 = 𝑂 → 𝒫 dom 𝑥 = 𝒫 dom 𝑂) | 
| 18 |  | fveq1 6904 | . . . . . 6
⊢ (𝑥 = 𝑂 → (𝑥‘∪ 𝑦) = (𝑂‘∪ 𝑦)) | 
| 19 |  | reseq1 5990 | . . . . . . 7
⊢ (𝑥 = 𝑂 → (𝑥 ↾ 𝑦) = (𝑂 ↾ 𝑦)) | 
| 20 | 19 | fveq2d 6909 | . . . . . 6
⊢ (𝑥 = 𝑂 →
(Σ^‘(𝑥 ↾ 𝑦)) =
(Σ^‘(𝑂 ↾ 𝑦))) | 
| 21 | 18, 20 | breq12d 5155 | . . . . 5
⊢ (𝑥 = 𝑂 → ((𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦)) ↔ (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))) | 
| 22 | 21 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑂 → ((𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))) ↔ (𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))))) | 
| 23 | 17, 22 | raleqbidv 3345 | . . 3
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))) ↔ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))))) | 
| 24 | 16, 23 | anbi12d 632 | . 2
⊢ (𝑥 = 𝑂 → (((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦)))) ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) | 
| 25 |  | df-ome 46510 | . 2
⊢ OutMeas =
{𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))))} | 
| 26 | 24, 25 | elab2g 3679 | 1
⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) |