Proof of Theorem esumrnmpt2
Step | Hyp | Ref
| Expression |
1 | | nfrab1 3099 |
. . . . 5
⊢
Ⅎ𝑘{𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} |
2 | | esumrnmpt2.1 |
. . . . 5
⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) |
3 | | esumrnmpt2.2 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
4 | | ssrab2 3650 |
. . . . . . 7
⊢ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴 |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴) |
6 | 3, 5 | ssexd 4733 |
. . . . 5
⊢ (𝜑 → {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ∈ V) |
7 | 5 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘 ∈ 𝐴) |
8 | | esumrnmpt2.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)) |
9 | 7, 8 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞)) |
10 | | esumrnmpt2.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
11 | 7, 10 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵 ∈ 𝑊) |
12 | | rabid 3095 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↔ (𝑘 ∈ 𝐴 ∧ ¬ 𝐵 = ∅)) |
13 | 12 | simprbi 479 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} → ¬ 𝐵 = ∅) |
14 | 13 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 = ∅) |
15 | | elsng 4139 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑊 → (𝐵 ∈ {∅} ↔ 𝐵 = ∅)) |
16 | 11, 15 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) → (𝐵 ∈ {∅} ↔ 𝐵 = ∅)) |
17 | 14, 16 | mtbird 314 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 ∈ {∅}) |
18 | 11, 17 | eldifd 3551 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵 ∈ (𝑊 ∖ {∅})) |
19 | | esumrnmpt2.6 |
. . . . . 6
⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵) |
20 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘𝐴 |
21 | 1, 20 | disjss1f 28768 |
. . . . . 6
⊢ ({𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴 → (Disj 𝑘 ∈ 𝐴 𝐵 → Disj 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐵)) |
22 | 5, 19, 21 | sylc 63 |
. . . . 5
⊢ (𝜑 → Disj 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐵) |
23 | 1, 2, 6, 9, 18, 22 | esumrnmpt 29441 |
. . . 4
⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷) |
24 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) |
25 | | snex 4835 |
. . . . . . . . . . . 12
⊢ {∅}
∈ V |
26 | 25 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) → {∅} ∈
V) |
27 | | velsn 4141 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅) |
28 | 27 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ {∅} → 𝑦 = ∅) |
29 | 28 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝑦 = ∅) |
30 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘𝜑 |
31 | | nfre1 2988 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘∃𝑘 ∈ 𝐴 𝐵 = ∅ |
32 | 30, 31 | nfan 1816 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) |
33 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘 𝑦 = ∅ |
34 | 32, 33 | nfan 1816 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) |
35 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘 𝐶 = 0 |
36 | | simpllr 795 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝑦 = ∅) |
37 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝐵 = ∅) |
38 | 36, 37 | eqtr4d 2647 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝑦 = 𝐵) |
39 | 38, 2 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝐶 = 𝐷) |
40 | | simp-4l 802 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝜑) |
41 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝑘 ∈ 𝐴) |
42 | | esumrnmpt2.5 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0) |
43 | 40, 41, 37, 42 | syl21anc 1317 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0) |
44 | 39, 43 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → 𝐶 = 0) |
45 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → ∃𝑘 ∈ 𝐴 𝐵 = ∅) |
46 | 34, 35, 44, 45 | r19.29af2 3057 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → 𝐶 = 0) |
47 | 29, 46 | syldan 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 = 0) |
48 | | 0e0iccpnf 12154 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]+∞) |
49 | 47, 48 | syl6eqel 2696 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 ∈ (0[,]+∞)) |
50 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘𝑦 |
51 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) |
52 | 51 | nfrn 5289 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) |
53 | 50, 52 | nfel 2763 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) |
54 | 30, 53 | nfan 1816 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) |
55 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
56 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↔ (𝑘 ∈ 𝐴 ∧ 𝐵 = ∅)) |
57 | 56 | simprbi 479 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} → 𝐵 = ∅) |
58 | 57 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐵 = ∅) |
59 | 55, 58 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = ∅) |
60 | 59, 27 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 ∈ {∅}) |
61 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
62 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) |
63 | 62 | elrnmpt 5293 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝑦 = 𝐵)) |
64 | 61, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝑦 = 𝐵) |
65 | 64 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝑦 = 𝐵) |
66 | 65 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝑦 = 𝐵) |
67 | 54, 60, 66 | r19.29af 3058 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) → 𝑦 ∈ {∅}) |
68 | 67 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) → 𝑦 ∈ {∅})) |
69 | 68 | ssrdv 3574 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ⊆ {∅}) |
70 | 69 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) → ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ⊆ {∅}) |
71 | 24, 26, 49, 70 | esummono 29443 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ≤ Σ*𝑦 ∈ {∅}𝐶) |
72 | | 0ex 4718 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
73 | 72 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) → ∅ ∈
V) |
74 | 48 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) → 0 ∈
(0[,]+∞)) |
75 | 46, 73, 74 | esumsn 29454 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) → Σ*𝑦 ∈ {∅}𝐶 = 0) |
76 | 71, 75 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑘 ∈ 𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0) |
77 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ ∃𝑘 ∈ 𝐴 𝐵 = ∅) → ¬ ∃𝑘 ∈ 𝐴 𝐵 = ∅) |
78 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 ¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ |
79 | 31 | nfn 1768 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘 ¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ |
80 | | nfrab1 3099 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘{𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} |
81 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘∅ |
82 | | rabn0 3912 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ≠ ∅ ↔ ∃𝑘 ∈ 𝐴 𝐵 = ∅) |
83 | 82 | biimpi 205 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ≠ ∅ → ∃𝑘 ∈ 𝐴 𝐵 = ∅) |
84 | 83 | necon1bi 2810 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ → {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} = ∅) |
85 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐵 = 𝐵 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ → 𝐵 = 𝐵) |
87 | 79, 80, 81, 84, 86 | mpteq12df 28837 |
. . . . . . . . . . . . . . . 16
⊢ (¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ ∅ ↦ 𝐵)) |
88 | | mpt0 5934 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ∅ ↦ 𝐵) = ∅ |
89 | 87, 88 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) = ∅) |
90 | 89 | rneqd 5274 |
. . . . . . . . . . . . . 14
⊢ (¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) = ran ∅) |
91 | | rn0 5298 |
. . . . . . . . . . . . . 14
⊢ ran
∅ = ∅ |
92 | 90, 91 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) = ∅) |
93 | 78, 92 | esumeq1d 29424 |
. . . . . . . . . . . 12
⊢ (¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑦 ∈ ∅𝐶) |
94 | | esumnul 29437 |
. . . . . . . . . . . 12
⊢
Σ*𝑦
∈ ∅𝐶 =
0 |
95 | 93, 94 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 = 0) |
96 | | 0le0 10987 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
97 | 95, 96 | syl6eqbr 4622 |
. . . . . . . . . 10
⊢ (¬
∃𝑘 ∈ 𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0) |
98 | 77, 97 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∃𝑘 ∈ 𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0) |
99 | 76, 98 | pm2.61dan 828 |
. . . . . . . 8
⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0) |
100 | | ssrab2 3650 |
. . . . . . . . . . . . 13
⊢ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ⊆ 𝐴 |
101 | 100 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ⊆ 𝐴) |
102 | 3, 101 | ssexd 4733 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∈ V) |
103 | 80 | mptexgf 28809 |
. . . . . . . . . . 11
⊢ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∈ V) |
104 | | rnexg 6990 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∈ V) |
105 | 102, 103,
104 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∈ V) |
106 | 2 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) |
107 | | simplll 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑) |
108 | 101 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) → 𝑘 ∈ 𝐴) |
109 | 108 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) → 𝑘 ∈ 𝐴) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘 ∈ 𝐴) |
111 | 107, 110,
8 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞)) |
112 | 106, 111 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞)) |
113 | 54, 112, 66 | r19.29af 3058 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞)) |
114 | 113 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞)) |
115 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) |
116 | 115 | esumcl 29419 |
. . . . . . . . . 10
⊢ ((ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∈ V ∧ ∀𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞)) →
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞)) |
117 | 105, 114,
116 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞)) |
118 | | elxrge0 12152 |
. . . . . . . . . 10
⊢
(Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) ↔
(Σ*𝑦
∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ≤
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶)) |
119 | 118 | simprbi 479 |
. . . . . . . . 9
⊢
(Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) → 0 ≤
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶) |
120 | 117, 119 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶) |
121 | 99, 120 | jca 553 |
. . . . . . 7
⊢ (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶)) |
122 | | iccssxr 12127 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
123 | 122, 117 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈
ℝ*) |
124 | 122, 48 | sselii 3565 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
125 | 124 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ*) |
126 | | xrletri3 11861 |
. . . . . . . 8
⊢
((Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ∈
ℝ*) → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶))) |
127 | 123, 125,
126 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶))) |
128 | 121, 127 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 = 0) |
129 | 128 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (0 +𝑒
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)) |
130 | 9 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞)) |
131 | 1 | esumcl 29419 |
. . . . . . . . 9
⊢ (({𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ∈ V ∧ ∀𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
{𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞)) |
132 | 6, 130, 131 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞)) |
133 | 122, 132 | sseldi 3566 |
. . . . . . 7
⊢ (𝜑 → Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈
ℝ*) |
134 | 23, 133 | eqeltrd 2688 |
. . . . . 6
⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈
ℝ*) |
135 | | xaddid2 11947 |
. . . . . 6
⊢
(Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* → (0
+𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) |
136 | 134, 135 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 +𝑒
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) |
137 | 129, 136 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) |
138 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) → 𝜑) |
139 | 57 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) → 𝐵 = ∅) |
140 | 138, 108,
139, 42 | syl21anc 1317 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) → 𝐷 = 0) |
141 | 140 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝐷 = 0) |
142 | 30, 141 | esumeq2d 29426 |
. . . . . . 7
⊢ (𝜑 → Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝐷 = Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}0) |
143 | 80 | esum0 29438 |
. . . . . . . 8
⊢ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∈ V →
Σ*𝑘 ∈
{𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}0 = 0) |
144 | 102, 143 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}0 = 0) |
145 | 142, 144 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝐷 = 0) |
146 | 145 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → (Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝐷 +𝑒
Σ*𝑘 ∈
{𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = (0 +𝑒
Σ*𝑘 ∈
{𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷)) |
147 | | xaddid2 11947 |
. . . . . 6
⊢
(Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ ℝ* → (0
+𝑒 Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷) |
148 | 133, 147 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 +𝑒
Σ*𝑘 ∈
{𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷) |
149 | 146, 148 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝐷 +𝑒
Σ*𝑘 ∈
{𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷) |
150 | 23, 137, 149 | 3eqtr4d 2654 |
. . 3
⊢ (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝐷 +𝑒
Σ*𝑘 ∈
{𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷)) |
151 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑦𝜑 |
152 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑦ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) |
153 | 1 | mptexgf 28809 |
. . . . 5
⊢ ({𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V) |
154 | | rnexg 6990 |
. . . . 5
⊢ ((𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V) |
155 | 6, 153, 154 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V) |
156 | | ssrin 3800 |
. . . . . . 7
⊢ (ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ⊆ {∅} → (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ({∅} ∩ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))) |
157 | 69, 156 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ({∅} ∩ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))) |
158 | | incom 3767 |
. . . . . . 7
⊢ (ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ({∅} ∩ ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) |
159 | 13 | neqned 2789 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} → 𝐵 ≠ ∅) |
160 | 159 | necomd 2837 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} → ∅ ≠ 𝐵) |
161 | 160 | neneqd 2787 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} → ¬ ∅ = 𝐵) |
162 | 161 | nrex 2983 |
. . . . . . . . 9
⊢ ¬
∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵 |
163 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) |
164 | 163 | elrnmpt 5293 |
. . . . . . . . . 10
⊢ (∅
∈ V → (∅ ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵)) |
165 | 72, 164 | ax-mp 5 |
. . . . . . . . 9
⊢ (∅
∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵) |
166 | 162, 165 | mtbir 312 |
. . . . . . . 8
⊢ ¬
∅ ∈ ran (𝑘
∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) |
167 | | disjsn 4192 |
. . . . . . . 8
⊢ ((ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ∅ ↔ ¬
∅ ∈ ran (𝑘
∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) |
168 | 166, 167 | mpbir 220 |
. . . . . . 7
⊢ (ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) =
∅ |
169 | 158, 168 | eqtr3i 2634 |
. . . . . 6
⊢
({∅} ∩ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅ |
170 | 157, 169 | syl6sseq 3614 |
. . . . 5
⊢ (𝜑 → (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅) |
171 | | ss0 3926 |
. . . . 5
⊢ ((ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅ → (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅) |
172 | 170, 171 | syl 17 |
. . . 4
⊢ (𝜑 → (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅) |
173 | | nfmpt1 4675 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) |
174 | 173 | nfrn 5289 |
. . . . . . 7
⊢
Ⅎ𝑘ran
(𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) |
175 | 50, 174 | nfel 2763 |
. . . . . 6
⊢
Ⅎ𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) |
176 | 30, 175 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) |
177 | 2 | adantl 481 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) |
178 | | simplll 794 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑) |
179 | 7 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘 ∈ 𝐴) |
180 | 179 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘 ∈ 𝐴) |
181 | 178, 180,
8 | syl2anc 691 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞)) |
182 | 177, 181 | eqeltrd 2688 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞)) |
183 | 163 | elrnmpt 5293 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)) |
184 | 61, 183 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵) |
185 | 184 | biimpi 205 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵) |
186 | 185 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵) |
187 | 176, 182,
186 | r19.29af 3058 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞)) |
188 | 151, 115,
152, 105, 155, 172, 113, 187 | esumsplit 29442 |
. . 3
⊢ (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒
Σ*𝑦 ∈
ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)) |
189 | | rabnc 3916 |
. . . . 5
⊢ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∩ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) = ∅ |
190 | 189 | a1i 11 |
. . . 4
⊢ (𝜑 → ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∩ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) = ∅) |
191 | 108, 8 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞)) |
192 | 30, 80, 1, 102, 6, 190, 191, 9 | esumsplit 29442 |
. . 3
⊢ (𝜑 → Σ*𝑘 ∈ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∪ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅})𝐷 = (Σ*𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅}𝐷 +𝑒
Σ*𝑘 ∈
{𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}𝐷)) |
193 | 150, 188,
192 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = Σ*𝑘 ∈ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∪ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅})𝐷) |
194 | | rabxm 3915 |
. . . . . . . 8
⊢ 𝐴 = ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∪ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) |
195 | 194, 85 | mpteq12i 4670 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∪ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵) |
196 | | mptun 5938 |
. . . . . . 7
⊢ (𝑘 ∈ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∪ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵) = ((𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) |
197 | 195, 196 | eqtri 2632 |
. . . . . 6
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = ((𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) |
198 | 197 | rneqi 5273 |
. . . . 5
⊢ ran
(𝑘 ∈ 𝐴 ↦ 𝐵) = ran ((𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) |
199 | | rnun 5460 |
. . . . 5
⊢ ran
((𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) |
200 | 198, 199 | eqtri 2632 |
. . . 4
⊢ ran
(𝑘 ∈ 𝐴 ↦ 𝐵) = (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) |
201 | 200 | a1i 11 |
. . 3
⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ 𝐵) = (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))) |
202 | 151, 201 | esumeq1d 29424 |
. 2
⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝐶 = Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶) |
203 | 194 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐴 = ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∪ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅})) |
204 | 30, 203 | esumeq1d 29424 |
. 2
⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐷 = Σ*𝑘 ∈ ({𝑘 ∈ 𝐴 ∣ 𝐵 = ∅} ∪ {𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅})𝐷) |
205 | 193, 202,
204 | 3eqtr4d 2654 |
1
⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐷) |