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 41264
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 4231 . . . . . . . . 9 (𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
32adantl 467 . . . . . . . 8 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
4 isomenndlem.f . . . . . . . . . . 11 (𝜑𝐹:𝐵1-1-onto𝑌)
5 f1of 6278 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵𝑌)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵𝑌)
7 ssun1 3927 . . . . . . . . . . 11 𝑌 ⊆ (𝑌 ∪ {∅})
87a1i 11 . . . . . . . . . 10 (𝜑𝑌 ⊆ (𝑌 ∪ {∅}))
96, 8fssd 6197 . . . . . . . . 9 (𝜑𝐹:𝐵⟶(𝑌 ∪ {∅}))
109ffvelrnda 6502 . . . . . . . 8 ((𝜑𝑛𝐵) → (𝐹𝑛) ∈ (𝑌 ∪ {∅}))
113, 10eqeltrd 2850 . . . . . . 7 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
1211adantlr 694 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13 iffalse 4234 . . . . . . . . 9 𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
1413adantl 467 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
15 0ex 4924 . . . . . . . . . . 11 ∅ ∈ V
1615snid 4347 . . . . . . . . . 10 ∅ ∈ {∅}
17 elun2 3932 . . . . . . . . . 10 (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
1816, 17ax-mp 5 . . . . . . . . 9 ∅ ∈ (𝑌 ∪ {∅})
1918a1i 11 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
2014, 19eqeltrd 2850 . . . . . . 7 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2120adantlr 694 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2212, 21pm2.61dan 814 . . . . 5 ((𝜑𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23 isomenndlem.a . . . . 5 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
2422, 23fmptd 6527 . . . 4 (𝜑𝐴:ℕ⟶(𝑌 ∪ {∅}))
25 isomenndlem.y . . . . 5 (𝜑𝑌 ⊆ 𝒫 𝑋)
26 0elpw 4965 . . . . . . 7 ∅ ∈ 𝒫 𝑋
27 snssi 4474 . . . . . . 7 (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
2826, 27ax-mp 5 . . . . . 6 {∅} ⊆ 𝒫 𝑋
2928a1i 11 . . . . 5 (𝜑 → {∅} ⊆ 𝒫 𝑋)
3025, 29unssd 3940 . . . 4 (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
3124, 30fssd 6197 . . 3 (𝜑𝐴:ℕ⟶𝒫 𝑋)
32 nnex 11228 . . . . . 6 ℕ ∈ V
3332mptex 6630 . . . . 5 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) ∈ V
3423, 33eqeltri 2846 . . . 4 𝐴 ∈ V
35 feq1 6166 . . . . . 6 (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋𝐴:ℕ⟶𝒫 𝑋))
3635anbi2d 614 . . . . 5 (𝑎 = 𝐴 → ((𝜑𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑𝐴:ℕ⟶𝒫 𝑋)))
37 fveq1 6331 . . . . . . . 8 (𝑎 = 𝐴 → (𝑎𝑛) = (𝐴𝑛))
3837iuneq2d 4681 . . . . . . 7 (𝑎 = 𝐴 𝑛 ∈ ℕ (𝑎𝑛) = 𝑛 ∈ ℕ (𝐴𝑛))
3938fveq2d 6336 . . . . . 6 (𝑎 = 𝐴 → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
40 simpl 468 . . . . . . . . . 10 ((𝑎 = 𝐴𝑛 ∈ ℕ) → 𝑎 = 𝐴)
4140fveq1d 6334 . . . . . . . . 9 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑎𝑛) = (𝐴𝑛))
4241fveq2d 6336 . . . . . . . 8 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑂‘(𝑎𝑛)) = (𝑂‘(𝐴𝑛)))
4342mpteq2dva 4878 . . . . . . 7 (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))
4443fveq2d 6336 . . . . . 6 (𝑎 = 𝐴 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
4539, 44breq12d 4799 . . . . 5 (𝑎 = 𝐴 → ((𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
4636, 45imbi12d 333 . . . 4 (𝑎 = 𝐴 → (((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))))) ↔ ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))))
47 isomenndlem.subadd . . . 4 ((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))))
4834, 46, 47vtocl 3410 . . 3 ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
491, 31, 48syl2anc 573 . 2 (𝜑 → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
506ad2antrr 705 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵𝑌)
51 simpr 471 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52 id 22 . . . . . . . . . . . . . . 15 (𝐵 = ℕ → 𝐵 = ℕ)
5352eqcomd 2777 . . . . . . . . . . . . . 14 (𝐵 = ℕ → ℕ = 𝐵)
5453adantr 466 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
5551, 54eleqtrd 2852 . . . . . . . . . . . 12 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5655adantll 693 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5750, 56ffvelrnd 6503 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑌)
58 eqid 2771 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ (𝐹𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛))
5957, 58fmptd 6527 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌)
6023a1i 11 . . . . . . . . . . . 12 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)))
6155iftrued 4233 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
6261mpteq2dva 4878 . . . . . . . . . . . 12 (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6360, 62eqtrd 2805 . . . . . . . . . . 11 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6463feq1d 6170 . . . . . . . . . 10 (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6564adantl 467 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6659, 65mpbird 247 . . . . . . . 8 ((𝜑𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67 f1ofo 6285 . . . . . . . . . . . . . . . 16 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵onto𝑌)
684, 67syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐵onto𝑌)
69 dffo3 6517 . . . . . . . . . . . . . . 15 (𝐹:𝐵onto𝑌 ↔ (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7068, 69sylib 208 . . . . . . . . . . . . . 14 (𝜑 → (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7170simprd 483 . . . . . . . . . . . . 13 (𝜑 → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
7271adantr 466 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
73 simpr 471 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → 𝑦𝑌)
74 rspa 3079 . . . . . . . . . . . 12 ((∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7572, 73, 74syl2anc 573 . . . . . . . . . . 11 ((𝜑𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7675adantlr 694 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
77 nfv 1995 . . . . . . . . . . . 12 𝑛(𝜑𝐵 = ℕ)
78 nfre1 3153 . . . . . . . . . . . 12 𝑛𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)
79 simpr 471 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛𝐵)
80 simpl 468 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝐵 = ℕ)
8179, 80eleqtrd 2852 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
8281adantll 693 . . . . . . . . . . . . . . 15 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
83823adant3 1126 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑛 ∈ ℕ)
8460fveq1d 6334 . . . . . . . . . . . . . . . . 17 (𝐵 = ℕ → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
85843ad2ant1 1127 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
86 fvex 6342 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑛) ∈ V
8786, 15ifex 4295 . . . . . . . . . . . . . . . . . . . 20 if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
89 eqid 2771 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
9089fvmpt2 6433 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
9181, 88, 90syl2anc 573 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
922adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
9391, 92eqtrd 2805 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
94933adant3 1126 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
95 id 22 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐹𝑛) → 𝑦 = (𝐹𝑛))
9695eqcomd 2777 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐹𝑛) → (𝐹𝑛) = 𝑦)
97963ad2ant3 1129 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐹𝑛) = 𝑦)
9885, 94, 973eqtrrd 2810 . . . . . . . . . . . . . . 15 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
99983adant1l 1185 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
100 rspe 3151 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10183, 99, 100syl2anc 573 . . . . . . . . . . . . 13 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1021013exp 1112 . . . . . . . . . . . 12 ((𝜑𝐵 = ℕ) → (𝑛𝐵 → (𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
10377, 78, 102rexlimd 3174 . . . . . . . . . . 11 ((𝜑𝐵 = ℕ) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
104103adantr 466 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
10576, 104mpd 15 . . . . . . . . 9 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
106105ralrimiva 3115 . . . . . . . 8 ((𝜑𝐵 = ℕ) → ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10766, 106jca 501 . . . . . . 7 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
108 dffo3 6517 . . . . . . 7 (𝐴:ℕ–onto𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
109107, 108sylibr 224 . . . . . 6 ((𝜑𝐵 = ℕ) → 𝐴:ℕ–onto𝑌)
110 founiiun 39880 . . . . . 6 (𝐴:ℕ–onto𝑌 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
111109, 110syl 17 . . . . 5 ((𝜑𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
112 uniun 4593 . . . . . . . 8 (𝑌 ∪ {∅}) = ( 𝑌 {∅})
11315unisn 4589 . . . . . . . . 9 {∅} = ∅
114113uneq2i 3915 . . . . . . . 8 ( 𝑌 {∅}) = ( 𝑌 ∪ ∅)
115 un0 4111 . . . . . . . 8 ( 𝑌 ∪ ∅) = 𝑌
116112, 114, 1153eqtrri 2798 . . . . . . 7 𝑌 = (𝑌 ∪ {∅})
117116a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = (𝑌 ∪ {∅}))
11824adantr 466 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119 isomenndlem.b . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ ℕ)
120119adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
12152necon3bi 2969 . . . . . . . . . . . . . . . . . 18 𝐵 = ℕ → 𝐵 ≠ ℕ)
122121adantl 467 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
123120, 122jca 501 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
124 df-pss 3739 . . . . . . . . . . . . . . . 16 (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125123, 124sylibr 224 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
126 pssnel 4181 . . . . . . . . . . . . . . 15 (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
127125, 126syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
128127adantr 466 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
129 nfv 1995 . . . . . . . . . . . . . 14 𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
130 simprl 754 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
131 simprl 754 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
13287a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
13323fvmpt2 6433 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
134131, 132, 133syl2anc 573 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
135134adantlr 694 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
13613ad2antll 708 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
137 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ∅ → 𝑦 = ∅)
138137eqcomd 2777 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ∅ → ∅ = 𝑦)
139138ad2antlr 706 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∅ = 𝑦)
140135, 136, 1393eqtrrd 2810 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑦 = (𝐴𝑛))
141130, 140, 100syl2anc 573 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
142141ex 397 . . . . . . . . . . . . . . 15 ((𝜑𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
143142adantlr 694 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
144129, 78, 143exlimd 2243 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → (∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
145128, 144mpd 15 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
146145adantlr 694 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
147 simplll 758 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
148 simpl 468 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
149 elsni 4333 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {∅} → 𝑦 = ∅)
150149con3i 151 . . . . . . . . . . . . . . 15 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
151150adantl 467 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
152 elunnel2 39720 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦𝑌)
153148, 151, 152syl2anc 573 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
154153adantll 693 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
15568adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → 𝐹:𝐵onto𝑌)
156 foelrni 6386 . . . . . . . . . . . . . 14 ((𝐹:𝐵onto𝑌𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
157155, 73, 156syl2anc 573 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
158 nfv 1995 . . . . . . . . . . . . . 14 𝑛(𝜑𝑦𝑌)
159119sselda 3752 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵) → 𝑛 ∈ ℕ)
1601593adant3 1126 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑛 ∈ ℕ)
161159, 87, 133sylancl 574 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛𝐵) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
162161, 3eqtrd 2805 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐵) → (𝐴𝑛) = (𝐹𝑛))
1631623adant3 1126 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐴𝑛) = (𝐹𝑛))
164 simp3 1132 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐹𝑛) = 𝑦)
165163, 164eqtr2d 2806 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑦 = (𝐴𝑛))
166160, 165, 100syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1671663exp 1112 . . . . . . . . . . . . . . 15 (𝜑 → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
168167adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
169158, 78, 168rexlimd 3174 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → (∃𝑛𝐵 (𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
170157, 169mpd 15 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
171147, 154, 170syl2anc 573 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
172146, 171pm2.61dan 814 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
173172ralrimiva 3115 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
174118, 173jca 501 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
175 dffo3 6517 . . . . . . . 8 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
176174, 175sylibr 224 . . . . . . 7 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
177 founiiun 39880 . . . . . . 7 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
178176, 177syl 17 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
179117, 178eqtrd 2805 . . . . 5 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
180111, 179pm2.61dan 814 . . . 4 (𝜑 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
181180fveq2d 6336 . . 3 (𝜑 → (𝑂 𝑌) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
182 uncom 3908 . . . . . . . . 9 ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
183182a1i 11 . . . . . . . 8 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
184 undif 4191 . . . . . . . . 9 (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185119, 184sylib 208 . . . . . . . 8 (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
186183, 185eqtrd 2805 . . . . . . 7 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
187186eqcomd 2777 . . . . . 6 (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
188187mpteq1d 4872 . . . . 5 (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛))))
189188fveq2d 6336 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))))
190 nfv 1995 . . . . 5 𝑛𝜑
191 difexg 4942 . . . . . . 7 (ℕ ∈ V → (ℕ ∖ 𝐵) ∈ V)
19232, 191ax-mp 5 . . . . . 6 (ℕ ∖ 𝐵) ∈ V
193192a1i 11 . . . . 5 (𝜑 → (ℕ ∖ 𝐵) ∈ V)
19432a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
195194, 119ssexd 4939 . . . . 5 (𝜑𝐵 ∈ V)
196 incom 3956 . . . . . . 7 ((ℕ ∖ 𝐵) ∩ 𝐵) = (𝐵 ∩ (ℕ ∖ 𝐵))
197 disjdif 4182 . . . . . . 7 (𝐵 ∩ (ℕ ∖ 𝐵)) = ∅
198196, 197eqtri 2793 . . . . . 6 ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
199198a1i 11 . . . . 5 (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
200 simpl 468 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
201 eldifi 3883 . . . . . . 7 (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
202201adantl 467 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
203 isomenndlem.o . . . . . . . 8 (𝜑𝑂:𝒫 𝑋⟶(0[,]+∞))
204203adantr 466 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
20531ffvelrnda 6502 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 𝑋)
206204, 205ffvelrnd 6503 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
207200, 202, 206syl2anc 573 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
208159, 206syldan 579 . . . . 5 ((𝜑𝑛𝐵) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
209190, 193, 195, 199, 207, 208sge0splitmpt 41145 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
210 eqid 2771 . . . . . . . 8 (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))) = (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))
211208, 210fmptd 6527 . . . . . . 7 (𝜑 → (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))):𝐵⟶(0[,]+∞))
212195, 211sge0xrcl 41119 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) ∈ ℝ*)
213212xaddid2d 40051 . . . . 5 (𝜑 → (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
21487a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
215202, 214, 133syl2anc 573 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
216 eldifn 3884 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛𝐵)
217216adantl 467 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛𝐵)
218217iffalsed 4236 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
219215, 218eqtrd 2805 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = ∅)
220219fveq2d 6336 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = (𝑂‘∅))
221 isomenndlem.o0 . . . . . . . . . . 11 (𝜑 → (𝑂‘∅) = 0)
222200, 221syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
223220, 222eqtrd 2805 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = 0)
224223mpteq2dva 4878 . . . . . . . 8 (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
225224fveq2d 6336 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
226190, 193sge0z 41109 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
227225, 226eqtrd 2805 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = 0)
228227oveq1d 6808 . . . . 5 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
229203, 25feqresmpt 6392 . . . . . . 7 (𝜑 → (𝑂𝑌) = (𝑦𝑌 ↦ (𝑂𝑦)))
230229fveq2d 6336 . . . . . 6 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))))
231 nfv 1995 . . . . . . 7 𝑦𝜑
232 fveq2 6332 . . . . . . 7 (𝑦 = (𝐴𝑛) → (𝑂𝑦) = (𝑂‘(𝐴𝑛)))
233162eqcomd 2777 . . . . . . 7 ((𝜑𝑛𝐵) → (𝐹𝑛) = (𝐴𝑛))
234203adantr 466 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
23525sselda 3752 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑦 ∈ 𝒫 𝑋)
236234, 235ffvelrnd 6503 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑂𝑦) ∈ (0[,]+∞))
237231, 190, 232, 195, 4, 233, 236sge0f1o 41116 . . . . . 6 (𝜑 → (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
238 eqidd 2772 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
239230, 237, 2383eqtrd 2809 . . . . 5 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
240213, 228, 2393eqtr4d 2815 . . . 4 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑂𝑌)))
241189, 209, 2403eqtrrd 2810 . . 3 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
242181, 241breq12d 4799 . 2 (𝜑 → ((𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
24349, 242mpbird 247 1 (𝜑 → (𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351  cdif 3720  cun 3721  cin 3722  wss 3723  wpss 3724  c0 4063  ifcif 4225  𝒫 cpw 4297  {csn 4316   cuni 4574   ciun 4654   class class class wbr 4786  cmpt 4863  cres 5251  wf 6027  ontowfo 6029  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6793  0cc0 10138  +∞cpnf 10273  cle 10277  cn 11222   +𝑒 cxad 12149  [,]cicc 12383  Σ^csumge0 41096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-oi 8571  df-card 8965  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-rp 12036  df-xadd 12152  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-sum 14625  df-sumge0 41097
This theorem is referenced by:  isomennd  41265
  Copyright terms: Public domain W3C validator