Step | Hyp | Ref
| Expression |
1 | | sge0fodjrnlem.k |
. . . 4
⊢
Ⅎ𝑘𝜑 |
2 | | sge0fodjrnlem.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
3 | | sge0fodjrnlem.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐶–onto→𝐴) |
4 | | fornex 7135 |
. . . . 5
⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V)) |
5 | 2, 3, 4 | sylc 65 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ V) |
6 | | difssd 3738 |
. . . 4
⊢ (𝜑 → (𝐴 ∖ {∅}) ⊆ 𝐴) |
7 | | simpl 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝜑) |
8 | 6 | sselda 3603 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝑘 ∈ 𝐴) |
9 | | sge0fodjrnlem.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
10 | 7, 8, 9 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝐵 ∈
(0[,]+∞)) |
11 | | simpl 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝜑) |
12 | | dfin4 3867 |
. . . . . . . . . 10
⊢ (𝐴 ∩ {∅}) = (𝐴 ∖ (𝐴 ∖ {∅})) |
13 | 12 | eqcomi 2631 |
. . . . . . . . 9
⊢ (𝐴 ∖ (𝐴 ∖ {∅})) = (𝐴 ∩ {∅}) |
14 | | inss2 3834 |
. . . . . . . . 9
⊢ (𝐴 ∩ {∅}) ⊆
{∅} |
15 | 13, 14 | eqsstri 3635 |
. . . . . . . 8
⊢ (𝐴 ∖ (𝐴 ∖ {∅})) ⊆
{∅} |
16 | | id 22 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) |
17 | 15, 16 | sseldi 3601 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈
{∅}) |
18 | | elsni 4194 |
. . . . . . 7
⊢ (𝑘 ∈ {∅} → 𝑘 = ∅) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 = ∅) |
20 | 19 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝑘 = ∅) |
21 | | sge0fodjrnlem.b0 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) |
22 | 11, 20, 21 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝐵 = 0) |
23 | 1, 5, 6, 10, 22 | sge0ss 40629 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) =
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵))) |
24 | 23 | eqcomd 2628 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵))) |
25 | | sge0fodjrnlem.n |
. . 3
⊢
Ⅎ𝑛𝜑 |
26 | | sge0fodjrnlem.bd |
. . 3
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
27 | | difexg 4808 |
. . . 4
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∖ 𝑍) ∈ V) |
28 | 2, 27 | syl 17 |
. . 3
⊢ (𝜑 → (𝐶 ∖ 𝑍) ∈ V) |
29 | | eqid 2622 |
. . . . 5
⊢ (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) |
30 | | fof 6115 |
. . . . . . 7
⊢ (𝐹:𝐶–onto→𝐴 → 𝐹:𝐶⟶𝐴) |
31 | 3, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
32 | 31 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
33 | | sge0fodjrnlem.dj |
. . . . 5
⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛)) |
34 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
35 | 34 | neeq1d 2853 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ≠ ∅ ↔ (𝐹‘𝑛) ≠ ∅)) |
36 | 35 | cbvrabv 3199 |
. . . . 5
⊢ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} = {𝑛 ∈ 𝐶 ∣ (𝐹‘𝑛) ≠ ∅} |
37 | 34 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) |
38 | 37 | rneqi 5352 |
. . . . . 6
⊢ ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) |
39 | 38 | difeq1i 3724 |
. . . . 5
⊢ (ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}) = (ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ∖ {∅}) |
40 | 25, 29, 32, 33, 36, 39 | disjf1o 39378 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})) |
41 | 31 | feqmptd 6249 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))) |
42 | | difssd 3738 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 ∖ 𝑍) ⊆ 𝐶) |
43 | 42 | sselda 3603 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶) |
44 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ 𝐶) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝐶) |
46 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) = ∅) |
47 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹‘𝑛) ∈ V |
48 | 47 | elsn 4192 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑛) ∈ {∅} ↔ (𝐹‘𝑛) = ∅) |
49 | 46, 48 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ∈ {∅}) |
50 | 49 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝐹‘𝑛) ∈ {∅}) |
51 | 45, 50 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})) |
52 | 51 | adantll 750 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})) |
53 | 31 | ffnd 6046 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 Fn 𝐶) |
54 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . 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 2712 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝑍) |
60 | | eldifn 3733 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ¬ 𝑛 ∈ 𝑍) |
61 | 60 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → ¬ 𝑛 ∈ 𝑍) |
62 | 59, 61 | pm2.65da 600 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ¬ (𝐹‘𝑛) = ∅) |
63 | 62 | neqned 2801 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) ≠ ∅) |
64 | 43, 63 | jca 554 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅)) |
65 | 35 | elrab 3363 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅)) |
66 | 64, 65 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) |
67 | 66 | ex 450 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
68 | 65 | simplbi 476 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ 𝐶) |
69 | 68 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ 𝐶) |
70 | 58 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (◡𝐹 “ {∅})) |
71 | 70 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (◡𝐹 “ {∅})) |
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (◡𝐹 “ {∅})) |
73 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))) |
74 | 72, 73 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})) |
75 | 74 | simprd 479 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ {∅}) |
76 | | elsni 4194 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑛) ∈ {∅} → (𝐹‘𝑛) = ∅) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅) |
78 | 77 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅) |
79 | 65 | simprbi 480 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → (𝐹‘𝑛) ≠ ∅) |
80 | 79 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≠ ∅) |
81 | 80 | neneqd 2799 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → ¬ (𝐹‘𝑛) = ∅) |
82 | 78, 81 | pm2.65da 600 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → ¬ 𝑛 ∈ 𝑍) |
83 | 69, 82 | eldifd 3585 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ (𝐶 ∖ 𝑍)) |
84 | 83 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍))) |
85 | 25, 84 | ralrimi 2957 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍)) |
86 | | dfss3 3592 |
. . . . . . . . . . 11
⊢ ({𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍) ↔ ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍)) |
87 | 85, 86 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍)) |
88 | 87 | sseld 3602 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍))) |
89 | 67, 88 | impbid 202 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
90 | 25, 89 | alrimi 2082 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
91 | | dfcleq 2616 |
. . . . . . 7
⊢ ((𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
92 | 90, 91 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) |
93 | 41, 92 | reseq12d 5397 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)) = ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
94 | 41, 37 | syl6eqr 2674 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚))) |
95 | 94 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝜑 → (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = 𝐹) |
96 | 95 | rneqd 5353 |
. . . . . . 7
⊢ (𝜑 → ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran 𝐹) |
97 | | forn 6118 |
. . . . . . . 8
⊢ (𝐹:𝐶–onto→𝐴 → ran 𝐹 = 𝐴) |
98 | 3, 97 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 = 𝐴) |
99 | 96, 98 | eqtr2d 2657 |
. . . . . 6
⊢ (𝜑 → 𝐴 = ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚))) |
100 | 99 | difeq1d 3727 |
. . . . 5
⊢ (𝜑 → (𝐴 ∖ {∅}) = (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})) |
101 | 93, 92, 100 | f1oeq123d 6133 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}) ↔ ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))) |
102 | 40, 101 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅})) |
103 | | fvres 6207 |
. . . . 5
⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛)) |
104 | 103 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛)) |
105 | | simpl 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝜑) |
106 | | sge0fodjrnlem.fng |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
107 | 105, 43, 106 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) = 𝐺) |
108 | 104, 107 | eqtrd 2656 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = 𝐺) |
109 | 1, 25, 26, 28, 102, 108, 10 | sge0f1o 40599 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷))) |
110 | 106 | eqcomd 2628 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 = (𝐹‘𝑛)) |
111 | 110, 32 | eqeltrd 2701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴) |
112 | 105, 43, 111 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐺 ∈ 𝐴) |
113 | 112 | ex 450 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝐺 ∈ 𝐴)) |
114 | 113 | imdistani 726 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝜑 ∧ 𝐺 ∈ 𝐴)) |
115 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑘𝐺 |
116 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑘 𝐺 ∈ 𝐴 |
117 | 1, 116 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝐺 ∈ 𝐴) |
118 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑘 𝐷 ∈
(0[,]+∞) |
119 | 117, 118 | nfim 1825 |
. . . . 5
⊢
Ⅎ𝑘((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)) |
120 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑘 = 𝐺 → (𝑘 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴)) |
121 | 120 | anbi2d 740 |
. . . . . 6
⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝐺 ∈ 𝐴))) |
122 | 26 | eleq1d 2686 |
. . . . . 6
⊢ (𝑘 = 𝐺 → (𝐵 ∈ (0[,]+∞) ↔ 𝐷 ∈
(0[,]+∞))) |
123 | 121, 122 | imbi12d 334 |
. . . . 5
⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)))) |
124 | 115, 119,
123, 9 | vtoclgf 3264 |
. . . 4
⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))) |
125 | 112, 114,
124 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐷 ∈ (0[,]+∞)) |
126 | | simpl 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝜑) |
127 | | eldifi 3732 |
. . . . . 6
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶) |
128 | 127 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝐶) |
129 | 126, 128,
111 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 ∈ 𝐴) |
130 | | dfin4 3867 |
. . . . . . . . 9
⊢ (𝑍 ∩ 𝐶) = (𝑍 ∖ (𝑍 ∖ 𝐶)) |
131 | | difss 3737 |
. . . . . . . . 9
⊢ (𝑍 ∖ (𝑍 ∖ 𝐶)) ⊆ 𝑍 |
132 | 130, 131 | eqsstri 3635 |
. . . . . . . 8
⊢ (𝑍 ∩ 𝐶) ⊆ 𝑍 |
133 | | inss2 3834 |
. . . . . . . . . 10
⊢ (𝐶 ∩ 𝑍) ⊆ 𝑍 |
134 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) |
135 | | dfin4 3867 |
. . . . . . . . . . . 12
⊢ (𝐶 ∩ 𝑍) = (𝐶 ∖ (𝐶 ∖ 𝑍)) |
136 | 135 | eqcomi 2631 |
. . . . . . . . . . 11
⊢ (𝐶 ∖ (𝐶 ∖ 𝑍)) = (𝐶 ∩ 𝑍) |
137 | 134, 136 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∩ 𝑍)) |
138 | 133, 137 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍) |
139 | 138, 127 | elind 3798 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝑍 ∩ 𝐶)) |
140 | 132, 139 | sseldi 3601 |
. . . . . . 7
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍) |
141 | 140 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝑍) |
142 | 77 | eqcomd 2628 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∅ = (𝐹‘𝑛)) |
143 | | simpl 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝜑) |
144 | 74 | simpld 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝐶) |
145 | 143, 144,
106 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = 𝐺) |
146 | 142, 145 | eqtr2d 2657 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐺 = ∅) |
147 | 126, 141,
146 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 = ∅) |
148 | 126, 147 | jca 554 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → (𝜑 ∧ 𝐺 = ∅)) |
149 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑘 𝐺 = ∅ |
150 | 1, 149 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝐺 = ∅) |
151 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑘 𝐷 = 0 |
152 | 150, 151 | nfim 1825 |
. . . . 5
⊢
Ⅎ𝑘((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0) |
153 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑘 = 𝐺 → (𝑘 = ∅ ↔ 𝐺 = ∅)) |
154 | 153 | anbi2d 740 |
. . . . . 6
⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 = ∅) ↔ (𝜑 ∧ 𝐺 = ∅))) |
155 | 26 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑘 = 𝐺 → (𝐵 = 0 ↔ 𝐷 = 0)) |
156 | 154, 155 | imbi12d 334 |
. . . . 5
⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) ↔ ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0))) |
157 | 115, 152,
156, 21 | vtoclgf 3264 |
. . . 4
⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)) |
158 | 129, 148,
157 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐷 = 0) |
159 | 25, 2, 42, 125, 158 | sge0ss 40629 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |
160 | 24, 109, 159 | 3eqtrd 2660 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |