| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | omessle.a | . . 3
⊢ (𝜑 → 𝐴 ⊆ 𝐵) | 
| 2 |  | omessle.o | . . . . . . 7
⊢ (𝜑 → 𝑂 ∈ OutMeas) | 
| 3 |  | omessle.x | . . . . . . 7
⊢ 𝑋 = ∪
dom 𝑂 | 
| 4 | 2, 3 | unidmex 45060 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ V) | 
| 5 |  | omessle.b | . . . . . 6
⊢ (𝜑 → 𝐵 ⊆ 𝑋) | 
| 6 | 4, 5 | ssexd 5323 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ V) | 
| 7 | 6, 1 | ssexd 5323 | . . . 4
⊢ (𝜑 → 𝐴 ∈ V) | 
| 8 |  | elpwg 4602 | . . . 4
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | 
| 9 | 7, 8 | syl 17 | . . 3
⊢ (𝜑 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | 
| 10 | 1, 9 | mpbird 257 | . 2
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) | 
| 11 | 5, 3 | sseqtrdi 4023 | . . . 4
⊢ (𝜑 → 𝐵 ⊆ ∪ dom
𝑂) | 
| 12 |  | elpwg 4602 | . . . . 5
⊢ (𝐵 ∈ V → (𝐵 ∈ 𝒫 ∪ dom 𝑂 ↔ 𝐵 ⊆ ∪ dom
𝑂)) | 
| 13 | 6, 12 | syl 17 | . . . 4
⊢ (𝜑 → (𝐵 ∈ 𝒫 ∪ dom 𝑂 ↔ 𝐵 ⊆ ∪ dom
𝑂)) | 
| 14 | 11, 13 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐵 ∈ 𝒫 ∪ dom 𝑂) | 
| 15 |  | isome 46514 | . . . . . 6
⊢ (𝑂 ∈ OutMeas → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) | 
| 16 | 2, 15 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) | 
| 17 | 2, 16 | mpbid 232 | . . . 4
⊢ (𝜑 → ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))))) | 
| 18 | 17 | simplrd 769 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) | 
| 19 |  | pweq 4613 | . . . . . 6
⊢ (𝑦 = 𝐵 → 𝒫 𝑦 = 𝒫 𝐵) | 
| 20 | 19 | raleqdv 3325 | . . . . 5
⊢ (𝑦 = 𝐵 → (∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦) ↔ ∀𝑧 ∈ 𝒫 𝐵(𝑂‘𝑧) ≤ (𝑂‘𝑦))) | 
| 21 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑂‘𝑦) = (𝑂‘𝐵)) | 
| 22 | 21 | breq2d 5154 | . . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑂‘𝑧) ≤ (𝑂‘𝑦) ↔ (𝑂‘𝑧) ≤ (𝑂‘𝐵))) | 
| 23 | 22 | ralbidv 3177 | . . . . 5
⊢ (𝑦 = 𝐵 → (∀𝑧 ∈ 𝒫 𝐵(𝑂‘𝑧) ≤ (𝑂‘𝑦) ↔ ∀𝑧 ∈ 𝒫 𝐵(𝑂‘𝑧) ≤ (𝑂‘𝐵))) | 
| 24 | 20, 23 | bitrd 279 | . . . 4
⊢ (𝑦 = 𝐵 → (∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦) ↔ ∀𝑧 ∈ 𝒫 𝐵(𝑂‘𝑧) ≤ (𝑂‘𝐵))) | 
| 25 | 24 | rspcva 3619 | . . 3
⊢ ((𝐵 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) → ∀𝑧 ∈ 𝒫 𝐵(𝑂‘𝑧) ≤ (𝑂‘𝐵)) | 
| 26 | 14, 18, 25 | syl2anc 584 | . 2
⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝐵(𝑂‘𝑧) ≤ (𝑂‘𝐵)) | 
| 27 |  | fveq2 6905 | . . . 4
⊢ (𝑧 = 𝐴 → (𝑂‘𝑧) = (𝑂‘𝐴)) | 
| 28 | 27 | breq1d 5152 | . . 3
⊢ (𝑧 = 𝐴 → ((𝑂‘𝑧) ≤ (𝑂‘𝐵) ↔ (𝑂‘𝐴) ≤ (𝑂‘𝐵))) | 
| 29 | 28 | rspcva 3619 | . 2
⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ∀𝑧 ∈ 𝒫 𝐵(𝑂‘𝑧) ≤ (𝑂‘𝐵)) → (𝑂‘𝐴) ≤ (𝑂‘𝐵)) | 
| 30 | 10, 26, 29 | syl2anc 584 | 1
⊢ (𝜑 → (𝑂‘𝐴) ≤ (𝑂‘𝐵)) |