Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
⊢ (𝜑 → 𝜑) |
2 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛)) |
3 | 2 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛)) |
4 | | isomenndlem.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌) |
5 | | f1of 6050 |
. . . . . . . . . . 11
⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵⟶𝑌) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐵⟶𝑌) |
7 | | ssun1 3738 |
. . . . . . . . . . 11
⊢ 𝑌 ⊆ (𝑌 ∪ {∅}) |
8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ⊆ (𝑌 ∪ {∅})) |
9 | 6, 8 | fssd 5970 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐵⟶(𝑌 ∪ {∅})) |
10 | 9 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) ∈ (𝑌 ∪ {∅})) |
11 | 3, 10 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅})) |
12 | 11 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅})) |
13 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
𝑛 ∈ 𝐵 → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅) |
14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅) |
15 | | 0ex 4718 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
16 | 15 | snid 4155 |
. . . . . . . . . 10
⊢ ∅
∈ {∅} |
17 | | elun2 3743 |
. . . . . . . . . 10
⊢ (∅
∈ {∅} → ∅ ∈ (𝑌 ∪ {∅})) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . 9
⊢ ∅
∈ (𝑌 ∪
{∅}) |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → ∅ ∈ (𝑌 ∪ {∅})) |
20 | 14, 19 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅})) |
21 | 20 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅})) |
22 | 12, 21 | pm2.61dan 828 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ (𝑌 ∪ {∅})) |
23 | | isomenndlem.a |
. . . . 5
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) |
24 | 22, 23 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐴:ℕ⟶(𝑌 ∪ {∅})) |
25 | | isomenndlem.y |
. . . . 5
⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋) |
26 | | 0elpw 4760 |
. . . . . . 7
⊢ ∅
∈ 𝒫 𝑋 |
27 | | snssi 4280 |
. . . . . . 7
⊢ (∅
∈ 𝒫 𝑋 →
{∅} ⊆ 𝒫 𝑋) |
28 | 26, 27 | ax-mp 5 |
. . . . . 6
⊢ {∅}
⊆ 𝒫 𝑋 |
29 | 28 | a1i 11 |
. . . . 5
⊢ (𝜑 → {∅} ⊆
𝒫 𝑋) |
30 | 25, 29 | unssd 3751 |
. . . 4
⊢ (𝜑 → (𝑌 ∪ {∅}) ⊆ 𝒫 𝑋) |
31 | 24, 30 | fssd 5970 |
. . 3
⊢ (𝜑 → 𝐴:ℕ⟶𝒫 𝑋) |
32 | | nnex 10903 |
. . . . . 6
⊢ ℕ
∈ V |
33 | 32 | mptex 6390 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) ∈ V |
34 | 23, 33 | eqeltri 2684 |
. . . 4
⊢ 𝐴 ∈ V |
35 | | feq1 5939 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑎:ℕ⟶𝒫 𝑋 ↔ 𝐴:ℕ⟶𝒫 𝑋)) |
36 | 35 | anbi2d 736 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) ↔ (𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋))) |
37 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎‘𝑛) = (𝐴‘𝑛)) |
38 | 37 | iuneq2d 4483 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ∪
𝑛 ∈ ℕ (𝑎‘𝑛) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) |
39 | 38 | fveq2d 6107 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) = (𝑂‘∪
𝑛 ∈ ℕ (𝐴‘𝑛))) |
40 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → 𝑎 = 𝐴) |
41 | 40 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑎‘𝑛) = (𝐴‘𝑛)) |
42 | 41 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑎 = 𝐴 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝑎‘𝑛)) = (𝑂‘(𝐴‘𝑛))) |
43 | 42 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))) |
44 | 43 | fveq2d 6107 |
. . . . . 6
⊢ (𝑎 = 𝐴 →
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))) |
45 | 39, 44 | breq12d 4596 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))) ↔ (𝑂‘∪
𝑛 ∈ ℕ (𝐴‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))) |
46 | 36, 45 | imbi12d 333 |
. . . 4
⊢ (𝑎 = 𝐴 → (((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) ↔ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝐴‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))))) |
47 | | isomenndlem.subadd |
. . . 4
⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝑎‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) |
48 | 34, 46, 47 | vtocl 3232 |
. . 3
⊢ ((𝜑 ∧ 𝐴:ℕ⟶𝒫 𝑋) → (𝑂‘∪
𝑛 ∈ ℕ (𝐴‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))) |
49 | 1, 31, 48 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ ℕ (𝐴‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))) |
50 | 6 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝐹:𝐵⟶𝑌) |
51 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℕ) |
52 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = ℕ → 𝐵 = ℕ) |
53 | 52 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = ℕ → ℕ =
𝐵) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → ℕ
= 𝐵) |
55 | 51, 54 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵) |
56 | 55 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ 𝐵) |
57 | 50, 56 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑌) |
58 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)) |
59 | 57, 58 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌) |
60 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))) |
61 | 55 | iftrued 4044 |
. . . . . . . . . . . . 13
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛)) |
62 | 61 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢ (𝐵 = ℕ → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛))) |
63 | 60, 62 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝐵 = ℕ → 𝐴 = (𝑛 ∈ ℕ ↦ (𝐹‘𝑛))) |
64 | 63 | feq1d 5943 |
. . . . . . . . . 10
⊢ (𝐵 = ℕ → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌)) |
65 | 64 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ↔ (𝑛 ∈ ℕ ↦ (𝐹‘𝑛)):ℕ⟶𝑌)) |
66 | 59, 65 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ⟶𝑌) |
67 | | f1ofo 6057 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐵–1-1-onto→𝑌 → 𝐹:𝐵–onto→𝑌) |
68 | 4, 67 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐵–onto→𝑌) |
69 | | dffo3 6282 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝐵–onto→𝑌 ↔ (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))) |
70 | 68, 69 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹:𝐵⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛))) |
71 | 70 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)) |
72 | 71 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)) |
73 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
74 | | rspa 2914 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝑌 ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)) |
75 | 72, 73, 74 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)) |
76 | 75 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛)) |
77 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝜑 ∧ 𝐵 = ℕ) |
78 | | nfre1 2988 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛) |
79 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ 𝐵) |
80 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝐵 = ℕ) |
81 | 79, 80 | eleqtrd 2690 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ) |
82 | 81 | adantll 746 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ) |
83 | 82 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑛 ∈ ℕ) |
84 | 60 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 = ℕ → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛)) |
85 | 84 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐴‘𝑛) = ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛)) |
86 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹‘𝑛) ∈ V |
87 | 86, 15 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) |
89 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) |
90 | 89 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) |
91 | 81, 88, 90 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) |
92 | 2 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = (𝐹‘𝑛)) |
93 | 91, 92 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛)) |
94 | 93 | 3adant3 1074 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))‘𝑛) = (𝐹‘𝑛)) |
95 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝐹‘𝑛) → 𝑦 = (𝐹‘𝑛)) |
96 | 95 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐹‘𝑛) → (𝐹‘𝑛) = 𝑦) |
97 | 96 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → (𝐹‘𝑛) = 𝑦) |
98 | 85, 94, 97 | 3eqtrrd 2649 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 = ℕ ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛)) |
99 | 98 | 3adant1l 1310 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → 𝑦 = (𝐴‘𝑛)) |
100 | | rspe 2986 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 𝑦 = (𝐴‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
101 | 83, 99, 100 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑛 ∈ 𝐵 ∧ 𝑦 = (𝐹‘𝑛)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
102 | 101 | 3exp 1256 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝑛 ∈ 𝐵 → (𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))) |
103 | 77, 78, 102 | rexlimd 3008 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = ℕ) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
104 | 103 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 𝑦 = (𝐹‘𝑛) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
105 | 76, 104 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 = ℕ) ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
106 | 105 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
107 | 66, 106 | jca 553 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 = ℕ) → (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
108 | | dffo3 6282 |
. . . . . . 7
⊢ (𝐴:ℕ–onto→𝑌 ↔ (𝐴:ℕ⟶𝑌 ∧ ∀𝑦 ∈ 𝑌 ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
109 | 107, 108 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 = ℕ) → 𝐴:ℕ–onto→𝑌) |
110 | | founiiun 38355 |
. . . . . 6
⊢ (𝐴:ℕ–onto→𝑌 → ∪ 𝑌 = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) |
111 | 109, 110 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = ℕ) → ∪ 𝑌 =
∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) |
112 | | uniun 4392 |
. . . . . . . 8
⊢ ∪ (𝑌
∪ {∅}) = (∪ 𝑌 ∪ ∪
{∅}) |
113 | 15 | unisn 4387 |
. . . . . . . . 9
⊢ ∪ {∅} = ∅ |
114 | 113 | uneq2i 3726 |
. . . . . . . 8
⊢ (∪ 𝑌
∪ ∪ {∅}) = (∪
𝑌 ∪
∅) |
115 | | un0 3919 |
. . . . . . . 8
⊢ (∪ 𝑌
∪ ∅) = ∪ 𝑌 |
116 | 112, 114,
115 | 3eqtrri 2637 |
. . . . . . 7
⊢ ∪ 𝑌 =
∪ (𝑌 ∪ {∅}) |
117 | 116 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 =
∪ (𝑌 ∪ {∅})) |
118 | 24 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ⟶(𝑌 ∪ {∅})) |
119 | | isomenndlem.b |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ⊆ ℕ) |
120 | 119 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊆ ℕ) |
121 | 52 | necon3bi 2808 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝐵 = ℕ → 𝐵 ≠ ℕ) |
122 | 121 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ≠ ℕ) |
123 | 120, 122 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ)) |
124 | | df-pss 3556 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ⊊ ℕ ↔ (𝐵 ⊆ ℕ ∧ 𝐵 ≠ ℕ)) |
125 | 123, 124 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐵 ⊊ ℕ) |
126 | | pssnel 3991 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ⊊ ℕ →
∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) |
128 | 127 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) |
129 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) |
130 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ) |
131 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑛 ∈ ℕ) |
132 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) |
133 | 23 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ ∧ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) |
134 | 131, 132,
133 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) |
135 | 134 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) |
136 | 13 | ad2antll 761 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅) |
137 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ∅ → 𝑦 = ∅) |
138 | 137 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ∅ → ∅ =
𝑦) |
139 | 138 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∅ = 𝑦) |
140 | 135, 136,
139 | 3eqtrrd 2649 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → 𝑦 = (𝐴‘𝑛)) |
141 | 130, 140,
100 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 = ∅) ∧ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵)) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
142 | 141 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
143 | 142 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
144 | 129, 78, 143 | exlimd 2074 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → (∃𝑛(𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐵) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
145 | 128, 144 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
146 | 145 | adantlr 747 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
147 | | simplll 794 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝜑) |
148 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ (𝑌 ∪ {∅})) |
149 | | elsni 4142 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {∅} → 𝑦 = ∅) |
150 | 149 | con3i 149 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑦 = ∅ → ¬
𝑦 ∈
{∅}) |
151 | 150 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → ¬ 𝑦 ∈
{∅}) |
152 | | elunnel2 38221 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 ∈ {∅}) → 𝑦 ∈ 𝑌) |
153 | 148, 151,
152 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (𝑌 ∪ {∅}) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌) |
154 | 153 | adantll 746 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ 𝑌) |
155 | 68 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐹:𝐵–onto→𝑌) |
156 | | foelrni 6154 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐵–onto→𝑌 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦) |
157 | 155, 73, 156 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦) |
158 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝜑 ∧ 𝑦 ∈ 𝑌) |
159 | 119 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ℕ) |
160 | 159 | 3adant3 1074 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑛 ∈ ℕ) |
161 | 159, 87, 133 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) |
162 | 161, 3 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐴‘𝑛) = (𝐹‘𝑛)) |
163 | 162 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐴‘𝑛) = (𝐹‘𝑛)) |
164 | | simp3 1056 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → (𝐹‘𝑛) = 𝑦) |
165 | 163, 164 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → 𝑦 = (𝐴‘𝑛)) |
166 | 160, 165,
100 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵 ∧ (𝐹‘𝑛) = 𝑦) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
167 | 166 | 3exp 1256 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))) |
168 | 167 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑛 ∈ 𝐵 → ((𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)))) |
169 | 158, 78, 168 | rexlimd 3008 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (∃𝑛 ∈ 𝐵 (𝐹‘𝑛) = 𝑦 → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
170 | 157, 169 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
171 | 147, 154,
170 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) ∧ ¬ 𝑦 = ∅) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
172 | 146, 171 | pm2.61dan 828 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝐵 = ℕ) ∧ 𝑦 ∈ (𝑌 ∪ {∅})) → ∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
173 | 172 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛)) |
174 | 118, 173 | jca 553 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
175 | | dffo3 6282 |
. . . . . . . 8
⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) ↔ (𝐴:ℕ⟶(𝑌 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑌 ∪ {∅})∃𝑛 ∈ ℕ 𝑦 = (𝐴‘𝑛))) |
176 | 174, 175 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → 𝐴:ℕ–onto→(𝑌 ∪ {∅})) |
177 | | founiiun 38355 |
. . . . . . 7
⊢ (𝐴:ℕ–onto→(𝑌 ∪ {∅}) → ∪ (𝑌
∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) |
178 | 176, 177 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ (𝑌
∪ {∅}) = ∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) |
179 | 117, 178 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐵 = ℕ) → ∪ 𝑌 =
∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) |
180 | 111, 179 | pm2.61dan 828 |
. . . 4
⊢ (𝜑 → ∪ 𝑌 =
∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) |
181 | 180 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (𝑂‘∪ 𝑌) = (𝑂‘∪
𝑛 ∈ ℕ (𝐴‘𝑛))) |
182 | | uncom 3719 |
. . . . . . . . 9
⊢ ((ℕ
∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵)) |
183 | 182 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (ℕ ∖ 𝐵))) |
184 | | undif 4001 |
. . . . . . . . 9
⊢ (𝐵 ⊆ ℕ ↔ (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ) |
185 | 119, 184 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∪ (ℕ ∖ 𝐵)) = ℕ) |
186 | 183, 185 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → ((ℕ ∖ 𝐵) ∪ 𝐵) = ℕ) |
187 | 186 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → ℕ = ((ℕ
∖ 𝐵) ∪ 𝐵)) |
188 | 187 | mpteq1d 4666 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) |
189 | 188 | fveq2d 6107 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))) =
(Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))))) |
190 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑛𝜑 |
191 | | difexg 4735 |
. . . . . . 7
⊢ (ℕ
∈ V → (ℕ ∖ 𝐵) ∈ V) |
192 | 32, 191 | ax-mp 5 |
. . . . . 6
⊢ (ℕ
∖ 𝐵) ∈
V |
193 | 192 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ℕ ∖ 𝐵) ∈ V) |
194 | 32 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℕ ∈
V) |
195 | 194, 119 | ssexd 4733 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
196 | | incom 3767 |
. . . . . . 7
⊢ ((ℕ
∖ 𝐵) ∩ 𝐵) = (𝐵 ∩ (ℕ ∖ 𝐵)) |
197 | | disjdif 3992 |
. . . . . . 7
⊢ (𝐵 ∩ (ℕ ∖ 𝐵)) = ∅ |
198 | 196, 197 | eqtri 2632 |
. . . . . 6
⊢ ((ℕ
∖ 𝐵) ∩ 𝐵) = ∅ |
199 | 198 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((ℕ ∖ 𝐵) ∩ 𝐵) = ∅) |
200 | | simpl 472 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝜑) |
201 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → 𝑛 ∈ ℕ) |
202 | 201 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → 𝑛 ∈ ℕ) |
203 | | isomenndlem.o |
. . . . . . . 8
⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
204 | 203 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
205 | 31 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋) |
206 | 204, 205 | ffvelrnd 6268 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞)) |
207 | 200, 202,
206 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞)) |
208 | 159, 206 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝑂‘(𝐴‘𝑛)) ∈ (0[,]+∞)) |
209 | 190, 193,
195, 199, 207, 208 | sge0splitmpt 39304 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ((ℕ ∖ 𝐵) ∪ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) =
((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +𝑒
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))) |
210 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))) |
211 | 208, 210 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))):𝐵⟶(0[,]+∞)) |
212 | 195, 211 | sge0xrcl 39278 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) ∈
ℝ*) |
213 | 212 | xaddid2d 38476 |
. . . . 5
⊢ (𝜑 → (0 +𝑒
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) =
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) |
214 | 87 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) ∈ V) |
215 | 202, 214,
133 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) |
216 | | eldifn 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (ℕ ∖ 𝐵) → ¬ 𝑛 ∈ 𝐵) |
217 | 216 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → ¬ 𝑛 ∈ 𝐵) |
218 | 217 | iffalsed 4047 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅) = ∅) |
219 | 215, 218 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝐴‘𝑛) = ∅) |
220 | 219 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = (𝑂‘∅)) |
221 | | isomenndlem.o0 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘∅) = 0) |
222 | 200, 221 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘∅) = 0) |
223 | 220, 222 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐵)) → (𝑂‘(𝐴‘𝑛)) = 0) |
224 | 223 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛))) = (𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) |
225 | 224 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) =
(Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0))) |
226 | 190, 193 | sge0z 39268 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ 0)) = 0) |
227 | 225, 226 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) = 0) |
228 | 227 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 →
((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +𝑒
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) = (0 +𝑒
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))))) |
229 | 203, 25 | feqresmpt 6160 |
. . . . . . 7
⊢ (𝜑 → (𝑂 ↾ 𝑌) = (𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))) |
230 | 229 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑂 ↾ 𝑌)) =
(Σ^‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦)))) |
231 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑦𝜑 |
232 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = (𝐴‘𝑛) → (𝑂‘𝑦) = (𝑂‘(𝐴‘𝑛))) |
233 | 162 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) = (𝐴‘𝑛)) |
234 | 203 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
235 | 25 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝒫 𝑋) |
236 | 234, 235 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑂‘𝑦) ∈ (0[,]+∞)) |
237 | 231, 190,
232, 195, 4, 233, 236 | sge0f1o 39275 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑦 ∈ 𝑌 ↦ (𝑂‘𝑦))) =
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) |
238 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛)))) =
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) |
239 | 230, 237,
238 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑂 ↾ 𝑌)) =
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) |
240 | 213, 228,
239 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 →
((Σ^‘(𝑛 ∈ (ℕ ∖ 𝐵) ↦ (𝑂‘(𝐴‘𝑛)))) +𝑒
(Σ^‘(𝑛 ∈ 𝐵 ↦ (𝑂‘(𝐴‘𝑛))))) =
(Σ^‘(𝑂 ↾ 𝑌))) |
241 | 189, 209,
240 | 3eqtrrd 2649 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑂 ↾ 𝑌)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛))))) |
242 | 181, 241 | breq12d 4596 |
. 2
⊢ (𝜑 → ((𝑂‘∪ 𝑌) ≤
(Σ^‘(𝑂 ↾ 𝑌)) ↔ (𝑂‘∪
𝑛 ∈ ℕ (𝐴‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐴‘𝑛)))))) |
243 | 49, 242 | mpbird 246 |
1
⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤
(Σ^‘(𝑂 ↾ 𝑌))) |