Metamath Proof Explorer

Theorem esumrnmpt2

Description: Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 30-May-2020)

Ref Expression
Hypotheses esumrnmpt2.1 ⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
esumrnmpt2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumrnmpt2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
esumrnmpt2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
esumrnmpt2.5 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐷 = 0 )
esumrnmpt2.6 ⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
Assertion esumrnmpt2 ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐷 )

Proof

Step Hyp Ref Expression
1 esumrnmpt2.1 ⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
2 esumrnmpt2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 esumrnmpt2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
4 esumrnmpt2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5 esumrnmpt2.5 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐷 = 0 )
6 esumrnmpt2.6 ⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
7 nfrab1 ⊢ Ⅎ 𝑘 { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ }
8 ssrab2 ⊢ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ⊆ 𝐴
9 8 a1i ⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ⊆ 𝐴 )
10 2 9 ssexd ⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∈ V )
11 9 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝑘 ∈ 𝐴 )
12 11 3 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝐷 ∈ ( 0 [,] +∞ ) )
13 11 4 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝐵 ∈ 𝑊 )
14 rabid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↔ ( 𝑘 ∈ 𝐴 ∧ ¬ 𝐵 = ∅ ) )
15 14 simprbi ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } → ¬ 𝐵 = ∅ )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → ¬ 𝐵 = ∅ )
17 elsng ⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∈ { ∅ } ↔ 𝐵 = ∅ ) )
18 13 17 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → ( 𝐵 ∈ { ∅ } ↔ 𝐵 = ∅ ) )
19 16 18 mtbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → ¬ 𝐵 ∈ { ∅ } )
20 13 19 eldifd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝐵 ∈ ( 𝑊 ∖ { ∅ } ) )
21 nfcv ⊢ Ⅎ 𝑘 𝐴
22 7 21 disjss1f ⊢ ( { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ⊆ 𝐴 → ( Disj 𝑘 ∈ 𝐴 𝐵 → Disj 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐵 ) )
23 9 6 22 sylc ⊢ ( 𝜑 → Disj 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐵 )
24 7 1 10 12 20 23 esumrnmpt ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 )
25 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
26 snex ⊢ { ∅ } ∈ V
27 26 a1i ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → { ∅ } ∈ V )
28 velsn ⊢ ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ )
29 28 biimpi ⊢ ( 𝑦 ∈ { ∅ } → 𝑦 = ∅ )
30 29 adantl ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 ∈ { ∅ } ) → 𝑦 = ∅ )
31 nfv ⊢ Ⅎ 𝑘 𝜑
32 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ 𝐴 𝐵 = ∅
33 31 32 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
34 nfv ⊢ Ⅎ 𝑘 𝑦 = ∅
35 33 34 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ )
36 nfv ⊢ Ⅎ 𝑘 𝐶 = 0
37 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝑦 = ∅ )
38 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
39 37 38 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝑦 = 𝐵 )
40 39 1 syl ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐶 = 𝐷 )
41 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝜑 )
42 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝑘 ∈ 𝐴 )
43 41 42 38 5 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐷 = 0 )
44 40 43 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐶 = 0 )
45 simplr ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) → ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
46 35 36 44 45 r19.29af2 ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) → 𝐶 = 0 )
47 30 46 syldan ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 ∈ { ∅ } ) → 𝐶 = 0 )
48 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
49 47 48 eqeltrdi ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 ∈ { ∅ } ) → 𝐶 ∈ ( 0 [,] +∞ ) )
50 nfcv ⊢ Ⅎ 𝑘 𝑦
51 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
52 51 nfrn ⊢ Ⅎ 𝑘 ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
53 50 52 nfel ⊢ Ⅎ 𝑘 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
54 31 53 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) )
55 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
56 rabid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↔ ( 𝑘 ∈ 𝐴 ∧ 𝐵 = ∅ ) )
57 56 simprbi ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } → 𝐵 = ∅ )
58 57 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐵 = ∅ )
59 55 58 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑦 = ∅ )
60 59 28 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑦 ∈ { ∅ } )
61 vex ⊢ 𝑦 ∈ V
62 eqid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
63 62 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝑦 = 𝐵 ) )
64 61 63 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝑦 = 𝐵 )
65 64 biimpi ⊢ ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) → ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝑦 = 𝐵 )
66 65 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) → ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝑦 = 𝐵 )
67 54 60 66 r19.29af ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) → 𝑦 ∈ { ∅ } )
68 67 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) → 𝑦 ∈ { ∅ } ) )
69 68 ssrdv ⊢ ( 𝜑 → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ⊆ { ∅ } )
70 69 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ⊆ { ∅ } )
71 25 27 49 70 esummono ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ Σ* 𝑦 ∈ { ∅ } 𝐶 )
72 0ex ⊢ ∅ ∈ V
73 72 a1i ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → ∅ ∈ V )
74 48 a1i ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → 0 ∈ ( 0 [,] +∞ ) )
75 46 73 74 esumsn ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → Σ* 𝑦 ∈ { ∅ } 𝐶 = 0 )
76 71 75 breqtrd ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 )
77 simpr ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
78 nfv ⊢ Ⅎ 𝑦 ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅
79 32 nfn ⊢ Ⅎ 𝑘 ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅
80 rabn0 ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ≠ ∅ ↔ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
81 80 biimpi ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ≠ ∅ → ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
82 81 necon1bi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } = ∅ )
83 eqid ⊢ 𝐵 = 𝐵
84 83 a1i ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → 𝐵 = 𝐵 )
85 79 82 84 mpteq12df ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ( 𝑘 ∈ ∅ ↦ 𝐵 ) )
86 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ 𝐵 ) = ∅
87 85 86 eqtrdi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ∅ )
88 87 rneqd ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ran ∅ )
89 rn0 ⊢ ran ∅ = ∅
90 88 89 eqtrdi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ∅ )
91 78 90 esumeq1d ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = Σ* 𝑦 ∈ ∅ 𝐶 )
92 esumnul ⊢ Σ* 𝑦 ∈ ∅ 𝐶 = 0
93 91 92 eqtrdi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = 0 )
94 0le0 ⊢ 0 ≤ 0
95 93 94 eqbrtrdi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 )
96 77 95 syl ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 )
97 76 96 pm2.61dan ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 )
98 ssrab2 ⊢ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ⊆ 𝐴
99 98 a1i ⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ⊆ 𝐴 )
100 2 99 ssexd ⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∈ V )
101 nfrab1 ⊢ Ⅎ 𝑘 { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ }
102 101 mptexgf ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∈ V → ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
103 rnexg ⊢ ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
104 100 102 103 3syl ⊢ ( 𝜑 → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
105 1 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
106 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝜑 )
107 99 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝑘 ∈ 𝐴 )
108 107 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝑘 ∈ 𝐴 )
109 108 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑘 ∈ 𝐴 )
110 106 109 3 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
111 105 110 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
112 54 111 66 r19.29af ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
113 112 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
114 nfcv ⊢ Ⅎ 𝑦 ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
115 114 esumcl ⊢ ( ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V ∧ ∀ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
116 104 113 115 syl2anc ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
117 elxrge0 ⊢ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) ↔ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* ∧ 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) )
118 117 simprbi ⊢ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) → 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
119 116 118 syl ⊢ ( 𝜑 → 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
120 97 119 jca ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 ∧ 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) )
121 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
122 121 116 sselid ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* )
123 121 48 sselii ⊢ 0 ∈ ℝ*
124 123 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
125 xrletri3 ⊢ ( ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = 0 ↔ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 ∧ 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) ) )
126 122 124 125 syl2anc ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = 0 ↔ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 ∧ 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) ) )
127 120 126 mpbird ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = 0 )
128 127 oveq1d ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = ( 0 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) )
129 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ( 0 [,] +∞ ) )
130 7 esumcl ⊢ ( ( { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∈ V ∧ ∀ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ( 0 [,] +∞ ) )
131 10 129 130 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ( 0 [,] +∞ ) )
132 121 131 sselid ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ℝ* )
133 24 132 eqeltrd ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* )
134 xaddid2 ⊢ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* → ( 0 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
135 133 134 syl ⊢ ( 𝜑 → ( 0 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
136 128 135 eqtrd ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
137 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝜑 )
138 57 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝐵 = ∅ )
139 137 107 138 5 syl21anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝐷 = 0 )
140 139 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 = 0 )
141 31 140 esumeq2d ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 0 )
142 101 esum0 ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∈ V → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 0 = 0 )
143 100 142 syl ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 0 = 0 )
144 141 143 eqtrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 = 0 )
145 144 oveq1d ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) = ( 0 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) )
146 xaddid2 ⊢ ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ℝ* → ( 0 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 )
147 132 146 syl ⊢ ( 𝜑 → ( 0 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 )
148 145 147 eqtrd ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 )
149 24 136 148 3eqtr4d ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) )
150 nfv ⊢ Ⅎ 𝑦 𝜑
151 nfcv ⊢ Ⅎ 𝑦 ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
152 7 mptexgf ⊢ ( { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∈ V → ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
153 rnexg ⊢ ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
154 10 152 153 3syl ⊢ ( 𝜑 → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
155 69 ssrind ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ⊆ ( { ∅ } ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) )
156 incom ⊢ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∩ { ∅ } ) = ( { ∅ } ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
157 15 neqned ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } → 𝐵 ≠ ∅ )
158 157 necomd ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } → ∅ ≠ 𝐵 )
159 158 neneqd ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } → ¬ ∅ = 𝐵 )
160 159 nrex ⊢ ¬ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∅ = 𝐵
161 eqid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) = ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
162 161 elrnmpt ⊢ ( ∅ ∈ V → ( ∅ ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∅ = 𝐵 ) )
163 72 162 ax-mp ⊢ ( ∅ ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∅ = 𝐵 )
164 160 163 mtbir ⊢ ¬ ∅ ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
165 disjsn ⊢ ( ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
166 164 165 mpbir ⊢ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∩ { ∅ } ) = ∅
167 156 166 eqtr3i ⊢ ( { ∅ } ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) = ∅
168 155 167 sseqtrdi ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ⊆ ∅ )
169 ss0 ⊢ ( ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ⊆ ∅ → ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) = ∅ )
170 168 169 syl ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) = ∅ )
171 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
172 171 nfrn ⊢ Ⅎ 𝑘 ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
173 50 172 nfel ⊢ Ⅎ 𝑘 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
174 31 173 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
175 1 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
176 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝜑 )
177 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝑘 ∈ 𝐴 )
178 177 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑘 ∈ 𝐴 )
179 176 178 3 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
180 175 179 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
181 161 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝑦 = 𝐵 ) )
182 61 181 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝑦 = 𝐵 )
183 182 biimpi ⊢ ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) → ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝑦 = 𝐵 )
184 183 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) → ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝑦 = 𝐵 )
185 174 180 184 r19.29af ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
186 150 114 151 104 154 170 112 185 esumsplit ⊢ ( 𝜑 → Σ* 𝑦 ∈ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) 𝐶 = ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) )
187 rabnc ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∩ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) = ∅
188 187 a1i ⊢ ( 𝜑 → ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∩ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) = ∅ )
189 107 3 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝐷 ∈ ( 0 [,] +∞ ) )
190 31 101 7 100 10 188 189 12 esumsplit ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) 𝐷 = ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) )
191 149 186 190 3eqtr4d ⊢ ( 𝜑 → Σ* 𝑦 ∈ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) 𝐶 = Σ* 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) 𝐷 )
192 rabxm ⊢ 𝐴 = ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } )
193 192 83 mpteq12i ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ↦ 𝐵 )
194 mptun ⊢ ( 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ↦ 𝐵 ) = ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
195 193 194 eqtri ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
196 195 rneqi ⊢ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ran ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
197 rnun ⊢ ran ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) = ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
198 196 197 eqtri ⊢ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
199 198 a1i ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) )
200 150 199 esumeq1d ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑦 ∈ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) 𝐶 )
201 192 a1i ⊢ ( 𝜑 → 𝐴 = ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) )
202 31 201 esumeq1d ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐷 = Σ* 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) 𝐷 )
203 191 200 202 3eqtr4d ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐷 )