Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → 𝑥 = 𝑂) |
2 | | dmeq 5746 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → dom 𝑥 = dom 𝑂) |
3 | 1, 2 | feq12d 6492 |
. . . . . 6
⊢ (𝑥 = 𝑂 → (𝑥:dom 𝑥⟶(0[,]+∞) ↔ 𝑂:dom 𝑂⟶(0[,]+∞))) |
4 | 2 | unieqd 4810 |
. . . . . . . 8
⊢ (𝑥 = 𝑂 → ∪ dom
𝑥 = ∪ dom 𝑂) |
5 | 4 | pweqd 4507 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → 𝒫 ∪ dom 𝑥 = 𝒫 ∪ dom
𝑂) |
6 | 2, 5 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑥 = 𝑂 → (dom 𝑥 = 𝒫 ∪ dom
𝑥 ↔ dom 𝑂 = 𝒫 ∪ dom 𝑂)) |
7 | 3, 6 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = 𝑂 → ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ↔ (𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂))) |
8 | | fveq1 6673 |
. . . . . 6
⊢ (𝑥 = 𝑂 → (𝑥‘∅) = (𝑂‘∅)) |
9 | 8 | eqeq1d 2740 |
. . . . 5
⊢ (𝑥 = 𝑂 → ((𝑥‘∅) = 0 ↔ (𝑂‘∅) = 0)) |
10 | 7, 9 | anbi12d 634 |
. . . 4
⊢ (𝑥 = 𝑂 → (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ↔ ((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0))) |
11 | | fveq1 6673 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → (𝑥‘𝑧) = (𝑂‘𝑧)) |
12 | | fveq1 6673 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → (𝑥‘𝑦) = (𝑂‘𝑦)) |
13 | 11, 12 | breq12d 5043 |
. . . . . 6
⊢ (𝑥 = 𝑂 → ((𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ (𝑂‘𝑧) ≤ (𝑂‘𝑦))) |
14 | 13 | ralbidv 3109 |
. . . . 5
⊢ (𝑥 = 𝑂 → (∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ ∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦))) |
15 | 5, 14 | raleqbidv 3304 |
. . . 4
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦))) |
16 | 10, 15 | anbi12d 634 |
. . 3
⊢ (𝑥 = 𝑂 → ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ↔ (((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)))) |
17 | 2 | pweqd 4507 |
. . . 4
⊢ (𝑥 = 𝑂 → 𝒫 dom 𝑥 = 𝒫 dom 𝑂) |
18 | | fveq1 6673 |
. . . . . 6
⊢ (𝑥 = 𝑂 → (𝑥‘∪ 𝑦) = (𝑂‘∪ 𝑦)) |
19 | | reseq1 5819 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → (𝑥 ↾ 𝑦) = (𝑂 ↾ 𝑦)) |
20 | 19 | fveq2d 6678 |
. . . . . 6
⊢ (𝑥 = 𝑂 →
(Σ^‘(𝑥 ↾ 𝑦)) =
(Σ^‘(𝑂 ↾ 𝑦))) |
21 | 18, 20 | breq12d 5043 |
. . . . 5
⊢ (𝑥 = 𝑂 → ((𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦)) ↔ (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))) |
22 | 21 | imbi2d 344 |
. . . 4
⊢ (𝑥 = 𝑂 → ((𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))) ↔ (𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))))) |
23 | 17, 22 | raleqbidv 3304 |
. . 3
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))) ↔ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))))) |
24 | 16, 23 | anbi12d 634 |
. 2
⊢ (𝑥 = 𝑂 → (((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦)))) ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) |
25 | | df-ome 43570 |
. 2
⊢ OutMeas =
{𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))))} |
26 | 24, 25 | elab2g 3575 |
1
⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) |