| Step | Hyp | Ref
| Expression |
| 1 | | isomennd.o |
. . . . 5
⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
| 2 | | id 22 |
. . . . . 6
⊢ (𝑂:𝒫 𝑋⟶(0[,]+∞) → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
| 3 | | fdm 6745 |
. . . . . . 7
⊢ (𝑂:𝒫 𝑋⟶(0[,]+∞) → dom 𝑂 = 𝒫 𝑋) |
| 4 | 3 | feq2d 6722 |
. . . . . 6
⊢ (𝑂:𝒫 𝑋⟶(0[,]+∞) → (𝑂:dom 𝑂⟶(0[,]+∞) ↔ 𝑂:𝒫 𝑋⟶(0[,]+∞))) |
| 5 | 2, 4 | mpbird 257 |
. . . . 5
⊢ (𝑂:𝒫 𝑋⟶(0[,]+∞) → 𝑂:dom 𝑂⟶(0[,]+∞)) |
| 6 | 1, 5 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑂:dom 𝑂⟶(0[,]+∞)) |
| 7 | | unipw 5455 |
. . . . . . 7
⊢ ∪ 𝒫 𝑋 = 𝑋 |
| 8 | 7 | pweqi 4616 |
. . . . . 6
⊢ 𝒫
∪ 𝒫 𝑋 = 𝒫 𝑋 |
| 9 | 8 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝒫 ∪ 𝒫 𝑋 = 𝒫 𝑋) |
| 10 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 𝑂 = 𝒫 𝑋) |
| 11 | 10 | unieqd 4920 |
. . . . . 6
⊢ (𝜑 → ∪ dom 𝑂 = ∪ 𝒫
𝑋) |
| 12 | 11 | pweqd 4617 |
. . . . 5
⊢ (𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 ∪
𝒫 𝑋) |
| 13 | 9, 12, 10 | 3eqtr4rd 2788 |
. . . 4
⊢ (𝜑 → dom 𝑂 = 𝒫 ∪
dom 𝑂) |
| 14 | | isomennd.o0 |
. . . 4
⊢ (𝜑 → (𝑂‘∅) = 0) |
| 15 | 6, 13, 14 | jca31 514 |
. . 3
⊢ (𝜑 → ((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0)) |
| 16 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥)) → 𝜑) |
| 17 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂) → 𝑥 ∈ 𝒫 ∪ dom 𝑂) |
| 18 | 12, 9 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂) → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋) |
| 20 | 17, 19 | eleqtrd 2843 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂) → 𝑥 ∈ 𝒫 𝑋) |
| 21 | | elpwi 4607 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
| 22 | 20, 21 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂) → 𝑥 ⊆ 𝑋) |
| 23 | 22 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥)) → 𝑥 ⊆ 𝑋) |
| 24 | | elpwi 4607 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 𝑥 → 𝑦 ⊆ 𝑥) |
| 25 | 24 | adantl 481 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥) → 𝑦 ⊆ 𝑥) |
| 26 | 25 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥)) → 𝑦 ⊆ 𝑥) |
| 27 | | isomennd.le |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥) → (𝑂‘𝑦) ≤ (𝑂‘𝑥)) |
| 28 | 16, 23, 26, 27 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥)) → (𝑂‘𝑦) ≤ (𝑂‘𝑥)) |
| 29 | 28 | ralrimivva 3202 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝒫 ∪ dom 𝑂∀𝑦 ∈ 𝒫 𝑥(𝑂‘𝑦) ≤ (𝑂‘𝑥)) |
| 30 | | 0le0 12367 |
. . . . . . . . 9
⊢ 0 ≤
0 |
| 31 | 30 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = ∅) → 0 ≤ 0) |
| 32 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∪ ∅) |
| 33 | | uni0 4935 |
. . . . . . . . . . . . . 14
⊢ ∪ ∅ = ∅ |
| 34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → ∪ ∅ = ∅) |
| 35 | 32, 34 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∅) |
| 36 | 35 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑂‘∪ 𝑥) =
(𝑂‘∅)) |
| 37 | 36 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑂‘∪ 𝑥) = (𝑂‘∅)) |
| 38 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑂‘∅) = 0) |
| 39 | 37, 38 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑂‘∪ 𝑥) = 0) |
| 40 | | reseq2 5992 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑂 ↾ 𝑥) = (𝑂 ↾ ∅)) |
| 41 | | res0 6001 |
. . . . . . . . . . . . . 14
⊢ (𝑂 ↾ ∅) =
∅ |
| 42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑂 ↾ ∅) =
∅) |
| 43 | 40, 42 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑂 ↾ 𝑥) = ∅) |
| 44 | 43 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ →
(Σ^‘(𝑂 ↾ 𝑥)) =
(Σ^‘∅)) |
| 45 | | sge00 46391 |
. . . . . . . . . . . 12
⊢
(Σ^‘∅) = 0 |
| 46 | 45 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ →
(Σ^‘∅) = 0) |
| 47 | 44, 46 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ →
(Σ^‘(𝑂 ↾ 𝑥)) = 0) |
| 48 | 47 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = ∅) →
(Σ^‘(𝑂 ↾ 𝑥)) = 0) |
| 49 | 39, 48 | breq12d 5156 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = ∅) → ((𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)) ↔ 0 ≤ 0)) |
| 50 | 31, 49 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))) |
| 51 | 50 | ad4ant14 752 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ 𝑥 = ∅) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))) |
| 52 | | simpl 482 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ ¬ 𝑥 = ∅) → ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω)) |
| 53 | | neqne 2948 |
. . . . . . . 8
⊢ (¬
𝑥 = ∅ → 𝑥 ≠ ∅) |
| 54 | 53 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ ¬ 𝑥 = ∅) → 𝑥 ≠ ∅) |
| 55 | | ssnnf1octb 45199 |
. . . . . . . . 9
⊢ ((𝑥 ≼ ω ∧ 𝑥 ≠ ∅) →
∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) |
| 56 | 55 | adantll 714 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) |
| 57 | 1 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
| 58 | 14 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → (𝑂‘∅) = 0) |
| 59 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝑥 ∈ 𝒫 dom 𝑂) |
| 60 | 10 | pweqd 4617 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋) |
| 61 | 60 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋) |
| 62 | 59, 61 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝑥 ∈ 𝒫 𝒫 𝑋) |
| 63 | | elpwi 4607 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 𝒫
𝑋 → 𝑥 ⊆ 𝒫 𝑋) |
| 64 | 62, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝑥 ⊆ 𝒫 𝑋) |
| 65 | 64 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → 𝑥 ⊆ 𝒫 𝑋) |
| 66 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝜑) |
| 67 | | isomennd.sa |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) |
| 68 | 66, 67 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) |
| 69 | 68 | adantlr 715 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) |
| 70 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → dom 𝑓 ⊆ ℕ) |
| 71 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → 𝑓:dom 𝑓–1-1-onto→𝑥) |
| 72 | | eleq1w 2824 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑚 ∈ dom 𝑓 ↔ 𝑛 ∈ dom 𝑓)) |
| 73 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑓‘𝑚) = (𝑓‘𝑛)) |
| 74 | 72, 73 | ifbieq1d 4550 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → if(𝑚 ∈ dom 𝑓, (𝑓‘𝑚), ∅) = if(𝑛 ∈ dom 𝑓, (𝑓‘𝑛), ∅)) |
| 75 | 74 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ ↦ if(𝑚 ∈ dom 𝑓, (𝑓‘𝑚), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ dom 𝑓, (𝑓‘𝑛), ∅)) |
| 76 | 57, 58, 65, 69, 70, 71, 75 | isomenndlem 46545 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))) |
| 77 | 76 | ex 412 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → ((dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))) |
| 78 | 77 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → ((dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))) |
| 79 | 78 | exlimdv 1933 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → (∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))) |
| 80 | 56, 79 | mpd 15 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))) |
| 81 | 52, 54, 80 | syl2anc 584 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ ¬ 𝑥 = ∅) → (𝑂‘∪ 𝑥)
≤ (Σ^‘(𝑂 ↾ 𝑥))) |
| 82 | 51, 81 | pm2.61dan 813 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))) |
| 83 | 82 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → (𝑥 ≼ ω → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))) |
| 84 | 83 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝒫 dom 𝑂(𝑥 ≼ ω → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))) |
| 85 | 15, 29, 84 | jca31 514 |
. 2
⊢ (𝜑 → ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑥 ∈ 𝒫 ∪ dom 𝑂∀𝑦 ∈ 𝒫 𝑥(𝑂‘𝑦) ≤ (𝑂‘𝑥)) ∧ ∀𝑥 ∈ 𝒫 dom 𝑂(𝑥 ≼ ω → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))))) |
| 86 | | isomennd.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 87 | 86 | pwexd 5379 |
. . . 4
⊢ (𝜑 → 𝒫 𝑋 ∈ V) |
| 88 | 1, 87 | fexd 7247 |
. . 3
⊢ (𝜑 → 𝑂 ∈ V) |
| 89 | | isome 46509 |
. . 3
⊢ (𝑂 ∈ V → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑥 ∈ 𝒫 ∪ dom 𝑂∀𝑦 ∈ 𝒫 𝑥(𝑂‘𝑦) ≤ (𝑂‘𝑥)) ∧ ∀𝑥 ∈ 𝒫 dom 𝑂(𝑥 ≼ ω → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))))) |
| 90 | 88, 89 | syl 17 |
. 2
⊢ (𝜑 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑥 ∈ 𝒫 ∪ dom 𝑂∀𝑦 ∈ 𝒫 𝑥(𝑂‘𝑦) ≤ (𝑂‘𝑥)) ∧ ∀𝑥 ∈ 𝒫 dom 𝑂(𝑥 ≼ ω → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))))) |
| 91 | 85, 90 | mpbird 257 |
1
⊢ (𝜑 → 𝑂 ∈ OutMeas) |