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 42243
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 4350 . . . . . . . . 9 (𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
32adantl 474 . . . . . . . 8 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
4 isomenndlem.f . . . . . . . . . . 11 (𝜑𝐹:𝐵1-1-onto𝑌)
5 f1of 6438 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵𝑌)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵𝑌)
7 ssun1 4031 . . . . . . . . . . 11 𝑌 ⊆ (𝑌 ∪ {∅})
87a1i 11 . . . . . . . . . 10 (𝜑𝑌 ⊆ (𝑌 ∪ {∅}))
96, 8fssd 6352 . . . . . . . . 9 (𝜑𝐹:𝐵⟶(𝑌 ∪ {∅}))
109ffvelrnda 6670 . . . . . . . 8 ((𝜑𝑛𝐵) → (𝐹𝑛) ∈ (𝑌 ∪ {∅}))
113, 10eqeltrd 2860 . . . . . . 7 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
1211adantlr 702 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13 iffalse 4353 . . . . . . . . 9 𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
1413adantl 474 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
15 0ex 5062 . . . . . . . . . . 11 ∅ ∈ V
1615snid 4467 . . . . . . . . . 10 ∅ ∈ {∅}
17 elun2 4036 . . . . . . . . . 10 (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
1816, 17ax-mp 5 . . . . . . . . 9 ∅ ∈ (𝑌 ∪ {∅})
1918a1i 11 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
2014, 19eqeltrd 2860 . . . . . . 7 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2120adantlr 702 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2212, 21pm2.61dan 800 . . . . 5 ((𝜑𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23 isomenndlem.a . . . . 5 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
2422, 23fmptd 6695 . . . 4 (𝜑𝐴:ℕ⟶(𝑌 ∪ {∅}))
25 isomenndlem.y . . . . 5 (𝜑𝑌 ⊆ 𝒫 𝑋)
26 0elpw 5104 . . . . . . 7 ∅ ∈ 𝒫 𝑋
27 snssi 4609 . . . . . . 7 (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
2826, 27ax-mp 5 . . . . . 6 {∅} ⊆ 𝒫 𝑋
2928a1i 11 . . . . 5 (𝜑 → {∅} ⊆ 𝒫 𝑋)
3025, 29unssd 4044 . . . 4 (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
3124, 30fssd 6352 . . 3 (𝜑𝐴:ℕ⟶𝒫 𝑋)
32 nnex 11440 . . . . . 6 ℕ ∈ V
3332mptex 6806 . . . . 5 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) ∈ V
3423, 33eqeltri 2856 . . . 4 𝐴 ∈ V
35 feq1 6319 . . . . . 6 (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋𝐴:ℕ⟶𝒫 𝑋))
3635anbi2d 619 . . . . 5 (𝑎 = 𝐴 → ((𝜑𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑𝐴:ℕ⟶𝒫 𝑋)))
37 fveq1 6492 . . . . . . . 8 (𝑎 = 𝐴 → (𝑎𝑛) = (𝐴𝑛))
3837iuneq2d 4814 . . . . . . 7 (𝑎 = 𝐴 𝑛 ∈ ℕ (𝑎𝑛) = 𝑛 ∈ ℕ (𝐴𝑛))
3938fveq2d 6497 . . . . . 6 (𝑎 = 𝐴 → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
40 simpl 475 . . . . . . . . . 10 ((𝑎 = 𝐴𝑛 ∈ ℕ) → 𝑎 = 𝐴)
4140fveq1d 6495 . . . . . . . . 9 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑎𝑛) = (𝐴𝑛))
4241fveq2d 6497 . . . . . . . 8 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑂‘(𝑎𝑛)) = (𝑂‘(𝐴𝑛)))
4342mpteq2dva 5016 . . . . . . 7 (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))
4443fveq2d 6497 . . . . . 6 (𝑎 = 𝐴 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
4539, 44breq12d 4936 . . . . 5 (𝑎 = 𝐴 → ((𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
4636, 45imbi12d 337 . . . 4 (𝑎 = 𝐴 → (((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))))) ↔ ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))))
47 isomenndlem.subadd . . . 4 ((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))))
4834, 46, 47vtocl 3472 . . 3 ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
491, 31, 48syl2anc 576 . 2 (𝜑 → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
506ad2antrr 713 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵𝑌)
51 simpr 477 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52 id 22 . . . . . . . . . . . . . . 15 (𝐵 = ℕ → 𝐵 = ℕ)
5352eqcomd 2778 . . . . . . . . . . . . . 14 (𝐵 = ℕ → ℕ = 𝐵)
5453adantr 473 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
5551, 54eleqtrd 2862 . . . . . . . . . . . 12 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5655adantll 701 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5750, 56ffvelrnd 6671 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑌)
58 eqid 2772 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ (𝐹𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛))
5957, 58fmptd 6695 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌)
6023a1i 11 . . . . . . . . . . . 12 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)))
6155iftrued 4352 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
6261mpteq2dva 5016 . . . . . . . . . . . 12 (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6360, 62eqtrd 2808 . . . . . . . . . . 11 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6463feq1d 6323 . . . . . . . . . 10 (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6564adantl 474 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6659, 65mpbird 249 . . . . . . . 8 ((𝜑𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67 f1ofo 6445 . . . . . . . . . . . . . . . 16 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵onto𝑌)
684, 67syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐵onto𝑌)
69 dffo3 6685 . . . . . . . . . . . . . . 15 (𝐹:𝐵onto𝑌 ↔ (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7068, 69sylib 210 . . . . . . . . . . . . . 14 (𝜑 → (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7170simprd 488 . . . . . . . . . . . . 13 (𝜑 → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
7271adantr 473 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
73 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → 𝑦𝑌)
74 rspa 3150 . . . . . . . . . . . 12 ((∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7572, 73, 74syl2anc 576 . . . . . . . . . . 11 ((𝜑𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7675adantlr 702 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
77 nfv 1873 . . . . . . . . . . . 12 𝑛(𝜑𝐵 = ℕ)
78 nfre1 3245 . . . . . . . . . . . 12 𝑛𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)
79 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛𝐵)
80 simpl 475 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝐵 = ℕ)
8179, 80eleqtrd 2862 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
8281adantll 701 . . . . . . . . . . . . . . 15 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
83823adant3 1112 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑛 ∈ ℕ)
8460fveq1d 6495 . . . . . . . . . . . . . . . . 17 (𝐵 = ℕ → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
85843ad2ant1 1113 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
86 fvex 6506 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑛) ∈ V
8786, 15ifex 4392 . . . . . . . . . . . . . . . . . . . 20 if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
89 eqid 2772 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
9089fvmpt2 6599 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
9181, 88, 90syl2anc 576 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
922adantl 474 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
9391, 92eqtrd 2808 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
94933adant3 1112 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
95 id 22 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐹𝑛) → 𝑦 = (𝐹𝑛))
9695eqcomd 2778 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐹𝑛) → (𝐹𝑛) = 𝑦)
97963ad2ant3 1115 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐹𝑛) = 𝑦)
9885, 94, 973eqtrrd 2813 . . . . . . . . . . . . . . 15 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
99983adant1l 1156 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
100 rspe 3243 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10183, 99, 100syl2anc 576 . . . . . . . . . . . . 13 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1021013exp 1099 . . . . . . . . . . . 12 ((𝜑𝐵 = ℕ) → (𝑛𝐵 → (𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
10377, 78, 102rexlimd 3254 . . . . . . . . . . 11 ((𝜑𝐵 = ℕ) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
104103adantr 473 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
10576, 104mpd 15 . . . . . . . . 9 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
106105ralrimiva 3126 . . . . . . . 8 ((𝜑𝐵 = ℕ) → ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10766, 106jca 504 . . . . . . 7 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
108 dffo3 6685 . . . . . . 7 (𝐴:ℕ–onto𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
109107, 108sylibr 226 . . . . . 6 ((𝜑𝐵 = ℕ) → 𝐴:ℕ–onto𝑌)
110 founiiun 40859 . . . . . 6 (𝐴:ℕ–onto𝑌 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
111109, 110syl 17 . . . . 5 ((𝜑𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
112 uniun 4725 . . . . . . . 8 (𝑌 ∪ {∅}) = ( 𝑌 {∅})
11315unisn 4722 . . . . . . . . 9 {∅} = ∅
114113uneq2i 4019 . . . . . . . 8 ( 𝑌 {∅}) = ( 𝑌 ∪ ∅)
115 un0 4224 . . . . . . . 8 ( 𝑌 ∪ ∅) = 𝑌
116112, 114, 1153eqtrri 2801 . . . . . . 7 𝑌 = (𝑌 ∪ {∅})
117116a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = (𝑌 ∪ {∅}))
11824adantr 473 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119 nfv 1873 . . . . . . . . . . . . 13 𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
120 isomenndlem.b . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ ℕ)
121120adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
12252necon3bi 2987 . . . . . . . . . . . . . . . . . 18 𝐵 = ℕ → 𝐵 ≠ ℕ)
123122adantl 474 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
124121, 123jca 504 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125 df-pss 3839 . . . . . . . . . . . . . . . 16 (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
126124, 125sylibr 226 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
127 pssnel 4297 . . . . . . . . . . . . . . 15 (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
128126, 127syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
129128adantr 473 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
130 simprl 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
131 simprl 758 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
13287a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
13323fvmpt2 6599 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
134131, 132, 133syl2anc 576 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
135134adantlr 702 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
13613ad2antll 716 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
137 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ∅ → 𝑦 = ∅)
138137eqcomd 2778 . . . . . . . . . . . . . . . . . 18 (𝑦 = ∅ → ∅ = 𝑦)
139138ad2antlr 714 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∅ = 𝑦)
140135, 136, 1393eqtrrd 2813 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑦 = (𝐴𝑛))
141130, 140, 100syl2anc 576 . . . . . . . . . . . . . . 15 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
142141ex 405 . . . . . . . . . . . . . 14 ((𝜑𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
143142adantlr 702 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
144119, 78, 129, 143exlimimdd 2149 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
145144adantlr 702 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
146 simplll 762 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
147 simpl 475 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
148 elsni 4452 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {∅} → 𝑦 = ∅)
149148con3i 152 . . . . . . . . . . . . . . 15 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
150149adantl 474 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
151 elunnel2 40715 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦𝑌)
152147, 150, 151syl2anc 576 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
153152adantll 701 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
15468adantr 473 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → 𝐹:𝐵onto𝑌)
155 foelrni 6551 . . . . . . . . . . . . . 14 ((𝐹:𝐵onto𝑌𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
156154, 73, 155syl2anc 576 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
157 nfv 1873 . . . . . . . . . . . . . 14 𝑛(𝜑𝑦𝑌)
158120sselda 3852 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵) → 𝑛 ∈ ℕ)
1591583adant3 1112 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑛 ∈ ℕ)
160158, 87, 133sylancl 577 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛𝐵) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
161160, 3eqtrd 2808 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐵) → (𝐴𝑛) = (𝐹𝑛))
1621613adant3 1112 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐴𝑛) = (𝐹𝑛))
163 simp3 1118 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐹𝑛) = 𝑦)
164162, 163eqtr2d 2809 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑦 = (𝐴𝑛))
165159, 164, 100syl2anc 576 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1661653exp 1099 . . . . . . . . . . . . . . 15 (𝜑 → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
167166adantr 473 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
168157, 78, 167rexlimd 3254 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → (∃𝑛𝐵 (𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
169156, 168mpd 15 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
170146, 153, 169syl2anc 576 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
171145, 170pm2.61dan 800 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
172171ralrimiva 3126 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
173118, 172jca 504 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
174 dffo3 6685 . . . . . . . 8 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
175173, 174sylibr 226 . . . . . . 7 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
176 founiiun 40859 . . . . . . 7 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
177175, 176syl 17 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
178117, 177eqtrd 2808 . . . . 5 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
179111, 178pm2.61dan 800 . . . 4 (𝜑 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
180179fveq2d 6497 . . 3 (𝜑 → (𝑂 𝑌) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
181 uncom 4012 . . . . . . . . 9 ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
182181a1i 11 . . . . . . . 8 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
183 undif 4307 . . . . . . . . 9 (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
184120, 183sylib 210 . . . . . . . 8 (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185182, 184eqtrd 2808 . . . . . . 7 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
186185eqcomd 2778 . . . . . 6 (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
187186mpteq1d 5010 . . . . 5 (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛))))
188187fveq2d 6497 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))))
189 nfv 1873 . . . . 5 𝑛𝜑
190 difexg 5081 . . . . . . 7 (ℕ ∈ V → (ℕ ∖ 𝐵) ∈ V)
19132, 190ax-mp 5 . . . . . 6 (ℕ ∖ 𝐵) ∈ V
192191a1i 11 . . . . 5 (𝜑 → (ℕ ∖ 𝐵) ∈ V)
19332a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
194193, 120ssexd 5078 . . . . 5 (𝜑𝐵 ∈ V)
195 incom 4060 . . . . . . 7 ((ℕ ∖ 𝐵) ∩ 𝐵) = (𝐵 ∩ (ℕ ∖ 𝐵))
196 disjdif 4298 . . . . . . 7 (𝐵 ∩ (ℕ ∖ 𝐵)) = ∅
197195, 196eqtri 2796 . . . . . 6 ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
198197a1i 11 . . . . 5 (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
199 simpl 475 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
200 eldifi 3987 . . . . . . 7 (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
201200adantl 474 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
202 isomenndlem.o . . . . . . . 8 (𝜑𝑂:𝒫 𝑋⟶(0[,]+∞))
203202adantr 473 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
20431ffvelrnda 6670 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 𝑋)
205203, 204ffvelrnd 6671 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
206199, 201, 205syl2anc 576 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
207158, 205syldan 582 . . . . 5 ((𝜑𝑛𝐵) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
208189, 192, 194, 198, 206, 207sge0splitmpt 42124 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
209 eqid 2772 . . . . . . . 8 (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))) = (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))
210207, 209fmptd 6695 . . . . . . 7 (𝜑 → (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))):𝐵⟶(0[,]+∞))
211194, 210sge0xrcl 42098 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) ∈ ℝ*)
212211xaddid2d 41016 . . . . 5 (𝜑 → (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
21387a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
214201, 213, 133syl2anc 576 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
215 eldifn 3988 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛𝐵)
216215adantl 474 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛𝐵)
217216iffalsed 4355 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
218214, 217eqtrd 2808 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = ∅)
219218fveq2d 6497 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = (𝑂‘∅))
220 isomenndlem.o0 . . . . . . . . . . 11 (𝜑 → (𝑂‘∅) = 0)
221199, 220syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
222219, 221eqtrd 2808 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = 0)
223222mpteq2dva 5016 . . . . . . . 8 (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
224223fveq2d 6497 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
225189, 192sge0z 42088 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
226224, 225eqtrd 2808 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = 0)
227226oveq1d 6985 . . . . 5 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
228202, 25feqresmpt 6557 . . . . . . 7 (𝜑 → (𝑂𝑌) = (𝑦𝑌 ↦ (𝑂𝑦)))
229228fveq2d 6497 . . . . . 6 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))))
230 nfv 1873 . . . . . . 7 𝑦𝜑
231 fveq2 6493 . . . . . . 7 (𝑦 = (𝐴𝑛) → (𝑂𝑦) = (𝑂‘(𝐴𝑛)))
232161eqcomd 2778 . . . . . . 7 ((𝜑𝑛𝐵) → (𝐹𝑛) = (𝐴𝑛))
233202adantr 473 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
23425sselda 3852 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑦 ∈ 𝒫 𝑋)
235233, 234ffvelrnd 6671 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑂𝑦) ∈ (0[,]+∞))
236230, 189, 231, 194, 4, 232, 235sge0f1o 42095 . . . . . 6 (𝜑 → (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
237 eqidd 2773 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
238229, 236, 2373eqtrd 2812 . . . . 5 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
239212, 227, 2383eqtr4d 2818 . . . 4 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑂𝑌)))
240188, 208, 2393eqtrrd 2813 . . 3 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
241180, 240breq12d 4936 . 2 (𝜑 → ((𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
24249, 241mpbird 249 1 (𝜑 → (𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wex 1742  wcel 2050  wne 2961  wral 3082  wrex 3083  Vcvv 3409  cdif 3820  cun 3821  cin 3822  wss 3823  wpss 3824  c0 4172  ifcif 4344  𝒫 cpw 4416  {csn 4435   cuni 4706   ciun 4786   class class class wbr 4923  cmpt 5002  cres 5403  wf 6178  ontowfo 6180  1-1-ontowf1o 6181  cfv 6182  (class class class)co 6970  0cc0 10329  +∞cpnf 10465  cle 10469  cn 11433   +𝑒 cxad 12316  [,]cicc 12551  Σ^csumge0 42075
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-inf2 8892  ax-cnex 10385  ax-resscn 10386  ax-1cn 10387  ax-icn 10388  ax-addcl 10389  ax-addrcl 10390  ax-mulcl 10391  ax-mulrcl 10392  ax-mulcom 10393  ax-addass 10394  ax-mulass 10395  ax-distr 10396  ax-i2m1 10397  ax-1ne0 10398  ax-1rid 10399  ax-rnegex 10400  ax-rrecex 10401  ax-cnre 10402  ax-pre-lttri 10403  ax-pre-lttrn 10404  ax-pre-ltadd 10405  ax-pre-mulgt0 10406  ax-pre-sup 10407
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5306  df-eprel 5311  df-po 5320  df-so 5321  df-fr 5360  df-se 5361  df-we 5362  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-1st 7495  df-2nd 7496  df-wrecs 7744  df-recs 7806  df-rdg 7844  df-1o 7899  df-oadd 7903  df-er 8083  df-en 8301  df-dom 8302  df-sdom 8303  df-fin 8304  df-sup 8695  df-oi 8763  df-card 9156  df-pnf 10470  df-mnf 10471  df-xr 10472  df-ltxr 10473  df-le 10474  df-sub 10666  df-neg 10667  df-div 11093  df-nn 11434  df-2 11497  df-3 11498  df-n0 11702  df-z 11788  df-uz 12053  df-rp 12199  df-xadd 12319  df-ico 12554  df-icc 12555  df-fz 12703  df-fzo 12844  df-seq 13179  df-exp 13239  df-hash 13500  df-cj 14313  df-re 14314  df-im 14315  df-sqrt 14449  df-abs 14450  df-clim 14700  df-sum 14898  df-sumge0 42076
This theorem is referenced by:  isomennd  42244
  Copyright terms: Public domain W3C validator