| Step | Hyp | Ref
| Expression |
| 1 | | caratheodorylem2.o |
. . 3
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
| 2 | | caratheodorylem2.x |
. . 3
⊢ 𝑋 = ∪
dom 𝑂 |
| 3 | | caratheodorylem2.s |
. . . . . . . . . . 11
⊢ 𝑆 = (CaraGen‘𝑂) |
| 4 | 3 | caragenss 46519 |
. . . . . . . . . 10
⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂) |
| 5 | 1, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ dom 𝑂) |
| 6 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ⊆ dom 𝑂) |
| 7 | | caratheodorylem2.e |
. . . . . . . . 9
⊢ (𝜑 → 𝐸:ℕ⟶𝑆) |
| 8 | 7 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) ∈ 𝑆) |
| 9 | 6, 8 | sseldd 3984 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) ∈ dom 𝑂) |
| 10 | | elssuni 4937 |
. . . . . . 7
⊢ ((𝐸‘𝑛) ∈ dom 𝑂 → (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
| 11 | 9, 10 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
| 12 | 11, 2 | sseqtrrdi 4025 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) ⊆ 𝑋) |
| 13 | 12 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐸‘𝑛) ⊆ 𝑋) |
| 14 | | iunss 5045 |
. . . 4
⊢ (∪ 𝑛 ∈ ℕ (𝐸‘𝑛) ⊆ 𝑋 ↔ ∀𝑛 ∈ ℕ (𝐸‘𝑛) ⊆ 𝑋) |
| 15 | 13, 14 | sylibr 234 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐸‘𝑛) ⊆ 𝑋) |
| 16 | 1, 2, 15 | omexrcl 46522 |
. 2
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛)) ∈
ℝ*) |
| 17 | | nnex 12272 |
. . . 4
⊢ ℕ
∈ V |
| 18 | 17 | a1i 11 |
. . 3
⊢ (𝜑 → ℕ ∈
V) |
| 19 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑂 ∈ OutMeas) |
| 20 | 19, 2, 12 | omecl 46518 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
| 21 | | eqid 2737 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))) |
| 22 | 20, 21 | fmptd 7134 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))):ℕ⟶(0[,]+∞)) |
| 23 | 18, 22 | sge0xrcl 46400 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛)))) ∈
ℝ*) |
| 24 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑛𝜑 |
| 25 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑛𝐸 |
| 26 | | nnuz 12921 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
| 27 | 1, 2, 3 | caragensspw 46524 |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ 𝒫 𝑋) |
| 28 | 7, 27 | fssd 6753 |
. . 3
⊢ (𝜑 → 𝐸:ℕ⟶𝒫 𝑋) |
| 29 | 24, 25, 1, 2, 26, 28 | omeiunle 46532 |
. 2
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))))) |
| 30 | | elpwinss 45054 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 ℕ ∩
Fin) → 𝑥 ⊆
ℕ) |
| 31 | 30 | resmptd 6058 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 ℕ ∩
Fin) → ((𝑛 ∈
ℕ ↦ (𝑂‘(𝐸‘𝑛))) ↾ 𝑥) = (𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛)))) |
| 32 | 31 | fveq2d 6910 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 ℕ ∩
Fin) → (Σ^‘((𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))) ↾ 𝑥)) =
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛))))) |
| 33 | 32 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 ℕ ∩ Fin)) →
(Σ^‘((𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))) ↾ 𝑥)) =
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛))))) |
| 34 | | 1zzd 12648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 ℕ ∩ Fin)) →
1 ∈ ℤ) |
| 35 | 30 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 ℕ ∩ Fin)) →
𝑥 ⊆
ℕ) |
| 36 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 ℕ ∩
Fin) → 𝑥 ∈
Fin) |
| 37 | 36 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 ℕ ∩ Fin)) →
𝑥 ∈
Fin) |
| 38 | 34, 26, 35, 37 | uzfissfz 45337 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 ℕ ∩ Fin)) →
∃𝑘 ∈ ℕ
𝑥 ⊆ (1...𝑘)) |
| 39 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 40 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ⊆ (1...𝑘)) → 𝑥 ∈ V) |
| 41 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ⊆ (1...𝑘)) ∧ 𝑛 ∈ 𝑥) → 𝑂 ∈ OutMeas) |
| 42 | 28 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ⊆ (1...𝑘)) ∧ 𝑛 ∈ 𝑥) → 𝐸:ℕ⟶𝒫 𝑋) |
| 43 | | fz1ssnn 13595 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...𝑘) ⊆
ℕ |
| 44 | | ssel2 3978 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ⊆ (1...𝑘) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ (1...𝑘)) |
| 45 | 43, 44 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ⊆ (1...𝑘) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ ℕ) |
| 46 | 45 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ⊆ (1...𝑘)) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ ℕ) |
| 47 | 42, 46 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ⊆ (1...𝑘)) ∧ 𝑛 ∈ 𝑥) → (𝐸‘𝑛) ∈ 𝒫 𝑋) |
| 48 | | elpwi 4607 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸‘𝑛) ∈ 𝒫 𝑋 → (𝐸‘𝑛) ⊆ 𝑋) |
| 49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ⊆ (1...𝑘)) ∧ 𝑛 ∈ 𝑥) → (𝐸‘𝑛) ⊆ 𝑋) |
| 50 | 41, 2, 49 | omecl 46518 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ (1...𝑘)) ∧ 𝑛 ∈ 𝑥) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
| 51 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛))) |
| 52 | 50, 51 | fmptd 7134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ⊆ (1...𝑘)) → (𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛))):𝑥⟶(0[,]+∞)) |
| 53 | 40, 52 | sge0xrcl 46400 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ (1...𝑘)) →
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛)))) ∈
ℝ*) |
| 54 | 53 | 3adant2 1132 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) →
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛)))) ∈
ℝ*) |
| 55 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢
(1...𝑘) ∈
V |
| 56 | 55 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑘) ∈ V) |
| 57 | | elfznn 13593 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ) |
| 58 | 57, 20 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑘)) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
| 59 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛))) |
| 60 | 58, 59 | fmptd 7134 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛))):(1...𝑘)⟶(0[,]+∞)) |
| 61 | 56, 60 | sge0xrcl 46400 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛)))) ∈
ℝ*) |
| 62 | 61 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) →
(Σ^‘(𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛)))) ∈
ℝ*) |
| 63 | 16 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) → (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛)) ∈
ℝ*) |
| 64 | 55 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) → (1...𝑘) ∈ V) |
| 65 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) ∧ 𝑛 ∈ (1...𝑘)) → 𝜑) |
| 66 | 57 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ) |
| 67 | 65, 66, 20 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) ∧ 𝑛 ∈ (1...𝑘)) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
| 68 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) → 𝑥 ⊆ (1...𝑘)) |
| 69 | 64, 67, 68 | sge0lessmpt 46414 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) →
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛)))) ≤
(Σ^‘(𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛))))) |
| 70 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑂 ∈ OutMeas) |
| 71 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐸:ℕ⟶𝑆) |
| 72 | | caratheodorylem2.5 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 73 | 72 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 74 | | caratheodorylem2.g |
. . . . . . . . . . . . . . 15
⊢ 𝐺 = (𝑘 ∈ ℕ ↦ ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛)) |
| 75 | | nfiu1 5027 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛) |
| 76 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘∪ 𝑚 ∈ (1...𝑛)(𝐸‘𝑚) |
| 77 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚)) |
| 78 | 77 | cbviunv 5040 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛) = ∪ 𝑚 ∈ (1...𝑘)(𝐸‘𝑚) |
| 79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → ∪
𝑛 ∈ (1...𝑘)(𝐸‘𝑛) = ∪ 𝑚 ∈ (1...𝑘)(𝐸‘𝑚)) |
| 80 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (1...𝑘) = (1...𝑛)) |
| 81 | 80 | iuneq1d 5019 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → ∪
𝑚 ∈ (1...𝑘)(𝐸‘𝑚) = ∪ 𝑚 ∈ (1...𝑛)(𝐸‘𝑚)) |
| 82 | 79, 81 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → ∪
𝑛 ∈ (1...𝑘)(𝐸‘𝑛) = ∪ 𝑚 ∈ (1...𝑛)(𝐸‘𝑚)) |
| 83 | 75, 76, 82 | cbvmpt 5253 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ ↦ ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛)) = (𝑛 ∈ ℕ ↦ ∪ 𝑚 ∈ (1...𝑛)(𝐸‘𝑚)) |
| 84 | 74, 83 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ∪ 𝑚 ∈ (1...𝑛)(𝐸‘𝑚)) |
| 85 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ) |
| 86 | 85, 26 | eleqtrdi 2851 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
(ℤ≥‘1)) |
| 87 | 86 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
| 88 | 70, 3, 26, 71, 73, 84, 87 | caratheodorylem1 46541 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑂‘(𝐺‘𝑘)) =
(Σ^‘(𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛))))) |
| 89 | 88 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(Σ^‘(𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛)))) = (𝑂‘(𝐺‘𝑘))) |
| 90 | 15 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∪ 𝑛 ∈ ℕ (𝐸‘𝑛) ⊆ 𝑋) |
| 91 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸‘𝑛) ∈ V |
| 92 | 55, 91 | iunex 7993 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛) ∈ V |
| 93 | 74 | fvmpt2 7027 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛) ∈ V) → (𝐺‘𝑘) = ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛)) |
| 94 | 85, 92, 93 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛)) |
| 95 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ →
(1...𝑘) ⊆
ℕ) |
| 96 | | iunss1 5006 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑘) ⊆
ℕ → ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛) ⊆ ∪
𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛) ⊆ ∪
𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 98 | 94, 97 | eqsstrd 4018 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ⊆ ∪
𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 99 | 98 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ⊆ ∪
𝑛 ∈ ℕ (𝐸‘𝑛)) |
| 100 | 70, 2, 90, 99 | omessle 46513 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑂‘(𝐺‘𝑘)) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 101 | 89, 100 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(Σ^‘(𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛)))) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 102 | 101 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) →
(Σ^‘(𝑛 ∈ (1...𝑘) ↦ (𝑂‘(𝐸‘𝑛)))) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 103 | 54, 62, 63, 69, 102 | xrletrd 13204 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ (1...𝑘)) →
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛)))) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 104 | 103 | 3exp 1120 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑥 ⊆ (1...𝑘) →
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛)))) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))))) |
| 105 | 104 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 ℕ ∩ Fin)) →
(𝑘 ∈ ℕ →
(𝑥 ⊆ (1...𝑘) →
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛)))) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))))) |
| 106 | 105 | rexlimdv 3153 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 ℕ ∩ Fin)) →
(∃𝑘 ∈ ℕ
𝑥 ⊆ (1...𝑘) →
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛)))) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛)))) |
| 107 | 38, 106 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 ℕ ∩ Fin)) →
(Σ^‘(𝑛 ∈ 𝑥 ↦ (𝑂‘(𝐸‘𝑛)))) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 108 | 33, 107 | eqbrtrd 5165 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 ℕ ∩ Fin)) →
(Σ^‘((𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))) ↾ 𝑥)) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 109 | 108 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 ℕ ∩
Fin)(Σ^‘((𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))) ↾ 𝑥)) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 110 | 18, 22, 16 | sge0lefi 46413 |
. . 3
⊢ (𝜑 →
((Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛)))) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛)) ↔ ∀𝑥 ∈ (𝒫 ℕ ∩
Fin)(Σ^‘((𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))) ↾ 𝑥)) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛)))) |
| 111 | 109, 110 | mpbird 257 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛)))) ≤ (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛))) |
| 112 | 16, 23, 29, 111 | xrletrid 13197 |
1
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ ℕ (𝐸‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))))) |