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 46061
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 4536 . . . . . . . . 9 (𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
32adantl 480 . . . . . . . 8 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
4 isomenndlem.f . . . . . . . . . . 11 (𝜑𝐹:𝐵1-1-onto𝑌)
5 f1of 6838 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵𝑌)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵𝑌)
7 ssun1 4170 . . . . . . . . . . 11 𝑌 ⊆ (𝑌 ∪ {∅})
87a1i 11 . . . . . . . . . 10 (𝜑𝑌 ⊆ (𝑌 ∪ {∅}))
96, 8fssd 6740 . . . . . . . . 9 (𝜑𝐹:𝐵⟶(𝑌 ∪ {∅}))
109ffvelcdmda 7093 . . . . . . . 8 ((𝜑𝑛𝐵) → (𝐹𝑛) ∈ (𝑌 ∪ {∅}))
113, 10eqeltrd 2825 . . . . . . 7 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
1211adantlr 713 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13 iffalse 4539 . . . . . . . . 9 𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
1413adantl 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
15 0ex 5308 . . . . . . . . . . 11 ∅ ∈ V
1615snid 4666 . . . . . . . . . 10 ∅ ∈ {∅}
17 elun2 4175 . . . . . . . . . 10 (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
1816, 17ax-mp 5 . . . . . . . . 9 ∅ ∈ (𝑌 ∪ {∅})
1918a1i 11 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
2014, 19eqeltrd 2825 . . . . . . 7 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2120adantlr 713 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2212, 21pm2.61dan 811 . . . . 5 ((𝜑𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23 isomenndlem.a . . . . 5 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
2422, 23fmptd 7123 . . . 4 (𝜑𝐴:ℕ⟶(𝑌 ∪ {∅}))
25 isomenndlem.y . . . . 5 (𝜑𝑌 ⊆ 𝒫 𝑋)
26 0elpw 5356 . . . . . . 7 ∅ ∈ 𝒫 𝑋
27 snssi 4813 . . . . . . 7 (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
2826, 27ax-mp 5 . . . . . 6 {∅} ⊆ 𝒫 𝑋
2928a1i 11 . . . . 5 (𝜑 → {∅} ⊆ 𝒫 𝑋)
3025, 29unssd 4184 . . . 4 (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
3124, 30fssd 6740 . . 3 (𝜑𝐴:ℕ⟶𝒫 𝑋)
32 nnex 12256 . . . . . 6 ℕ ∈ V
3332mptex 7235 . . . . 5 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) ∈ V
3423, 33eqeltri 2821 . . . 4 𝐴 ∈ V
35 feq1 6704 . . . . . 6 (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋𝐴:ℕ⟶𝒫 𝑋))
3635anbi2d 628 . . . . 5 (𝑎 = 𝐴 → ((𝜑𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑𝐴:ℕ⟶𝒫 𝑋)))
37 fveq1 6895 . . . . . . . 8 (𝑎 = 𝐴 → (𝑎𝑛) = (𝐴𝑛))
3837iuneq2d 5026 . . . . . . 7 (𝑎 = 𝐴 𝑛 ∈ ℕ (𝑎𝑛) = 𝑛 ∈ ℕ (𝐴𝑛))
3938fveq2d 6900 . . . . . 6 (𝑎 = 𝐴 → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
40 simpl 481 . . . . . . . . . 10 ((𝑎 = 𝐴𝑛 ∈ ℕ) → 𝑎 = 𝐴)
4140fveq1d 6898 . . . . . . . . 9 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑎𝑛) = (𝐴𝑛))
4241fveq2d 6900 . . . . . . . 8 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑂‘(𝑎𝑛)) = (𝑂‘(𝐴𝑛)))
4342mpteq2dva 5249 . . . . . . 7 (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))
4443fveq2d 6900 . . . . . 6 (𝑎 = 𝐴 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
4539, 44breq12d 5162 . . . . 5 (𝑎 = 𝐴 → ((𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
4636, 45imbi12d 343 . . . 4 (𝑎 = 𝐴 → (((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))))) ↔ ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))))
47 isomenndlem.subadd . . . 4 ((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))))
4834, 46, 47vtocl 3536 . . 3 ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
491, 31, 48syl2anc 582 . 2 (𝜑 → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
506ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵𝑌)
51 simpr 483 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52 id 22 . . . . . . . . . . . . . . 15 (𝐵 = ℕ → 𝐵 = ℕ)
5352eqcomd 2731 . . . . . . . . . . . . . 14 (𝐵 = ℕ → ℕ = 𝐵)
5453adantr 479 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
5551, 54eleqtrd 2827 . . . . . . . . . . . 12 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5655adantll 712 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5750, 56ffvelcdmd 7094 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑌)
58 eqid 2725 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ (𝐹𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛))
5957, 58fmptd 7123 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌)
6023a1i 11 . . . . . . . . . . . 12 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)))
6155iftrued 4538 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
6261mpteq2dva 5249 . . . . . . . . . . . 12 (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6360, 62eqtrd 2765 . . . . . . . . . . 11 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6463feq1d 6708 . . . . . . . . . 10 (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6564adantl 480 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6659, 65mpbird 256 . . . . . . . 8 ((𝜑𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67 f1ofo 6845 . . . . . . . . . . . . . . . 16 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵onto𝑌)
684, 67syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐵onto𝑌)
69 dffo3 7111 . . . . . . . . . . . . . . 15 (𝐹:𝐵onto𝑌 ↔ (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7068, 69sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7170simprd 494 . . . . . . . . . . . . 13 (𝜑 → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
7271adantr 479 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
73 simpr 483 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → 𝑦𝑌)
74 rspa 3235 . . . . . . . . . . . 12 ((∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7572, 73, 74syl2anc 582 . . . . . . . . . . 11 ((𝜑𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7675adantlr 713 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
77 nfv 1909 . . . . . . . . . . . 12 𝑛(𝜑𝐵 = ℕ)
78 nfre1 3272 . . . . . . . . . . . 12 𝑛𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)
79 simpr 483 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛𝐵)
80 simpl 481 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝐵 = ℕ)
8179, 80eleqtrd 2827 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
8281adantll 712 . . . . . . . . . . . . . . 15 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
83823adant3 1129 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑛 ∈ ℕ)
8460fveq1d 6898 . . . . . . . . . . . . . . . . 17 (𝐵 = ℕ → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
85843ad2ant1 1130 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
86 fvex 6909 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑛) ∈ V
8786, 15ifex 4580 . . . . . . . . . . . . . . . . . . . 20 if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
89 eqid 2725 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
9089fvmpt2 7015 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
9181, 88, 90syl2anc 582 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
922adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
9391, 92eqtrd 2765 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
94933adant3 1129 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
95 id 22 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐹𝑛) → 𝑦 = (𝐹𝑛))
9695eqcomd 2731 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐹𝑛) → (𝐹𝑛) = 𝑦)
97963ad2ant3 1132 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐹𝑛) = 𝑦)
9885, 94, 973eqtrrd 2770 . . . . . . . . . . . . . . 15 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
99983adant1l 1173 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
100 rspe 3236 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10183, 99, 100syl2anc 582 . . . . . . . . . . . . 13 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1021013exp 1116 . . . . . . . . . . . 12 ((𝜑𝐵 = ℕ) → (𝑛𝐵 → (𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
10377, 78, 102rexlimd 3253 . . . . . . . . . . 11 ((𝜑𝐵 = ℕ) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
104103adantr 479 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
10576, 104mpd 15 . . . . . . . . 9 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
106105ralrimiva 3135 . . . . . . . 8 ((𝜑𝐵 = ℕ) → ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10766, 106jca 510 . . . . . . 7 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
108 dffo3 7111 . . . . . . 7 (𝐴:ℕ–onto𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
109107, 108sylibr 233 . . . . . 6 ((𝜑𝐵 = ℕ) → 𝐴:ℕ–onto𝑌)
110 founiiun 44696 . . . . . 6 (𝐴:ℕ–onto𝑌 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
111109, 110syl 17 . . . . 5 ((𝜑𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
112 uniun 4934 . . . . . . . 8 (𝑌 ∪ {∅}) = ( 𝑌 {∅})
11315unisn 4930 . . . . . . . . 9 {∅} = ∅
114113uneq2i 4157 . . . . . . . 8 ( 𝑌 {∅}) = ( 𝑌 ∪ ∅)
115 un0 4392 . . . . . . . 8 ( 𝑌 ∪ ∅) = 𝑌
116112, 114, 1153eqtrri 2758 . . . . . . 7 𝑌 = (𝑌 ∪ {∅})
117116a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = (𝑌 ∪ {∅}))
11824adantr 479 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119 nfv 1909 . . . . . . . . . . . . 13 𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
120 isomenndlem.b . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ ℕ)
121120adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
12252necon3bi 2956 . . . . . . . . . . . . . . . . . 18 𝐵 = ℕ → 𝐵 ≠ ℕ)
123122adantl 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
124121, 123jca 510 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125 df-pss 3964 . . . . . . . . . . . . . . . 16 (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
126124, 125sylibr 233 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
127 pssnel 4472 . . . . . . . . . . . . . . 15 (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
128126, 127syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
129128adantr 479 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
130 simprl 769 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
131 simprl 769 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
13287a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
13323fvmpt2 7015 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
134131, 132, 133syl2anc 582 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
135134adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
13613ad2antll 727 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
137 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ∅ → 𝑦 = ∅)
138137eqcomd 2731 . . . . . . . . . . . . . . . . . 18 (𝑦 = ∅ → ∅ = 𝑦)
139138ad2antlr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∅ = 𝑦)
140135, 136, 1393eqtrrd 2770 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑦 = (𝐴𝑛))
141130, 140, 100syl2anc 582 . . . . . . . . . . . . . . 15 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
142141ex 411 . . . . . . . . . . . . . 14 ((𝜑𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
143142adantlr 713 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
144119, 78, 129, 143exlimimdd 2207 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
145144adantlr 713 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
146 simplll 773 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
147 simpl 481 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
148 elsni 4647 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {∅} → 𝑦 = ∅)
149148con3i 154 . . . . . . . . . . . . . . 15 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
150149adantl 480 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
151 elunnel2 4147 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦𝑌)
152147, 150, 151syl2anc 582 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
153152adantll 712 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
15468adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → 𝐹:𝐵onto𝑌)
155 foelcdmi 6959 . . . . . . . . . . . . . 14 ((𝐹:𝐵onto𝑌𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
156154, 73, 155syl2anc 582 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
157 nfv 1909 . . . . . . . . . . . . . 14 𝑛(𝜑𝑦𝑌)
158120sselda 3976 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵) → 𝑛 ∈ ℕ)
1591583adant3 1129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑛 ∈ ℕ)
160158, 87, 133sylancl 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛𝐵) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
161160, 3eqtrd 2765 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐵) → (𝐴𝑛) = (𝐹𝑛))
1621613adant3 1129 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐴𝑛) = (𝐹𝑛))
163 simp3 1135 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐹𝑛) = 𝑦)
164162, 163eqtr2d 2766 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑦 = (𝐴𝑛))
165159, 164, 100syl2anc 582 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1661653exp 1116 . . . . . . . . . . . . . . 15 (𝜑 → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
167166adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
168157, 78, 167rexlimd 3253 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → (∃𝑛𝐵 (𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
169156, 168mpd 15 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
170146, 153, 169syl2anc 582 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
171145, 170pm2.61dan 811 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
172171ralrimiva 3135 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
173118, 172jca 510 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
174 dffo3 7111 . . . . . . . 8 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
175173, 174sylibr 233 . . . . . . 7 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
176 founiiun 44696 . . . . . . 7 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
177175, 176syl 17 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
178117, 177eqtrd 2765 . . . . 5 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
179111, 178pm2.61dan 811 . . . 4 (𝜑 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
180179fveq2d 6900 . . 3 (𝜑 → (𝑂 𝑌) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
181 uncom 4150 . . . . . . . . 9 ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
182181a1i 11 . . . . . . . 8 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
183 undif 4483 . . . . . . . . 9 (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
184120, 183sylib 217 . . . . . . . 8 (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185182, 184eqtrd 2765 . . . . . . 7 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
186185eqcomd 2731 . . . . . 6 (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
187186mpteq1d 5244 . . . . 5 (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛))))
188187fveq2d 6900 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))))
189 nfv 1909 . . . . 5 𝑛𝜑
190 difexg 5330 . . . . . . 7 (ℕ ∈ V → (ℕ ∖ 𝐵) ∈ V)
19132, 190ax-mp 5 . . . . . 6 (ℕ ∖ 𝐵) ∈ V
192191a1i 11 . . . . 5 (𝜑 → (ℕ ∖ 𝐵) ∈ V)
19332a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
194193, 120ssexd 5325 . . . . 5 (𝜑𝐵 ∈ V)
195 disjdifr 4474 . . . . . 6 ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
196195a1i 11 . . . . 5 (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
197 simpl 481 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
198 eldifi 4123 . . . . . . 7 (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
199198adantl 480 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
200 isomenndlem.o . . . . . . . 8 (𝜑𝑂:𝒫 𝑋⟶(0[,]+∞))
201200adantr 479 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
20231ffvelcdmda 7093 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 𝑋)
203201, 202ffvelcdmd 7094 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
204197, 199, 203syl2anc 582 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
205158, 203syldan 589 . . . . 5 ((𝜑𝑛𝐵) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
206189, 192, 194, 196, 204, 205sge0splitmpt 45942 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
207 eqid 2725 . . . . . . . 8 (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))) = (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))
208205, 207fmptd 7123 . . . . . . 7 (𝜑 → (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))):𝐵⟶(0[,]+∞))
209194, 208sge0xrcl 45916 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) ∈ ℝ*)
210209xaddlidd 44844 . . . . 5 (𝜑 → (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
21187a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
212199, 211, 133syl2anc 582 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
213 eldifn 4124 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛𝐵)
214213adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛𝐵)
215214iffalsed 4541 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
216212, 215eqtrd 2765 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = ∅)
217216fveq2d 6900 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = (𝑂‘∅))
218 isomenndlem.o0 . . . . . . . . . . 11 (𝜑 → (𝑂‘∅) = 0)
219197, 218syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
220217, 219eqtrd 2765 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = 0)
221220mpteq2dva 5249 . . . . . . . 8 (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
222221fveq2d 6900 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
223189, 192sge0z 45906 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
224222, 223eqtrd 2765 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = 0)
225224oveq1d 7434 . . . . 5 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
226200, 25feqresmpt 6967 . . . . . . 7 (𝜑 → (𝑂𝑌) = (𝑦𝑌 ↦ (𝑂𝑦)))
227226fveq2d 6900 . . . . . 6 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))))
228 nfv 1909 . . . . . . 7 𝑦𝜑
229 fveq2 6896 . . . . . . 7 (𝑦 = (𝐴𝑛) → (𝑂𝑦) = (𝑂‘(𝐴𝑛)))
230161eqcomd 2731 . . . . . . 7 ((𝜑𝑛𝐵) → (𝐹𝑛) = (𝐴𝑛))
231200adantr 479 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
23225sselda 3976 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑦 ∈ 𝒫 𝑋)
233231, 232ffvelcdmd 7094 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑂𝑦) ∈ (0[,]+∞))
234228, 189, 229, 194, 4, 230, 233sge0f1o 45913 . . . . . 6 (𝜑 → (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
235 eqidd 2726 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
236227, 234, 2353eqtrd 2769 . . . . 5 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
237210, 225, 2363eqtr4d 2775 . . . 4 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑂𝑌)))
238188, 206, 2373eqtrrd 2770 . . 3 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
239180, 238breq12d 5162 . 2 (𝜑 → ((𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
24049, 239mpbird 256 1 (𝜑 → (𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wne 2929  wral 3050  wrex 3059  Vcvv 3461  cdif 3941  cun 3942  cin 3943  wss 3944  wpss 3945  c0 4322  ifcif 4530  𝒫 cpw 4604  {csn 4630   cuni 4909   ciun 4997   class class class wbr 5149  cmpt 5232  cres 5680  wf 6545  ontowfo 6547  1-1-ontowf1o 6548  cfv 6549  (class class class)co 7419  0cc0 11145  +∞cpnf 11282  cle 11286  cn 12250   +𝑒 cxad 13130  [,]cicc 13367  Σ^csumge0 45893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9671  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222  ax-pre-sup 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-sup 9472  df-oi 9540  df-card 9969  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-div 11909  df-nn 12251  df-2 12313  df-3 12314  df-n0 12511  df-z 12597  df-uz 12861  df-rp 13015  df-xadd 13133  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-seq 14008  df-exp 14068  df-hash 14334  df-cj 15090  df-re 15091  df-im 15092  df-sqrt 15226  df-abs 15227  df-clim 15476  df-sum 15677  df-sumge0 45894
This theorem is referenced by:  isomennd  46062
  Copyright terms: Public domain W3C validator