Step | Hyp | Ref
| Expression |
1 | | isomennd.o |
. . . . 5
⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
2 | | id 22 |
. . . . . 6
⊢ (𝑂:𝒫 𝑋⟶(0[,]+∞) → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
3 | | fdm 6607 |
. . . . . . 7
⊢ (𝑂:𝒫 𝑋⟶(0[,]+∞) → dom 𝑂 = 𝒫 𝑋) |
4 | 3 | feq2d 6584 |
. . . . . 6
⊢ (𝑂:𝒫 𝑋⟶(0[,]+∞) → (𝑂:dom 𝑂⟶(0[,]+∞) ↔ 𝑂:𝒫 𝑋⟶(0[,]+∞))) |
5 | 2, 4 | mpbird 256 |
. . . . 5
⊢ (𝑂:𝒫 𝑋⟶(0[,]+∞) → 𝑂:dom 𝑂⟶(0[,]+∞)) |
6 | 1, 5 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑂:dom 𝑂⟶(0[,]+∞)) |
7 | | unipw 5370 |
. . . . . . 7
⊢ ∪ 𝒫 𝑋 = 𝑋 |
8 | 7 | pweqi 4557 |
. . . . . 6
⊢ 𝒫
∪ 𝒫 𝑋 = 𝒫 𝑋 |
9 | 8 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝒫 ∪ 𝒫 𝑋 = 𝒫 𝑋) |
10 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 𝑂 = 𝒫 𝑋) |
11 | 10 | unieqd 4859 |
. . . . . 6
⊢ (𝜑 → ∪ dom 𝑂 = ∪ 𝒫
𝑋) |
12 | 11 | pweqd 4558 |
. . . . 5
⊢ (𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 ∪
𝒫 𝑋) |
13 | 9, 12, 10 | 3eqtr4rd 2791 |
. . . 4
⊢ (𝜑 → dom 𝑂 = 𝒫 ∪
dom 𝑂) |
14 | | isomennd.o0 |
. . . 4
⊢ (𝜑 → (𝑂‘∅) = 0) |
15 | 6, 13, 14 | jca31 515 |
. . 3
⊢ (𝜑 → ((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0)) |
16 | | simpl 483 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥)) → 𝜑) |
17 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂) → 𝑥 ∈ 𝒫 ∪ dom 𝑂) |
18 | 12, 9 | eqtrd 2780 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋) |
19 | 18 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂) → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋) |
20 | 17, 19 | eleqtrd 2843 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂) → 𝑥 ∈ 𝒫 𝑋) |
21 | | elpwi 4548 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 ∪ dom 𝑂) → 𝑥 ⊆ 𝑋) |
23 | 22 | adantrr 714 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥)) → 𝑥 ⊆ 𝑋) |
24 | | elpwi 4548 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 𝑥 → 𝑦 ⊆ 𝑥) |
25 | 24 | adantl 482 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥) → 𝑦 ⊆ 𝑥) |
26 | 25 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥)) → 𝑦 ⊆ 𝑥) |
27 | | isomennd.le |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥) → (𝑂‘𝑦) ≤ (𝑂‘𝑥)) |
28 | 16, 23, 26, 27 | syl3anc 1370 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 ∪ dom 𝑂 ∧ 𝑦 ∈ 𝒫 𝑥)) → (𝑂‘𝑦) ≤ (𝑂‘𝑥)) |
29 | 28 | ralrimivva 3117 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝒫 ∪ dom 𝑂∀𝑦 ∈ 𝒫 𝑥(𝑂‘𝑦) ≤ (𝑂‘𝑥)) |
30 | | 0le0 12074 |
. . . . . . . . 9
⊢ 0 ≤
0 |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = ∅) → 0 ≤ 0) |
32 | | unieq 4856 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∪ ∅) |
33 | | uni0 4875 |
. . . . . . . . . . . . . 14
⊢ ∪ ∅ = ∅ |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → ∪ ∅ = ∅) |
35 | 32, 34 | eqtrd 2780 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∅) |
36 | 35 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑂‘∪ 𝑥) =
(𝑂‘∅)) |
37 | 36 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑂‘∪ 𝑥) = (𝑂‘∅)) |
38 | 14 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑂‘∅) = 0) |
39 | 37, 38 | eqtrd 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑂‘∪ 𝑥) = 0) |
40 | | reseq2 5885 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑂 ↾ 𝑥) = (𝑂 ↾ ∅)) |
41 | | res0 5894 |
. . . . . . . . . . . . . 14
⊢ (𝑂 ↾ ∅) =
∅ |
42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑂 ↾ ∅) =
∅) |
43 | 40, 42 | eqtrd 2780 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑂 ↾ 𝑥) = ∅) |
44 | 43 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ →
(Σ^‘(𝑂 ↾ 𝑥)) =
(Σ^‘∅)) |
45 | | sge00 43885 |
. . . . . . . . . . . 12
⊢
(Σ^‘∅) = 0 |
46 | 45 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ →
(Σ^‘∅) = 0) |
47 | 44, 46 | eqtrd 2780 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ →
(Σ^‘(𝑂 ↾ 𝑥)) = 0) |
48 | 47 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = ∅) →
(Σ^‘(𝑂 ↾ 𝑥)) = 0) |
49 | 39, 48 | breq12d 5092 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = ∅) → ((𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)) ↔ 0 ≤ 0)) |
50 | 31, 49 | mpbird 256 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))) |
51 | 50 | ad4ant14 749 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ 𝑥 = ∅) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))) |
52 | | simpl 483 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ ¬ 𝑥 = ∅) → ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω)) |
53 | | neqne 2953 |
. . . . . . . 8
⊢ (¬
𝑥 = ∅ → 𝑥 ≠ ∅) |
54 | 53 | adantl 482 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ ¬ 𝑥 = ∅) → 𝑥 ≠ ∅) |
55 | | ssnnf1octb 42703 |
. . . . . . . . 9
⊢ ((𝑥 ≼ ω ∧ 𝑥 ≠ ∅) →
∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) |
56 | 55 | adantll 711 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) |
57 | 1 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
58 | 14 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → (𝑂‘∅) = 0) |
59 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝑥 ∈ 𝒫 dom 𝑂) |
60 | 10 | pweqd 4558 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝒫 dom 𝑂 = 𝒫 𝒫 𝑋) |
62 | 59, 61 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝑥 ∈ 𝒫 𝒫 𝑋) |
63 | | elpwi 4548 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 𝒫
𝑋 → 𝑥 ⊆ 𝒫 𝑋) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝑥 ⊆ 𝒫 𝑋) |
65 | 64 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → 𝑥 ⊆ 𝒫 𝑋) |
66 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → 𝜑) |
67 | | isomennd.sa |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) |
68 | 66, 67 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) |
69 | 68 | adantlr 712 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) |
70 | | simprl 768 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → dom 𝑓 ⊆ ℕ) |
71 | | simprr 770 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → 𝑓:dom 𝑓–1-1-onto→𝑥) |
72 | | eleq1w 2823 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑚 ∈ dom 𝑓 ↔ 𝑛 ∈ dom 𝑓)) |
73 | | fveq2 6771 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑓‘𝑚) = (𝑓‘𝑛)) |
74 | 72, 73 | ifbieq1d 4489 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → if(𝑚 ∈ dom 𝑓, (𝑓‘𝑚), ∅) = if(𝑛 ∈ dom 𝑓, (𝑓‘𝑛), ∅)) |
75 | 74 | cbvmptv 5192 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ ↦ if(𝑚 ∈ dom 𝑓, (𝑓‘𝑚), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ dom 𝑓, (𝑓‘𝑛), ∅)) |
76 | 57, 58, 65, 69, 70, 71, 75 | isomenndlem 44039 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ (dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥)) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))) |
77 | 76 | ex 413 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → ((dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))) |
78 | 77 | ad2antrr 723 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → ((dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝑥) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))) |
79 | 78 | exlimdv 1940 |
. . . . . . . 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 810 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) ∧ 𝑥 ≼ ω) → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))) |
83 | 82 | ex 413 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑂) → (𝑥 ≼ ω → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))) |
84 | 83 | ralrimiva 3110 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝒫 dom 𝑂(𝑥 ≼ ω → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥)))) |
85 | 15, 29, 84 | jca31 515 |
. 2
⊢ (𝜑 → ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑥 ∈ 𝒫 ∪ dom 𝑂∀𝑦 ∈ 𝒫 𝑥(𝑂‘𝑦) ≤ (𝑂‘𝑥)) ∧ ∀𝑥 ∈ 𝒫 dom 𝑂(𝑥 ≼ ω → (𝑂‘∪ 𝑥) ≤
(Σ^‘(𝑂 ↾ 𝑥))))) |
86 | | isomennd.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
87 | 86 | pwexd 5306 |
. . . 4
⊢ (𝜑 → 𝒫 𝑋 ∈ V) |
88 | 1, 87 | fexd 7100 |
. . 3
⊢ (𝜑 → 𝑂 ∈ V) |
89 | | isome 44003 |
. . 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 256 |
1
⊢ (𝜑 → 𝑂 ∈ OutMeas) |