Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isomenndlem Structured version   Visualization version   GIF version

Theorem isomenndlem 41227
Description: 𝑂 is sub-additive w.r.t. countable indexed union, implies that 𝑂 is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Hypotheses
Ref Expression
isomenndlem.o (𝜑𝑂:𝒫 𝑋⟶(0[,]+∞))
isomenndlem.o0 (𝜑 → (𝑂‘∅) = 0)
isomenndlem.y (𝜑𝑌 ⊆ 𝒫 𝑋)
isomenndlem.subadd ((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))))
isomenndlem.b (𝜑𝐵 ⊆ ℕ)
isomenndlem.f (𝜑𝐹:𝐵1-1-onto𝑌)
isomenndlem.a 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
Assertion
Ref Expression
isomenndlem (𝜑 → (𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)))
Distinct variable groups:   𝐴,𝑎,𝑛   𝐵,𝑛   𝑛,𝐹   𝑂,𝑎,𝑛   𝑋,𝑎   𝑛,𝑌   𝜑,𝑎,𝑛
Allowed substitution hints:   𝐵(𝑎)   𝐹(𝑎)   𝑋(𝑛)   𝑌(𝑎)

Proof of Theorem isomenndlem
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 id 22 . . 3 (𝜑𝜑)
2 iftrue 4292 . . . . . . . . 9 (𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
32adantl 469 . . . . . . . 8 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
4 isomenndlem.f . . . . . . . . . . 11 (𝜑𝐹:𝐵1-1-onto𝑌)
5 f1of 6356 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵𝑌)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵𝑌)
7 ssun1 3982 . . . . . . . . . . 11 𝑌 ⊆ (𝑌 ∪ {∅})
87a1i 11 . . . . . . . . . 10 (𝜑𝑌 ⊆ (𝑌 ∪ {∅}))
96, 8fssd 6273 . . . . . . . . 9 (𝜑𝐹:𝐵⟶(𝑌 ∪ {∅}))
109ffvelrnda 6584 . . . . . . . 8 ((𝜑𝑛𝐵) → (𝐹𝑛) ∈ (𝑌 ∪ {∅}))
113, 10eqeltrd 2892 . . . . . . 7 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
1211adantlr 697 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13 iffalse 4295 . . . . . . . . 9 𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
1413adantl 469 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
15 0ex 4991 . . . . . . . . . . 11 ∅ ∈ V
1615snid 4409 . . . . . . . . . 10 ∅ ∈ {∅}
17 elun2 3987 . . . . . . . . . 10 (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
1816, 17ax-mp 5 . . . . . . . . 9 ∅ ∈ (𝑌 ∪ {∅})
1918a1i 11 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
2014, 19eqeltrd 2892 . . . . . . 7 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2120adantlr 697 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2212, 21pm2.61dan 838 . . . . 5 ((𝜑𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23 isomenndlem.a . . . . 5 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
2422, 23fmptd 6609 . . . 4 (𝜑𝐴:ℕ⟶(𝑌 ∪ {∅}))
25 isomenndlem.y . . . . 5 (𝜑𝑌 ⊆ 𝒫 𝑋)
26 0elpw 5033 . . . . . . 7 ∅ ∈ 𝒫 𝑋
27 snssi 4536 . . . . . . 7 (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
2826, 27ax-mp 5 . . . . . 6 {∅} ⊆ 𝒫 𝑋
2928a1i 11 . . . . 5 (𝜑 → {∅} ⊆ 𝒫 𝑋)
3025, 29unssd 3995 . . . 4 (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
3124, 30fssd 6273 . . 3 (𝜑𝐴:ℕ⟶𝒫 𝑋)
32 nnex 11314 . . . . . 6 ℕ ∈ V
3332mptex 6714 . . . . 5 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) ∈ V
3423, 33eqeltri 2888 . . . 4 𝐴 ∈ V
35 feq1 6240 . . . . . 6 (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋𝐴:ℕ⟶𝒫 𝑋))
3635anbi2d 616 . . . . 5 (𝑎 = 𝐴 → ((𝜑𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑𝐴:ℕ⟶𝒫 𝑋)))
37 fveq1 6410 . . . . . . . 8 (𝑎 = 𝐴 → (𝑎𝑛) = (𝐴𝑛))
3837iuneq2d 4746 . . . . . . 7 (𝑎 = 𝐴 𝑛 ∈ ℕ (𝑎𝑛) = 𝑛 ∈ ℕ (𝐴𝑛))
3938fveq2d 6415 . . . . . 6 (𝑎 = 𝐴 → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
40 simpl 470 . . . . . . . . . 10 ((𝑎 = 𝐴𝑛 ∈ ℕ) → 𝑎 = 𝐴)
4140fveq1d 6413 . . . . . . . . 9 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑎𝑛) = (𝐴𝑛))
4241fveq2d 6415 . . . . . . . 8 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑂‘(𝑎𝑛)) = (𝑂‘(𝐴𝑛)))
4342mpteq2dva 4945 . . . . . . 7 (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))
4443fveq2d 6415 . . . . . 6 (𝑎 = 𝐴 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
4539, 44breq12d 4864 . . . . 5 (𝑎 = 𝐴 → ((𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
4636, 45imbi12d 335 . . . 4 (𝑎 = 𝐴 → (((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))))) ↔ ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))))
47 isomenndlem.subadd . . . 4 ((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))))
4834, 46, 47vtocl 3459 . . 3 ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
491, 31, 48syl2anc 575 . 2 (𝜑 → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
506ad2antrr 708 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵𝑌)
51 simpr 473 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52 id 22 . . . . . . . . . . . . . . 15 (𝐵 = ℕ → 𝐵 = ℕ)
5352eqcomd 2819 . . . . . . . . . . . . . 14 (𝐵 = ℕ → ℕ = 𝐵)
5453adantr 468 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
5551, 54eleqtrd 2894 . . . . . . . . . . . 12 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5655adantll 696 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5750, 56ffvelrnd 6585 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑌)
58 eqid 2813 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ (𝐹𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛))
5957, 58fmptd 6609 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌)
6023a1i 11 . . . . . . . . . . . 12 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)))
6155iftrued 4294 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
6261mpteq2dva 4945 . . . . . . . . . . . 12 (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6360, 62eqtrd 2847 . . . . . . . . . . 11 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6463feq1d 6244 . . . . . . . . . 10 (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6564adantl 469 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6659, 65mpbird 248 . . . . . . . 8 ((𝜑𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67 f1ofo 6363 . . . . . . . . . . . . . . . 16 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵onto𝑌)
684, 67syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐵onto𝑌)
69 dffo3 6599 . . . . . . . . . . . . . . 15 (𝐹:𝐵onto𝑌 ↔ (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7068, 69sylib 209 . . . . . . . . . . . . . 14 (𝜑 → (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7170simprd 485 . . . . . . . . . . . . 13 (𝜑 → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
7271adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
73 simpr 473 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → 𝑦𝑌)
74 rspa 3125 . . . . . . . . . . . 12 ((∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7572, 73, 74syl2anc 575 . . . . . . . . . . 11 ((𝜑𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7675adantlr 697 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
77 nfv 2005 . . . . . . . . . . . 12 𝑛(𝜑𝐵 = ℕ)
78 nfre1 3199 . . . . . . . . . . . 12 𝑛𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)
79 simpr 473 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛𝐵)
80 simpl 470 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝐵 = ℕ)
8179, 80eleqtrd 2894 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
8281adantll 696 . . . . . . . . . . . . . . 15 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
83823adant3 1155 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑛 ∈ ℕ)
8460fveq1d 6413 . . . . . . . . . . . . . . . . 17 (𝐵 = ℕ → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
85843ad2ant1 1156 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
86 fvex 6424 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑛) ∈ V
8786, 15ifex 4334 . . . . . . . . . . . . . . . . . . . 20 if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
89 eqid 2813 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
9089fvmpt2 6515 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
9181, 88, 90syl2anc 575 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
922adantl 469 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
9391, 92eqtrd 2847 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
94933adant3 1155 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
95 id 22 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐹𝑛) → 𝑦 = (𝐹𝑛))
9695eqcomd 2819 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐹𝑛) → (𝐹𝑛) = 𝑦)
97963ad2ant3 1158 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐹𝑛) = 𝑦)
9885, 94, 973eqtrrd 2852 . . . . . . . . . . . . . . 15 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
99983adant1l 1214 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
100 rspe 3197 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10183, 99, 100syl2anc 575 . . . . . . . . . . . . 13 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1021013exp 1141 . . . . . . . . . . . 12 ((𝜑𝐵 = ℕ) → (𝑛𝐵 → (𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
10377, 78, 102rexlimd 3221 . . . . . . . . . . 11 ((𝜑𝐵 = ℕ) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
104103adantr 468 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
10576, 104mpd 15 . . . . . . . . 9 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
106105ralrimiva 3161 . . . . . . . 8 ((𝜑𝐵 = ℕ) → ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10766, 106jca 503 . . . . . . 7 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
108 dffo3 6599 . . . . . . 7 (𝐴:ℕ–onto𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
109107, 108sylibr 225 . . . . . 6 ((𝜑𝐵 = ℕ) → 𝐴:ℕ–onto𝑌)
110 founiiun 39850 . . . . . 6 (𝐴:ℕ–onto𝑌 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
111109, 110syl 17 . . . . 5 ((𝜑𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
112 uniun 4658 . . . . . . . 8 (𝑌 ∪ {∅}) = ( 𝑌 {∅})
11315unisn 4653 . . . . . . . . 9 {∅} = ∅
114113uneq2i 3970 . . . . . . . 8 ( 𝑌 {∅}) = ( 𝑌 ∪ ∅)
115 un0 4172 . . . . . . . 8 ( 𝑌 ∪ ∅) = 𝑌
116112, 114, 1153eqtrri 2840 . . . . . . 7 𝑌 = (𝑌 ∪ {∅})
117116a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = (𝑌 ∪ {∅}))
11824adantr 468 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119 nfv 2005 . . . . . . . . . . . . 13 𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
120 isomenndlem.b . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ ℕ)
121120adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
12252necon3bi 3011 . . . . . . . . . . . . . . . . . 18 𝐵 = ℕ → 𝐵 ≠ ℕ)
123122adantl 469 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
124121, 123jca 503 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125 df-pss 3792 . . . . . . . . . . . . . . . 16 (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
126124, 125sylibr 225 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
127 pssnel 4242 . . . . . . . . . . . . . . 15 (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
128126, 127syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
129128adantr 468 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
130 simprl 778 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
131 simprl 778 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
13287a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
13323fvmpt2 6515 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
134131, 132, 133syl2anc 575 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
135134adantlr 697 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
13613ad2antll 711 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
137 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ∅ → 𝑦 = ∅)
138137eqcomd 2819 . . . . . . . . . . . . . . . . . 18 (𝑦 = ∅ → ∅ = 𝑦)
139138ad2antlr 709 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∅ = 𝑦)
140135, 136, 1393eqtrrd 2852 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑦 = (𝐴𝑛))
141130, 140, 100syl2anc 575 . . . . . . . . . . . . . . 15 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
142141ex 399 . . . . . . . . . . . . . 14 ((𝜑𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
143142adantlr 697 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
144119, 78, 129, 143exlimimdd 2257 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
145144adantlr 697 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
146 simplll 782 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
147 simpl 470 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
148 elsni 4394 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {∅} → 𝑦 = ∅)
149148con3i 151 . . . . . . . . . . . . . . 15 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
150149adantl 469 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
151 elunnel2 39693 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦𝑌)
152147, 150, 151syl2anc 575 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
153152adantll 696 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
15468adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → 𝐹:𝐵onto𝑌)
155 foelrni 6468 . . . . . . . . . . . . . 14 ((𝐹:𝐵onto𝑌𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
156154, 73, 155syl2anc 575 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
157 nfv 2005 . . . . . . . . . . . . . 14 𝑛(𝜑𝑦𝑌)
158120sselda 3805 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵) → 𝑛 ∈ ℕ)
1591583adant3 1155 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑛 ∈ ℕ)
160158, 87, 133sylancl 576 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛𝐵) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
161160, 3eqtrd 2847 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐵) → (𝐴𝑛) = (𝐹𝑛))
1621613adant3 1155 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐴𝑛) = (𝐹𝑛))
163 simp3 1161 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐹𝑛) = 𝑦)
164162, 163eqtr2d 2848 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑦 = (𝐴𝑛))
165159, 164, 100syl2anc 575 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1661653exp 1141 . . . . . . . . . . . . . . 15 (𝜑 → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
167166adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
168157, 78, 167rexlimd 3221 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → (∃𝑛𝐵 (𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
169156, 168mpd 15 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
170146, 153, 169syl2anc 575 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
171145, 170pm2.61dan 838 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
172171ralrimiva 3161 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
173118, 172jca 503 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
174 dffo3 6599 . . . . . . . 8 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
175173, 174sylibr 225 . . . . . . 7 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
176 founiiun 39850 . . . . . . 7 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
177175, 176syl 17 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
178117, 177eqtrd 2847 . . . . 5 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
179111, 178pm2.61dan 838 . . . 4 (𝜑 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
180179fveq2d 6415 . . 3 (𝜑 → (𝑂 𝑌) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
181 uncom 3963 . . . . . . . . 9 ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
182181a1i 11 . . . . . . . 8 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
183 undif 4252 . . . . . . . . 9 (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
184120, 183sylib 209 . . . . . . . 8 (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185182, 184eqtrd 2847 . . . . . . 7 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
186185eqcomd 2819 . . . . . 6 (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
187186mpteq1d 4939 . . . . 5 (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛))))
188187fveq2d 6415 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))))
189 nfv 2005 . . . . 5 𝑛𝜑
190 difexg 5010 . . . . . . 7 (ℕ ∈ V → (ℕ ∖ 𝐵) ∈ V)
19132, 190ax-mp 5 . . . . . 6 (ℕ ∖ 𝐵) ∈ V
192191a1i 11 . . . . 5 (𝜑 → (ℕ ∖ 𝐵) ∈ V)
19332a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
194193, 120ssexd 5007 . . . . 5 (𝜑𝐵 ∈ V)
195 incom 4011 . . . . . . 7 ((ℕ ∖ 𝐵) ∩ 𝐵) = (𝐵 ∩ (ℕ ∖ 𝐵))
196 disjdif 4243 . . . . . . 7 (𝐵 ∩ (ℕ ∖ 𝐵)) = ∅
197195, 196eqtri 2835 . . . . . 6 ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
198197a1i 11 . . . . 5 (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
199 simpl 470 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
200 eldifi 3938 . . . . . . 7 (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
201200adantl 469 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
202 isomenndlem.o . . . . . . . 8 (𝜑𝑂:𝒫 𝑋⟶(0[,]+∞))
203202adantr 468 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
20431ffvelrnda 6584 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 𝑋)
205203, 204ffvelrnd 6585 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
206199, 201, 205syl2anc 575 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
207158, 205syldan 581 . . . . 5 ((𝜑𝑛𝐵) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
208189, 192, 194, 198, 206, 207sge0splitmpt 41108 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
209 eqid 2813 . . . . . . . 8 (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))) = (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))
210207, 209fmptd 6609 . . . . . . 7 (𝜑 → (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))):𝐵⟶(0[,]+∞))
211194, 210sge0xrcl 41082 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) ∈ ℝ*)
212211xaddid2d 40016 . . . . 5 (𝜑 → (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
21387a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
214201, 213, 133syl2anc 575 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
215 eldifn 3939 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛𝐵)
216215adantl 469 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛𝐵)
217216iffalsed 4297 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
218214, 217eqtrd 2847 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = ∅)
219218fveq2d 6415 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = (𝑂‘∅))
220 isomenndlem.o0 . . . . . . . . . . 11 (𝜑 → (𝑂‘∅) = 0)
221199, 220syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
222219, 221eqtrd 2847 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = 0)
223222mpteq2dva 4945 . . . . . . . 8 (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
224223fveq2d 6415 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
225189, 192sge0z 41072 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
226224, 225eqtrd 2847 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = 0)
227226oveq1d 6892 . . . . 5 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
228202, 25feqresmpt 6474 . . . . . . 7 (𝜑 → (𝑂𝑌) = (𝑦𝑌 ↦ (𝑂𝑦)))
229228fveq2d 6415 . . . . . 6 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))))
230 nfv 2005 . . . . . . 7 𝑦𝜑
231 fveq2 6411 . . . . . . 7 (𝑦 = (𝐴𝑛) → (𝑂𝑦) = (𝑂‘(𝐴𝑛)))
232161eqcomd 2819 . . . . . . 7 ((𝜑𝑛𝐵) → (𝐹𝑛) = (𝐴𝑛))
233202adantr 468 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
23425sselda 3805 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑦 ∈ 𝒫 𝑋)
235233, 234ffvelrnd 6585 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑂𝑦) ∈ (0[,]+∞))
236230, 189, 231, 194, 4, 232, 235sge0f1o 41079 . . . . . 6 (𝜑 → (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
237 eqidd 2814 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
238229, 236, 2373eqtrd 2851 . . . . 5 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
239212, 227, 2383eqtr4d 2857 . . . 4 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑂𝑌)))
240188, 208, 2393eqtrrd 2852 . . 3 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
241180, 240breq12d 4864 . 2 (𝜑 → ((𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
24249, 241mpbird 248 1 (𝜑 → (𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2157  wne 2985  wral 3103  wrex 3104  Vcvv 3398  cdif 3773  cun 3774  cin 3775  wss 3776  wpss 3777  c0 4123  ifcif 4286  𝒫 cpw 4358  {csn 4377   cuni 4637   ciun 4719   class class class wbr 4851  cmpt 4930  cres 5320  wf 6100  ontowfo 6102  1-1-ontowf1o 6103  cfv 6104  (class class class)co 6877  0cc0 10224  +∞cpnf 10359  cle 10363  cn 11308   +𝑒 cxad 12163  [,]cicc 12399  Σ^csumge0 41059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-oadd 7803  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-sup 8590  df-oi 8657  df-card 9051  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-3 11368  df-n0 11563  df-z 11647  df-uz 11908  df-rp 12050  df-xadd 12166  df-ico 12402  df-icc 12403  df-fz 12553  df-fzo 12693  df-seq 13028  df-exp 13087  df-hash 13341  df-cj 14065  df-re 14066  df-im 14067  df-sqrt 14201  df-abs 14202  df-clim 14445  df-sum 14643  df-sumge0 41060
This theorem is referenced by:  isomennd  41228
  Copyright terms: Public domain W3C validator