| Step | Hyp | Ref
| Expression |
| 1 | | sge0fodjrnlem.k |
. . . 4
⊢
Ⅎ𝑘𝜑 |
| 2 | | sge0fodjrnlem.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
| 3 | | sge0fodjrnlem.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐶–onto→𝐴) |
| 4 | | focdmex 7980 |
. . . . 5
⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V)) |
| 5 | 2, 3, 4 | sylc 65 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ V) |
| 6 | | difssd 4137 |
. . . 4
⊢ (𝜑 → (𝐴 ∖ {∅}) ⊆ 𝐴) |
| 7 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝜑) |
| 8 | 6 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝑘 ∈ 𝐴) |
| 9 | | sge0fodjrnlem.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
| 10 | 7, 8, 9 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝐵 ∈
(0[,]+∞)) |
| 11 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝜑) |
| 12 | | dfin4 4278 |
. . . . . . . . . 10
⊢ (𝐴 ∩ {∅}) = (𝐴 ∖ (𝐴 ∖ {∅})) |
| 13 | 12 | eqcomi 2746 |
. . . . . . . . 9
⊢ (𝐴 ∖ (𝐴 ∖ {∅})) = (𝐴 ∩ {∅}) |
| 14 | | inss2 4238 |
. . . . . . . . 9
⊢ (𝐴 ∩ {∅}) ⊆
{∅} |
| 15 | 13, 14 | eqsstri 4030 |
. . . . . . . 8
⊢ (𝐴 ∖ (𝐴 ∖ {∅})) ⊆
{∅} |
| 16 | | id 22 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) |
| 17 | 15, 16 | sselid 3981 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈
{∅}) |
| 18 | | elsni 4643 |
. . . . . . 7
⊢ (𝑘 ∈ {∅} → 𝑘 = ∅) |
| 19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 = ∅) |
| 20 | 19 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝑘 = ∅) |
| 21 | | sge0fodjrnlem.b0 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) |
| 22 | 11, 20, 21 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝐵 = 0) |
| 23 | 1, 5, 6, 10, 22 | sge0ss 46427 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) =
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵))) |
| 24 | 23 | eqcomd 2743 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵))) |
| 25 | | sge0fodjrnlem.n |
. . 3
⊢
Ⅎ𝑛𝜑 |
| 26 | | sge0fodjrnlem.bd |
. . 3
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
| 27 | 2 | difexd 5331 |
. . 3
⊢ (𝜑 → (𝐶 ∖ 𝑍) ∈ V) |
| 28 | | eqid 2737 |
. . . . 5
⊢ (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) |
| 29 | | fof 6820 |
. . . . . . 7
⊢ (𝐹:𝐶–onto→𝐴 → 𝐹:𝐶⟶𝐴) |
| 30 | 3, 29 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
| 31 | 30 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
| 32 | | sge0fodjrnlem.dj |
. . . . 5
⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛)) |
| 33 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
| 34 | 33 | neeq1d 3000 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ≠ ∅ ↔ (𝐹‘𝑛) ≠ ∅)) |
| 35 | 34 | cbvrabv 3447 |
. . . . 5
⊢ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} = {𝑛 ∈ 𝐶 ∣ (𝐹‘𝑛) ≠ ∅} |
| 36 | 33 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) |
| 37 | 36 | rneqi 5948 |
. . . . . 6
⊢ ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) |
| 38 | 37 | difeq1i 4122 |
. . . . 5
⊢ (ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}) = (ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ∖ {∅}) |
| 39 | 25, 28, 31, 32, 35, 38 | disjf1o 45196 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})) |
| 40 | 30 | feqmptd 6977 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))) |
| 41 | | difssd 4137 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 ∖ 𝑍) ⊆ 𝐶) |
| 42 | 41 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶) |
| 43 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ 𝐶) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝐶) |
| 45 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) = ∅) |
| 46 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹‘𝑛) ∈ V |
| 47 | 46 | elsn 4641 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑛) ∈ {∅} ↔ (𝐹‘𝑛) = ∅) |
| 48 | 45, 47 | sylibr 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ∈ {∅}) |
| 49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝐹‘𝑛) ∈ {∅}) |
| 50 | 44, 49 | jca 511 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})) |
| 51 | 50 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})) |
| 52 | 30 | ffnd 6737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 Fn 𝐶) |
| 53 | | elpreima 7078 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 Fn 𝐶 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))) |
| 54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))) |
| 55 | 54 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))) |
| 56 | 51, 55 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ (◡𝐹 “ {∅})) |
| 57 | | sge0fodjrnlem.z |
. . . . . . . . . . . . . . 15
⊢ 𝑍 = (◡𝐹 “ {∅}) |
| 58 | 56, 57 | eleqtrrdi 2852 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝑍) |
| 59 | | eldifn 4132 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ¬ 𝑛 ∈ 𝑍) |
| 60 | 59 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → ¬ 𝑛 ∈ 𝑍) |
| 61 | 58, 60 | pm2.65da 817 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ¬ (𝐹‘𝑛) = ∅) |
| 62 | 61 | neqned 2947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) ≠ ∅) |
| 63 | 42, 62 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅)) |
| 64 | 34 | elrab 3692 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅)) |
| 65 | 63, 64 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) |
| 66 | 65 | ex 412 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
| 67 | 64 | simplbi 497 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ 𝐶) |
| 68 | 67 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ 𝐶) |
| 69 | 57 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (◡𝐹 “ {∅})) |
| 70 | 69 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (◡𝐹 “ {∅})) |
| 71 | 70 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (◡𝐹 “ {∅})) |
| 72 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))) |
| 73 | 71, 72 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})) |
| 74 | 73 | simprd 495 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ {∅}) |
| 75 | | elsni 4643 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑛) ∈ {∅} → (𝐹‘𝑛) = ∅) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅) |
| 77 | 76 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅) |
| 78 | 64 | simprbi 496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → (𝐹‘𝑛) ≠ ∅) |
| 79 | 78 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≠ ∅) |
| 80 | 79 | neneqd 2945 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → ¬ (𝐹‘𝑛) = ∅) |
| 81 | 77, 80 | pm2.65da 817 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → ¬ 𝑛 ∈ 𝑍) |
| 82 | 68, 81 | eldifd 3962 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ (𝐶 ∖ 𝑍)) |
| 83 | 82 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍))) |
| 84 | 25, 83 | ralrimi 3257 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍)) |
| 85 | | dfss3 3972 |
. . . . . . . . . . 11
⊢ ({𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍) ↔ ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍)) |
| 86 | 84, 85 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍)) |
| 87 | 86 | sseld 3982 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍))) |
| 88 | 66, 87 | impbid 212 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
| 89 | 25, 88 | alrimi 2213 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
| 90 | | dfcleq 2730 |
. . . . . . 7
⊢ ((𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
| 91 | 89, 90 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) |
| 92 | 40, 91 | reseq12d 5998 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)) = ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})) |
| 93 | 40, 36 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚))) |
| 94 | 93 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = 𝐹) |
| 95 | 94 | rneqd 5949 |
. . . . . . 7
⊢ (𝜑 → ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran 𝐹) |
| 96 | | forn 6823 |
. . . . . . . 8
⊢ (𝐹:𝐶–onto→𝐴 → ran 𝐹 = 𝐴) |
| 97 | 3, 96 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 = 𝐴) |
| 98 | 95, 97 | eqtr2d 2778 |
. . . . . 6
⊢ (𝜑 → 𝐴 = ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚))) |
| 99 | 98 | difeq1d 4125 |
. . . . 5
⊢ (𝜑 → (𝐴 ∖ {∅}) = (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})) |
| 100 | 92, 91, 99 | f1oeq123d 6842 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}) ↔ ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran
(𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))) |
| 101 | 39, 100 | mpbird 257 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅})) |
| 102 | | fvres 6925 |
. . . . 5
⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛)) |
| 103 | 102 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛)) |
| 104 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝜑) |
| 105 | | sge0fodjrnlem.fng |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
| 106 | 104, 42, 105 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) = 𝐺) |
| 107 | 103, 106 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = 𝐺) |
| 108 | 1, 25, 26, 27, 101, 107, 10 | sge0f1o 46397 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷))) |
| 109 | 105 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 = (𝐹‘𝑛)) |
| 110 | 109, 31 | eqeltrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴) |
| 111 | 104, 42, 110 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐺 ∈ 𝐴) |
| 112 | 111 | ex 412 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝐺 ∈ 𝐴)) |
| 113 | 112 | imdistani 568 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝜑 ∧ 𝐺 ∈ 𝐴)) |
| 114 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑘𝐺 |
| 115 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑘 𝐺 ∈ 𝐴 |
| 116 | 1, 115 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝐺 ∈ 𝐴) |
| 117 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑘 𝐷 ∈
(0[,]+∞) |
| 118 | 116, 117 | nfim 1896 |
. . . . 5
⊢
Ⅎ𝑘((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)) |
| 119 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑘 = 𝐺 → (𝑘 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴)) |
| 120 | 119 | anbi2d 630 |
. . . . . 6
⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝐺 ∈ 𝐴))) |
| 121 | 26 | eleq1d 2826 |
. . . . . 6
⊢ (𝑘 = 𝐺 → (𝐵 ∈ (0[,]+∞) ↔ 𝐷 ∈
(0[,]+∞))) |
| 122 | 120, 121 | imbi12d 344 |
. . . . 5
⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)))) |
| 123 | 114, 118,
122, 9 | vtoclgf 3569 |
. . . 4
⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))) |
| 124 | 111, 113,
123 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐷 ∈ (0[,]+∞)) |
| 125 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝜑) |
| 126 | | eldifi 4131 |
. . . . . 6
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶) |
| 127 | 126 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝐶) |
| 128 | 125, 127,
110 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 ∈ 𝐴) |
| 129 | | dfin4 4278 |
. . . . . . . . 9
⊢ (𝑍 ∩ 𝐶) = (𝑍 ∖ (𝑍 ∖ 𝐶)) |
| 130 | | difss 4136 |
. . . . . . . . 9
⊢ (𝑍 ∖ (𝑍 ∖ 𝐶)) ⊆ 𝑍 |
| 131 | 129, 130 | eqsstri 4030 |
. . . . . . . 8
⊢ (𝑍 ∩ 𝐶) ⊆ 𝑍 |
| 132 | | inss2 4238 |
. . . . . . . . . 10
⊢ (𝐶 ∩ 𝑍) ⊆ 𝑍 |
| 133 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) |
| 134 | | dfin4 4278 |
. . . . . . . . . . . 12
⊢ (𝐶 ∩ 𝑍) = (𝐶 ∖ (𝐶 ∖ 𝑍)) |
| 135 | 134 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ (𝐶 ∖ (𝐶 ∖ 𝑍)) = (𝐶 ∩ 𝑍) |
| 136 | 133, 135 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∩ 𝑍)) |
| 137 | 132, 136 | sselid 3981 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍) |
| 138 | 137, 126 | elind 4200 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝑍 ∩ 𝐶)) |
| 139 | 131, 138 | sselid 3981 |
. . . . . . 7
⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍) |
| 140 | 139 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝑍) |
| 141 | 76 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∅ = (𝐹‘𝑛)) |
| 142 | | simpl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝜑) |
| 143 | 73 | simpld 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝐶) |
| 144 | 142, 143,
105 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = 𝐺) |
| 145 | 141, 144 | eqtr2d 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐺 = ∅) |
| 146 | 125, 140,
145 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 = ∅) |
| 147 | 125, 146 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → (𝜑 ∧ 𝐺 = ∅)) |
| 148 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑘 𝐺 = ∅ |
| 149 | 1, 148 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝐺 = ∅) |
| 150 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑘 𝐷 = 0 |
| 151 | 149, 150 | nfim 1896 |
. . . . 5
⊢
Ⅎ𝑘((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0) |
| 152 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑘 = 𝐺 → (𝑘 = ∅ ↔ 𝐺 = ∅)) |
| 153 | 152 | anbi2d 630 |
. . . . . 6
⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 = ∅) ↔ (𝜑 ∧ 𝐺 = ∅))) |
| 154 | 26 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑘 = 𝐺 → (𝐵 = 0 ↔ 𝐷 = 0)) |
| 155 | 153, 154 | imbi12d 344 |
. . . . 5
⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) ↔ ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0))) |
| 156 | 114, 151,
155, 21 | vtoclgf 3569 |
. . . 4
⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)) |
| 157 | 128, 147,
156 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐷 = 0) |
| 158 | 25, 2, 41, 124, 157 | sge0ss 46427 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |
| 159 | 24, 108, 158 | 3eqtrd 2781 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |