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 44324
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 4476 . . . . . . . . 9 (𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
32adantl 482 . . . . . . . 8 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
4 isomenndlem.f . . . . . . . . . . 11 (𝜑𝐹:𝐵1-1-onto𝑌)
5 f1of 6753 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵𝑌)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵𝑌)
7 ssun1 4116 . . . . . . . . . . 11 𝑌 ⊆ (𝑌 ∪ {∅})
87a1i 11 . . . . . . . . . 10 (𝜑𝑌 ⊆ (𝑌 ∪ {∅}))
96, 8fssd 6655 . . . . . . . . 9 (𝜑𝐹:𝐵⟶(𝑌 ∪ {∅}))
109ffvelcdmda 7000 . . . . . . . 8 ((𝜑𝑛𝐵) → (𝐹𝑛) ∈ (𝑌 ∪ {∅}))
113, 10eqeltrd 2837 . . . . . . 7 ((𝜑𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
1211adantlr 712 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
13 iffalse 4479 . . . . . . . . 9 𝑛𝐵 → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
1413adantl 482 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
15 0ex 5245 . . . . . . . . . . 11 ∅ ∈ V
1615snid 4606 . . . . . . . . . 10 ∅ ∈ {∅}
17 elun2 4121 . . . . . . . . . 10 (∅ ∈ {∅} → ∅ ∈ (𝑌 ∪ {∅}))
1816, 17ax-mp 5 . . . . . . . . 9 ∅ ∈ (𝑌 ∪ {∅})
1918a1i 11 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑛𝐵) → ∅ ∈ (𝑌 ∪ {∅}))
2014, 19eqeltrd 2837 . . . . . . 7 ((𝜑 ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2120adantlr 712 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
2212, 21pm2.61dan 810 . . . . 5 ((𝜑𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ (𝑌 ∪ {∅}))
23 isomenndlem.a . . . . 5 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
2422, 23fmptd 7027 . . . 4 (𝜑𝐴:ℕ⟶(𝑌 ∪ {∅}))
25 isomenndlem.y . . . . 5 (𝜑𝑌 ⊆ 𝒫 𝑋)
26 0elpw 5292 . . . . . . 7 ∅ ∈ 𝒫 𝑋
27 snssi 4752 . . . . . . 7 (∅ ∈ 𝒫 𝑋 → {∅} ⊆ 𝒫 𝑋)
2826, 27ax-mp 5 . . . . . 6 {∅} ⊆ 𝒫 𝑋
2928a1i 11 . . . . 5 (𝜑 → {∅} ⊆ 𝒫 𝑋)
3025, 29unssd 4130 . . . 4 (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋)
3124, 30fssd 6655 . . 3 (𝜑𝐴:ℕ⟶𝒫 𝑋)
32 nnex 12058 . . . . . 6 ℕ ∈ V
3332mptex 7138 . . . . 5 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) ∈ V
3423, 33eqeltri 2833 . . . 4 𝐴 ∈ V
35 feq1 6618 . . . . . 6 (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋𝐴:ℕ⟶𝒫 𝑋))
3635anbi2d 629 . . . . 5 (𝑎 = 𝐴 → ((𝜑𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑𝐴:ℕ⟶𝒫 𝑋)))
37 fveq1 6810 . . . . . . . 8 (𝑎 = 𝐴 → (𝑎𝑛) = (𝐴𝑛))
3837iuneq2d 4965 . . . . . . 7 (𝑎 = 𝐴 𝑛 ∈ ℕ (𝑎𝑛) = 𝑛 ∈ ℕ (𝐴𝑛))
3938fveq2d 6815 . . . . . 6 (𝑎 = 𝐴 → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
40 simpl 483 . . . . . . . . . 10 ((𝑎 = 𝐴𝑛 ∈ ℕ) → 𝑎 = 𝐴)
4140fveq1d 6813 . . . . . . . . 9 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑎𝑛) = (𝐴𝑛))
4241fveq2d 6815 . . . . . . . 8 ((𝑎 = 𝐴𝑛 ∈ ℕ) → (𝑂‘(𝑎𝑛)) = (𝑂‘(𝐴𝑛)))
4342mpteq2dva 5186 . . . . . . 7 (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))
4443fveq2d 6815 . . . . . 6 (𝑎 = 𝐴 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
4539, 44breq12d 5099 . . . . 5 (𝑎 = 𝐴 → ((𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
4636, 45imbi12d 344 . . . 4 (𝑎 = 𝐴 → (((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛))))) ↔ ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))))
47 isomenndlem.subadd . . . 4 ((𝜑𝑎:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝑎𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎𝑛)))))
4834, 46, 47vtocl 3506 . . 3 ((𝜑𝐴:ℕ⟶𝒫 𝑋) → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
491, 31, 48syl2anc 584 . 2 (𝜑 → (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
506ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵𝑌)
51 simpr 485 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
52 id 22 . . . . . . . . . . . . . . 15 (𝐵 = ℕ → 𝐵 = ℕ)
5352eqcomd 2742 . . . . . . . . . . . . . 14 (𝐵 = ℕ → ℕ = 𝐵)
5453adantr 481 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ = 𝐵)
5551, 54eleqtrd 2839 . . . . . . . . . . . 12 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5655adantll 711 . . . . . . . . . . 11 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛𝐵)
5750, 56ffvelcdmd 7001 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑌)
58 eqid 2736 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ (𝐹𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛))
5957, 58fmptd 7027 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌)
6023a1i 11 . . . . . . . . . . . 12 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)))
6155iftrued 4478 . . . . . . . . . . . . 13 ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
6261mpteq2dva 5186 . . . . . . . . . . . 12 (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6360, 62eqtrd 2776 . . . . . . . . . . 11 (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹𝑛)))
6463feq1d 6622 . . . . . . . . . 10 (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6564adantl 482 . . . . . . . . 9 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹𝑛)):ℕ⟶𝑌))
6659, 65mpbird 256 . . . . . . . 8 ((𝜑𝐵 = ℕ) → 𝐴:ℕ⟶𝑌)
67 f1ofo 6760 . . . . . . . . . . . . . . . 16 (𝐹:𝐵1-1-onto𝑌𝐹:𝐵onto𝑌)
684, 67syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐵onto𝑌)
69 dffo3 7017 . . . . . . . . . . . . . . 15 (𝐹:𝐵onto𝑌 ↔ (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7068, 69sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (𝐹:𝐵𝑌 ∧ ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛)))
7170simprd 496 . . . . . . . . . . . . 13 (𝜑 → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
7271adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛))
73 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → 𝑦𝑌)
74 rspa 3227 . . . . . . . . . . . 12 ((∀𝑦𝑌𝑛𝐵 𝑦 = (𝐹𝑛) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7572, 73, 74syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
7675adantlr 712 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛𝐵 𝑦 = (𝐹𝑛))
77 nfv 1916 . . . . . . . . . . . 12 𝑛(𝜑𝐵 = ℕ)
78 nfre1 3264 . . . . . . . . . . . 12 𝑛𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)
79 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛𝐵)
80 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝐵 = ℕ)
8179, 80eleqtrd 2839 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
8281adantll 711 . . . . . . . . . . . . . . 15 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵) → 𝑛 ∈ ℕ)
83823adant3 1131 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑛 ∈ ℕ)
8460fveq1d 6813 . . . . . . . . . . . . . . . . 17 (𝐵 = ℕ → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
85843ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐴𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛))
86 fvex 6824 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑛) ∈ V
8786, 15ifex 4520 . . . . . . . . . . . . . . . . . . . 20 if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
89 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))
9089fvmpt2 6925 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
9181, 88, 90syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
922adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝐵 = ℕ ∧ 𝑛𝐵) → if(𝑛𝐵, (𝐹𝑛), ∅) = (𝐹𝑛))
9391, 92eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝐵 = ℕ ∧ 𝑛𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
94933adant3 1131 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛𝐵, (𝐹𝑛), ∅))‘𝑛) = (𝐹𝑛))
95 id 22 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐹𝑛) → 𝑦 = (𝐹𝑛))
9695eqcomd 2742 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐹𝑛) → (𝐹𝑛) = 𝑦)
97963ad2ant3 1134 . . . . . . . . . . . . . . . 16 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → (𝐹𝑛) = 𝑦)
9885, 94, 973eqtrrd 2781 . . . . . . . . . . . . . . 15 ((𝐵 = ℕ ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
99983adant1l 1175 . . . . . . . . . . . . . 14 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → 𝑦 = (𝐴𝑛))
100 rspe 3228 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10183, 99, 100syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝐵 = ℕ) ∧ 𝑛𝐵𝑦 = (𝐹𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1021013exp 1118 . . . . . . . . . . . 12 ((𝜑𝐵 = ℕ) → (𝑛𝐵 → (𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
10377, 78, 102rexlimd 3245 . . . . . . . . . . 11 ((𝜑𝐵 = ℕ) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
104103adantr 481 . . . . . . . . . 10 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → (∃𝑛𝐵 𝑦 = (𝐹𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
10576, 104mpd 15 . . . . . . . . 9 (((𝜑𝐵 = ℕ) ∧ 𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
106105ralrimiva 3139 . . . . . . . 8 ((𝜑𝐵 = ℕ) → ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
10766, 106jca 512 . . . . . . 7 ((𝜑𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
108 dffo3 7017 . . . . . . 7 (𝐴:ℕ–onto𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦𝑌𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
109107, 108sylibr 233 . . . . . 6 ((𝜑𝐵 = ℕ) → 𝐴:ℕ–onto𝑌)
110 founiiun 42961 . . . . . 6 (𝐴:ℕ–onto𝑌 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
111109, 110syl 17 . . . . 5 ((𝜑𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
112 uniun 4875 . . . . . . . 8 (𝑌 ∪ {∅}) = ( 𝑌 {∅})
11315unisn 4871 . . . . . . . . 9 {∅} = ∅
114113uneq2i 4104 . . . . . . . 8 ( 𝑌 {∅}) = ( 𝑌 ∪ ∅)
115 un0 4334 . . . . . . . 8 ( 𝑌 ∪ ∅) = 𝑌
116112, 114, 1153eqtrri 2769 . . . . . . 7 𝑌 = (𝑌 ∪ {∅})
117116a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = (𝑌 ∪ {∅}))
11824adantr 481 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅}))
119 nfv 1916 . . . . . . . . . . . . 13 𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅)
120 isomenndlem.b . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ ℕ)
121120adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ)
12252necon3bi 2967 . . . . . . . . . . . . . . . . . 18 𝐵 = ℕ → 𝐵 ≠ ℕ)
123122adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ)
124121, 123jca 512 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
125 df-pss 3915 . . . . . . . . . . . . . . . 16 (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ))
126124, 125sylibr 233 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ)
127 pssnel 4414 . . . . . . . . . . . . . . 15 (𝐵 ⊊ ℕ → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
128126, 127syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
129128adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵))
130 simprl 768 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
131 simprl 768 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑛 ∈ ℕ)
13287a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
13323fvmpt2 6925 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
134131, 132, 133syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
135134adantlr 712 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
13613ad2antll 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
137 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ∅ → 𝑦 = ∅)
138137eqcomd 2742 . . . . . . . . . . . . . . . . . 18 (𝑦 = ∅ → ∅ = 𝑦)
139138ad2antlr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∅ = 𝑦)
140135, 136, 1393eqtrrd 2781 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → 𝑦 = (𝐴𝑛))
141130, 140, 100syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
142141ex 413 . . . . . . . . . . . . . 14 ((𝜑𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
143142adantlr 712 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
144119, 78, 129, 143exlimimdd 2211 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
145144adantlr 712 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
146 simplll 772 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑)
147 simpl 483 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅}))
148 elsni 4587 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {∅} → 𝑦 = ∅)
149148con3i 154 . . . . . . . . . . . . . . 15 𝑦 = ∅ → ¬ 𝑦 ∈ {∅})
150149adantl 482 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈ {∅})
151 elunnel2 42821 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦𝑌)
152147, 150, 151syl2anc 584 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
153152adantll 711 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦𝑌)
15468adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → 𝐹:𝐵onto𝑌)
155 foelcdmi 6870 . . . . . . . . . . . . . 14 ((𝐹:𝐵onto𝑌𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
156154, 73, 155syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → ∃𝑛𝐵 (𝐹𝑛) = 𝑦)
157 nfv 1916 . . . . . . . . . . . . . 14 𝑛(𝜑𝑦𝑌)
158120sselda 3930 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵) → 𝑛 ∈ ℕ)
1591583adant3 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑛 ∈ ℕ)
160158, 87, 133sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛𝐵) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
161160, 3eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝐵) → (𝐴𝑛) = (𝐹𝑛))
1621613adant3 1131 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐴𝑛) = (𝐹𝑛))
163 simp3 1137 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → (𝐹𝑛) = 𝑦)
164162, 163eqtr2d 2777 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → 𝑦 = (𝐴𝑛))
165159, 164, 100syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐵 ∧ (𝐹𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
1661653exp 1118 . . . . . . . . . . . . . . 15 (𝜑 → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
167166adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑌) → (𝑛𝐵 → ((𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))))
168157, 78, 167rexlimd 3245 . . . . . . . . . . . . 13 ((𝜑𝑦𝑌) → (∃𝑛𝐵 (𝐹𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
169156, 168mpd 15 . . . . . . . . . . . 12 ((𝜑𝑦𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
170146, 153, 169syl2anc 584 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
171145, 170pm2.61dan 810 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
172171ralrimiva 3139 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛))
173118, 172jca 512 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
174 dffo3 7017 . . . . . . . 8 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴𝑛)))
175173, 174sylibr 233 . . . . . . 7 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅}))
176 founiiun 42961 . . . . . . 7 (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
177175, 176syl 17 . . . . . 6 ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝑌 ∪ {∅}) = 𝑛 ∈ ℕ (𝐴𝑛))
178117, 177eqtrd 2776 . . . . 5 ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
179111, 178pm2.61dan 810 . . . 4 (𝜑 𝑌 = 𝑛 ∈ ℕ (𝐴𝑛))
180179fveq2d 6815 . . 3 (𝜑 → (𝑂 𝑌) = (𝑂 𝑛 ∈ ℕ (𝐴𝑛)))
181 uncom 4097 . . . . . . . . 9 ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))
182181a1i 11 . . . . . . . 8 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)))
183 undif 4425 . . . . . . . . 9 (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
184120, 183sylib 217 . . . . . . . 8 (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ)
185182, 184eqtrd 2776 . . . . . . 7 (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ)
186185eqcomd 2742 . . . . . 6 (𝜑 → ℕ = ((ℕ ∖ 𝐵) ∪ 𝐵))
187186mpteq1d 5181 . . . . 5 (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛))))
188187fveq2d 6815 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))))
189 nfv 1916 . . . . 5 𝑛𝜑
190 difexg 5265 . . . . . . 7 (ℕ ∈ V → (ℕ ∖ 𝐵) ∈ V)
19132, 190ax-mp 5 . . . . . 6 (ℕ ∖ 𝐵) ∈ V
192191a1i 11 . . . . 5 (𝜑 → (ℕ ∖ 𝐵) ∈ V)
19332a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
194193, 120ssexd 5262 . . . . 5 (𝜑𝐵 ∈ V)
195 disjdifr 4416 . . . . . 6 ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅
196195a1i 11 . . . . 5 (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅)
197 simpl 483 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑)
198 eldifi 4071 . . . . . . 7 (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ)
199198adantl 482 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ)
200 isomenndlem.o . . . . . . . 8 (𝜑𝑂:𝒫 𝑋⟶(0[,]+∞))
201200adantr 481 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
20231ffvelcdmda 7000 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 𝑋)
203201, 202ffvelcdmd 7001 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
204197, 199, 203syl2anc 584 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
205158, 203syldan 591 . . . . 5 ((𝜑𝑛𝐵) → (𝑂‘(𝐴𝑛)) ∈ (0[,]+∞))
206189, 192, 194, 196, 204, 205sge0splitmpt 44205 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
207 eqid 2736 . . . . . . . 8 (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))) = (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))
208205, 207fmptd 7027 . . . . . . 7 (𝜑 → (𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))):𝐵⟶(0[,]+∞))
209194, 208sge0xrcl 44179 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) ∈ ℝ*)
210209xaddid2d 43112 . . . . 5 (𝜑 → (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
21187a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) ∈ V)
212199, 211, 133syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = if(𝑛𝐵, (𝐹𝑛), ∅))
213 eldifn 4072 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛𝐵)
214213adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛𝐵)
215214iffalsed 4481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛𝐵, (𝐹𝑛), ∅) = ∅)
216212, 215eqtrd 2776 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴𝑛) = ∅)
217216fveq2d 6815 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = (𝑂‘∅))
218 isomenndlem.o0 . . . . . . . . . . 11 (𝜑 → (𝑂‘∅) = 0)
219197, 218syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0)
220217, 219eqtrd 2776 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴𝑛)) = 0)
221220mpteq2dva 5186 . . . . . . . 8 (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))
222221fveq2d 6815 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)))
223189, 192sge0z 44169 . . . . . . 7 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0)
224222, 223eqtrd 2776 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) = 0)
225224oveq1d 7331 . . . . 5 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (0 +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))))
226200, 25feqresmpt 6877 . . . . . . 7 (𝜑 → (𝑂𝑌) = (𝑦𝑌 ↦ (𝑂𝑦)))
227226fveq2d 6815 . . . . . 6 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))))
228 nfv 1916 . . . . . . 7 𝑦𝜑
229 fveq2 6811 . . . . . . 7 (𝑦 = (𝐴𝑛) → (𝑂𝑦) = (𝑂‘(𝐴𝑛)))
230161eqcomd 2742 . . . . . . 7 ((𝜑𝑛𝐵) → (𝐹𝑛) = (𝐴𝑛))
231200adantr 481 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞))
23225sselda 3930 . . . . . . . 8 ((𝜑𝑦𝑌) → 𝑦 ∈ 𝒫 𝑋)
233231, 232ffvelcdmd 7001 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑂𝑦) ∈ (0[,]+∞))
234228, 189, 229, 194, 4, 230, 233sge0f1o 44176 . . . . . 6 (𝜑 → (Σ^‘(𝑦𝑌 ↦ (𝑂𝑦))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
235 eqidd 2737 . . . . . 6 (𝜑 → (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
236227, 234, 2353eqtrd 2780 . . . . 5 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛)))))
237210, 225, 2363eqtr4d 2786 . . . 4 (𝜑 → ((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴𝑛)))) +𝑒^‘(𝑛𝐵 ↦ (𝑂‘(𝐴𝑛))))) = (Σ^‘(𝑂𝑌)))
238188, 206, 2373eqtrrd 2781 . . 3 (𝜑 → (Σ^‘(𝑂𝑌)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛)))))
239180, 238breq12d 5099 . 2 (𝜑 → ((𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)) ↔ (𝑂 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴𝑛))))))
24049, 239mpbird 256 1 (𝜑 → (𝑂 𝑌) ≤ (Σ^‘(𝑂𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wne 2940  wral 3061  wrex 3070  Vcvv 3440  cdif 3893  cun 3894  cin 3895  wss 3896  wpss 3897  c0 4266  ifcif 4470  𝒫 cpw 4544  {csn 4570   cuni 4849   ciun 4936   class class class wbr 5086  cmpt 5169  cres 5609  wf 6461  ontowfo 6463  1-1-ontowf1o 6464  cfv 6465  (class class class)co 7316  0cc0 10950  +∞cpnf 11085  cle 11089  cn 12052   +𝑒 cxad 12925  [,]cicc 13161  Σ^csumge0 44156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-inf2 9476  ax-cnex 11006  ax-resscn 11007  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-addrcl 11011  ax-mulcl 11012  ax-mulrcl 11013  ax-mulcom 11014  ax-addass 11015  ax-mulass 11016  ax-distr 11017  ax-i2m1 11018  ax-1ne0 11019  ax-1rid 11020  ax-rnegex 11021  ax-rrecex 11022  ax-cnre 11023  ax-pre-lttri 11024  ax-pre-lttrn 11025  ax-pre-ltadd 11026  ax-pre-mulgt0 11027  ax-pre-sup 11028
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-int 4892  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7273  df-ov 7319  df-oprab 7320  df-mpo 7321  df-om 7759  df-1st 7877  df-2nd 7878  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-1o 8345  df-er 8547  df-en 8783  df-dom 8784  df-sdom 8785  df-fin 8786  df-sup 9277  df-oi 9345  df-card 9774  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093  df-le 11094  df-sub 11286  df-neg 11287  df-div 11712  df-nn 12053  df-2 12115  df-3 12116  df-n0 12313  df-z 12399  df-uz 12662  df-rp 12810  df-xadd 12928  df-ico 13164  df-icc 13165  df-fz 13319  df-fzo 13462  df-seq 13801  df-exp 13862  df-hash 14124  df-cj 14886  df-re 14887  df-im 14888  df-sqrt 15022  df-abs 15023  df-clim 15273  df-sum 15474  df-sumge0 44157
This theorem is referenced by:  isomennd  44325
  Copyright terms: Public domain W3C validator