Step | Hyp | Ref
| Expression |
1 | | df-ome 39380 |
. . . 4
⊢ OutMeas =
{𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))))} |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑂 ∈ 𝑉 → OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))))}) |
3 | 2 | eleq2d 2673 |
. 2
⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ OutMeas ↔ 𝑂 ∈ {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))))})) |
4 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 𝑂 → 𝑥 = 𝑂) |
5 | | dmeq 5246 |
. . . . . . . 8
⊢ (𝑥 = 𝑂 → dom 𝑥 = dom 𝑂) |
6 | 4, 5 | feq12d 5946 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → (𝑥:dom 𝑥⟶(0[,]+∞) ↔ 𝑂:dom 𝑂⟶(0[,]+∞))) |
7 | 5 | unieqd 4382 |
. . . . . . . . 9
⊢ (𝑥 = 𝑂 → ∪ dom
𝑥 = ∪ dom 𝑂) |
8 | 7 | pweqd 4113 |
. . . . . . . 8
⊢ (𝑥 = 𝑂 → 𝒫 ∪ dom 𝑥 = 𝒫 ∪ dom
𝑂) |
9 | 5, 8 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → (dom 𝑥 = 𝒫 ∪ dom
𝑥 ↔ dom 𝑂 = 𝒫 ∪ dom 𝑂)) |
10 | 6, 9 | anbi12d 743 |
. . . . . 6
⊢ (𝑥 = 𝑂 → ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ↔ (𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂))) |
11 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → (𝑥‘∅) = (𝑂‘∅)) |
12 | 11 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 = 𝑂 → ((𝑥‘∅) = 0 ↔ (𝑂‘∅) = 0)) |
13 | 10, 12 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = 𝑂 → (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ↔ ((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0))) |
14 | 8 | raleqdv 3121 |
. . . . . 6
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦))) |
15 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑥 = 𝑂 → (𝑥‘𝑧) = (𝑂‘𝑧)) |
16 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑥 = 𝑂 → (𝑥‘𝑦) = (𝑂‘𝑦)) |
17 | 15, 16 | breq12d 4596 |
. . . . . . . 8
⊢ (𝑥 = 𝑂 → ((𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ (𝑂‘𝑧) ≤ (𝑂‘𝑦))) |
18 | 17 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → (∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ ∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦))) |
19 | 18 | ralbidv 2969 |
. . . . . 6
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦))) |
20 | 14, 19 | bitrd 267 |
. . . . 5
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) ↔ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦))) |
21 | 13, 20 | anbi12d 743 |
. . . 4
⊢ (𝑥 = 𝑂 → ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ↔ (((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)))) |
22 | 5 | pweqd 4113 |
. . . . . 6
⊢ (𝑥 = 𝑂 → 𝒫 dom 𝑥 = 𝒫 dom 𝑂) |
23 | 22 | raleqdv 3121 |
. . . . 5
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))) ↔ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))))) |
24 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑥 = 𝑂 → (𝑥‘∪ 𝑦) = (𝑂‘∪ 𝑦)) |
25 | | reseq1 5311 |
. . . . . . . . 9
⊢ (𝑥 = 𝑂 → (𝑥 ↾ 𝑦) = (𝑂 ↾ 𝑦)) |
26 | 25 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = 𝑂 →
(Σ^‘(𝑥 ↾ 𝑦)) =
(Σ^‘(𝑂 ↾ 𝑦))) |
27 | 24, 26 | breq12d 4596 |
. . . . . . 7
⊢ (𝑥 = 𝑂 → ((𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦)) ↔ (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))) |
28 | 27 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = 𝑂 → ((𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))) ↔ (𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))))) |
29 | 28 | ralbidv 2969 |
. . . . 5
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))) ↔ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))))) |
30 | 23, 29 | bitrd 267 |
. . . 4
⊢ (𝑥 = 𝑂 → (∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))) ↔ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦))))) |
31 | 21, 30 | anbi12d 743 |
. . 3
⊢ (𝑥 = 𝑂 → (((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦)))) ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) |
32 | 31 | elabg 3320 |
. 2
⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))))} ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) |
33 | 3, 32 | bitrd 267 |
1
⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤
(Σ^‘(𝑂 ↾ 𝑦)))))) |