Step | Hyp | Ref
| Expression |
1 | | sge0fodjrnlem.k |
. . . 4
⊢
Ⅎ𝑘𝜑 |
2 | | sge0fodjrnlem.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
3 | | sge0fodjrnlem.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐶–onto→𝐴) |
4 | | fornex 7177 |
. . . . 5
⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V)) |
5 | 2, 3, 4 | sylc 65 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ V) |
6 | | difssd 3771 |
. . . 4
⊢ (𝜑 → (𝐴 ∖ {∅}) ⊆ 𝐴) |
7 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝜑) |
8 | 6 | sselda 3636 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝑘 ∈ 𝐴) |
9 | | sge0fodjrnlem.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
10 | 7, 8, 9 | syl2anc 694 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝐵 ∈
(0[,]+∞)) |
11 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝜑) |
12 | | dfin4 3900 |
. . . . . . . . . 10
⊢ (𝐴 ∩ {∅}) = (𝐴 ∖ (𝐴 ∖ {∅})) |
13 | 12 | eqcomi 2660 |
. . . . . . . . 9
⊢ (𝐴 ∖ (𝐴 ∖ {∅})) = (𝐴 ∩ {∅}) |
14 | | inss2 3867 |
. . . . . . . . 9
⊢ (𝐴 ∩ {∅}) ⊆
{∅} |
15 | 13, 14 | eqsstri 3668 |
. . . . . . . 8
⊢ (𝐴 ∖ (𝐴 ∖ {∅})) ⊆
{∅} |
16 | | id 22 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) |
17 | 15, 16 | sseldi 3634 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈
{∅}) |
18 | | elsni 4227 |
. . . . . . 7
⊢ (𝑘 ∈ {∅} → 𝑘 = ∅) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 = ∅) |
20 | 19 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝑘 = ∅) |
21 | | sge0fodjrnlem.b0 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) |
22 | 11, 20, 21 | syl2anc 694 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝐵 = 0) |
23 | 1, 5, 6, 10, 22 | sge0ss 40947 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) =
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵))) |
24 | 23 | eqcomd 2657 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵))) |
25 | | sge0fodjrnlem.n |
. . 3
⊢
Ⅎ𝑛𝜑 |
26 | | sge0fodjrnlem.bd |
. . 3
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
27 | | difexg 4841 |
. . . 4
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∖ 𝑍) ∈ V) |
28 | 2, 27 | syl 17 |
. . 3
⊢ (𝜑 → (𝐶 ∖ 𝑍) ∈ V) |
29 | | eqid 2651 |
. . . . 5
⊢ (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) |
30 | | fof 6153 |
. . . . . . 7
⊢ (𝐹:𝐶–onto→𝐴 → 𝐹:𝐶⟶𝐴) |
31 | 3, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
32 | 31 | ffvelrnda 6399 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
33 | | sge0fodjrnlem.dj |
. . . . 5
⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛)) |
34 | | fveq2 6229 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
35 | 34 | neeq1d 2882 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ≠ ∅ ↔ (𝐹‘𝑛) ≠ ∅)) |
36 | 35 | cbvrabv 3230 |
. . . . 5
⊢ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} = {𝑛 ∈ 𝐶 ∣ (𝐹‘𝑛) ≠ ∅} |
37 | 34 | cbvmptv 4783 |
. . . . . . 7
⊢ (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) |
38 | 37 | rneqi 5384 |
. . . . . 6
⊢ ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) |
39 | 38 | difeq1i 3757 |
. . . . 5
⊢ (ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}) = (ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ∖ {∅}) |
40 | 25, 29, 32, 33, 36, 39 | disjf1o 39692 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})) |
41 | 31 | feqmptd 6288 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))) |
42 | | difssd 3771 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 ∖ 𝑍) ⊆ 𝐶) |
43 | 42 | sselda 3636 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶) |
44 | | eldifi 3765 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ 𝐶) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝐶) |
46 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) = ∅) |
47 | | fvex 6239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹‘𝑛) ∈ V |
48 | 47 | elsn 4225 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑛) ∈ {∅} ↔ (𝐹‘𝑛) = ∅) |
49 | 46, 48 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ∈ {∅}) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝐹‘𝑛) ∈ {∅}) |
51 | 45, 50 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})) |
52 | 51 | adantll 750 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})) |
53 | 31 | ffnd 6084 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 Fn 𝐶) |
54 | | elpreima 6377 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 Fn 𝐶 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))) |
56 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))) |
57 | 52, 56 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ (◡𝐹 “ {∅})) |
58 | | sge0fodjrnlem.z |
. . . . . . . . . . . . . . 15
⊢ 𝑍 = (◡𝐹 “ {∅}) |
59 | 57, 58 | syl6eleqr 2741 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝑍) |
60 | | eldifn 3766 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ¬ 𝑛 ∈ 𝑍) |
61 | 60 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → ¬ 𝑛 ∈ 𝑍) |
62 | 59, 61 | pm2.65da 599 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ¬ (𝐹‘𝑛) = ∅) |
63 | 62 | neqned 2830 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) ≠ ∅) |
64 | 43, 63 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅)) |
65 | 35 | elrab 3396 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅)) |
66 | 64, 65 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) |
67 | 66 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
68 | 65 | simplbi 475 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ 𝐶) |
69 | 68 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ 𝐶) |
70 | 58 | eleq2i 2722 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (◡𝐹 “ {∅})) |
71 | 70 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (◡𝐹 “ {∅})) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (◡𝐹 “ {∅})) |
73 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))) |
74 | 72, 73 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})) |
75 | 74 | simprd 478 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ {∅}) |
76 | | elsni 4227 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑛) ∈ {∅} → (𝐹‘𝑛) = ∅) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅) |
78 | 77 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅) |
79 | 65 | simprbi 479 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → (𝐹‘𝑛) ≠ ∅) |
80 | 79 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≠ ∅) |
81 | 80 | neneqd 2828 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → ¬ (𝐹‘𝑛) = ∅) |
82 | 78, 81 | pm2.65da 599 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → ¬ 𝑛 ∈ 𝑍) |
83 | 69, 82 | eldifd 3618 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ (𝐶 ∖ 𝑍)) |
84 | 83 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍))) |
85 | 25, 84 | ralrimi 2986 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍)) |
86 | | dfss3 3625 |
. . . . . . . . . . 11
⊢ ({𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍) ↔ ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍)) |
87 | 85, 86 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍)) |
88 | 87 | sseld 3635 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍))) |
89 | 67, 88 | impbid 202 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
90 | 25, 89 | alrimi 2120 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
91 | | dfcleq 2645 |
. . . . . . 7
⊢ ((𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
92 | 90, 91 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) |
93 | 41, 92 | reseq12d 5429 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)) = ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
94 | 41, 37 | syl6eqr 2703 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚))) |
95 | 94 | eqcomd 2657 |
. . . . . . . 8
⊢ (𝜑 → (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = 𝐹) |
96 | 95 | rneqd 5385 |
. . . . . . 7
⊢ (𝜑 → ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran 𝐹) |
97 | | forn 6156 |
. . . . . . . 8
⊢ (𝐹:𝐶–onto→𝐴 → ran 𝐹 = 𝐴) |
98 | 3, 97 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 = 𝐴) |
99 | 96, 98 | eqtr2d 2686 |
. . . . . 6
⊢ (𝜑 → 𝐴 = ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚))) |
100 | 99 | difeq1d 3760 |
. . . . 5
⊢ (𝜑 → (𝐴 ∖ {∅}) = (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})) |
101 | 93, 92, 100 | f1oeq123d 6171 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}) ↔ ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))) |
102 | 40, 101 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅})) |
103 | | fvres 6245 |
. . . . 5
⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛)) |
104 | 103 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛)) |
105 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝜑) |
106 | | sge0fodjrnlem.fng |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
107 | 105, 43, 106 | syl2anc 694 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) = 𝐺) |
108 | 104, 107 | eqtrd 2685 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = 𝐺) |
109 | 1, 25, 26, 28, 102, 108, 10 | sge0f1o 40917 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷))) |
110 | 106 | eqcomd 2657 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 = (𝐹‘𝑛)) |
111 | 110, 32 | eqeltrd 2730 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴) |
112 | 105, 43, 111 | syl2anc 694 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐺 ∈ 𝐴) |
113 | 112 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝐺 ∈ 𝐴)) |
114 | 113 | imdistani 726 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝜑 ∧ 𝐺 ∈ 𝐴)) |
115 | | nfcv 2793 |
. . . . 5
⊢
Ⅎ𝑘𝐺 |
116 | | nfv 1883 |
. . . . . . 7
⊢
Ⅎ𝑘 𝐺 ∈ 𝐴 |
117 | 1, 116 | nfan 1868 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝐺 ∈ 𝐴) |
118 | | nfv 1883 |
. . . . . 6
⊢
Ⅎ𝑘 𝐷 ∈
(0[,]+∞) |
119 | 117, 118 | nfim 1865 |
. . . . 5
⊢
Ⅎ𝑘((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)) |
120 | | eleq1 2718 |
. . . . . . 7
⊢ (𝑘 = 𝐺 → (𝑘 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴)) |
121 | 120 | anbi2d 740 |
. . . . . 6
⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝐺 ∈ 𝐴))) |
122 | 26 | eleq1d 2715 |
. . . . . 6
⊢ (𝑘 = 𝐺 → (𝐵 ∈ (0[,]+∞) ↔ 𝐷 ∈
(0[,]+∞))) |
123 | 121, 122 | imbi12d 333 |
. . . . 5
⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)))) |
124 | 115, 119,
123, 9 | vtoclgf 3295 |
. . . 4
⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))) |
125 | 112, 114,
124 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐷 ∈ (0[,]+∞)) |
126 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝜑) |
127 | | eldifi 3765 |
. . . . . 6
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶) |
128 | 127 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝐶) |
129 | 126, 128,
111 | syl2anc 694 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 ∈ 𝐴) |
130 | | dfin4 3900 |
. . . . . . . . 9
⊢ (𝑍 ∩ 𝐶) = (𝑍 ∖ (𝑍 ∖ 𝐶)) |
131 | | difss 3770 |
. . . . . . . . 9
⊢ (𝑍 ∖ (𝑍 ∖ 𝐶)) ⊆ 𝑍 |
132 | 130, 131 | eqsstri 3668 |
. . . . . . . 8
⊢ (𝑍 ∩ 𝐶) ⊆ 𝑍 |
133 | | inss2 3867 |
. . . . . . . . . 10
⊢ (𝐶 ∩ 𝑍) ⊆ 𝑍 |
134 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) |
135 | | dfin4 3900 |
. . . . . . . . . . . 12
⊢ (𝐶 ∩ 𝑍) = (𝐶 ∖ (𝐶 ∖ 𝑍)) |
136 | 135 | eqcomi 2660 |
. . . . . . . . . . 11
⊢ (𝐶 ∖ (𝐶 ∖ 𝑍)) = (𝐶 ∩ 𝑍) |
137 | 134, 136 | syl6eleq 2740 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∩ 𝑍)) |
138 | 133, 137 | sseldi 3634 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍) |
139 | 138, 127 | elind 3831 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝑍 ∩ 𝐶)) |
140 | 132, 139 | sseldi 3634 |
. . . . . . 7
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍) |
141 | 140 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝑍) |
142 | 77 | eqcomd 2657 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∅ = (𝐹‘𝑛)) |
143 | | simpl 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝜑) |
144 | 74 | simpld 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝐶) |
145 | 143, 144,
106 | syl2anc 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = 𝐺) |
146 | 142, 145 | eqtr2d 2686 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐺 = ∅) |
147 | 126, 141,
146 | syl2anc 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 = ∅) |
148 | 126, 147 | jca 553 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → (𝜑 ∧ 𝐺 = ∅)) |
149 | | nfv 1883 |
. . . . . . 7
⊢
Ⅎ𝑘 𝐺 = ∅ |
150 | 1, 149 | nfan 1868 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝐺 = ∅) |
151 | | nfv 1883 |
. . . . . 6
⊢
Ⅎ𝑘 𝐷 = 0 |
152 | 150, 151 | nfim 1865 |
. . . . 5
⊢
Ⅎ𝑘((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0) |
153 | | eqeq1 2655 |
. . . . . . 7
⊢ (𝑘 = 𝐺 → (𝑘 = ∅ ↔ 𝐺 = ∅)) |
154 | 153 | anbi2d 740 |
. . . . . 6
⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 = ∅) ↔ (𝜑 ∧ 𝐺 = ∅))) |
155 | 26 | eqeq1d 2653 |
. . . . . 6
⊢ (𝑘 = 𝐺 → (𝐵 = 0 ↔ 𝐷 = 0)) |
156 | 154, 155 | imbi12d 333 |
. . . . 5
⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) ↔ ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0))) |
157 | 115, 152,
156, 21 | vtoclgf 3295 |
. . . 4
⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)) |
158 | 129, 148,
157 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐷 = 0) |
159 | 25, 2, 42, 125, 158 | sge0ss 40947 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |
160 | 24, 109, 159 | 3eqtrd 2689 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |