Metamath Proof Explorer

Theorem fsumrlim

Description: Limit of a finite sum of converging sequences. Note that C ( k ) is a collection of functions with implicit parameter k , each of which converges to D ( k ) as n ~> +oo . (Contributed by Mario Carneiro, 22-May-2016)

Ref Expression
Hypotheses fsumrlim.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
fsumrlim.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
fsumrlim.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑉 )
fsumrlim.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )
Assertion fsumrlim ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝐵 𝐷 )

Proof

Step Hyp Ref Expression
1 fsumrlim.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 fsumrlim.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
3 fsumrlim.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑉 )
4 fsumrlim.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )
5 ssid ⊢ 𝐵 ⊆ 𝐵
6 sseq1 ⊢ ( 𝑤 = ∅ → ( 𝑤 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵 ) )
7 sumeq1 ⊢ ( 𝑤 = ∅ → Σ 𝑘 ∈ 𝑤 𝐶 = Σ 𝑘 ∈ ∅ 𝐶 )
8 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐶 = 0
9 7 8 eqtrdi ⊢ ( 𝑤 = ∅ → Σ 𝑘 ∈ 𝑤 𝐶 = 0 )
10 9 mpteq2dv ⊢ ( 𝑤 = ∅ → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
11 sumeq1 ⊢ ( 𝑤 = ∅ → Σ 𝑘 ∈ 𝑤 𝐷 = Σ 𝑘 ∈ ∅ 𝐷 )
12 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐷 = 0
13 11 12 eqtrdi ⊢ ( 𝑤 = ∅ → Σ 𝑘 ∈ 𝑤 𝐷 = 0 )
14 10 13 breq12d ⊢ ( 𝑤 = ∅ → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ↔ ( 𝑥 ∈ 𝐴 ↦ 0 ) ⇝𝑟 0 ) )
15 6 14 imbi12d ⊢ ( 𝑤 = ∅ → ( ( 𝑤 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ) ↔ ( ∅ ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ 0 ) ⇝𝑟 0 ) ) )
16 15 imbi2d ⊢ ( 𝑤 = ∅ → ( ( 𝜑 → ( 𝑤 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ 0 ) ⇝𝑟 0 ) ) ) )
17 sseq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ⊆ 𝐵 ↔ 𝑦 ⊆ 𝐵 ) )
18 sumeq1 ⊢ ( 𝑤 = 𝑦 → Σ 𝑘 ∈ 𝑤 𝐶 = Σ 𝑘 ∈ 𝑦 𝐶 )
19 18 mpteq2dv ⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) )
20 sumeq1 ⊢ ( 𝑤 = 𝑦 → Σ 𝑘 ∈ 𝑤 𝐷 = Σ 𝑘 ∈ 𝑦 𝐷 )
21 19 20 breq12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ↔ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) )
22 17 21 imbi12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ) ↔ ( 𝑦 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) ) )
23 22 imbi2d ⊢ ( 𝑤 = 𝑦 → ( ( 𝜑 → ( 𝑤 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ) ) ↔ ( 𝜑 → ( 𝑦 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) ) ) )
24 sseq1 ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑤 ⊆ 𝐵 ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) )
25 sumeq1 ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑤 𝐶 = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 )
26 25 mpteq2dv ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) )
27 sumeq1 ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑤 𝐷 = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 )
28 26 27 breq12d ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ↔ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) )
29 24 28 imbi12d ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑤 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ) ↔ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) ) )
30 29 imbi2d ⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝜑 → ( 𝑤 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ) ) ↔ ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) ) ) )
31 sseq1 ⊢ ( 𝑤 = 𝐵 → ( 𝑤 ⊆ 𝐵 ↔ 𝐵 ⊆ 𝐵 ) )
32 sumeq1 ⊢ ( 𝑤 = 𝐵 → Σ 𝑘 ∈ 𝑤 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶 )
33 32 mpteq2dv ⊢ ( 𝑤 = 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) )
34 sumeq1 ⊢ ( 𝑤 = 𝐵 → Σ 𝑘 ∈ 𝑤 𝐷 = Σ 𝑘 ∈ 𝐵 𝐷 )
35 33 34 breq12d ⊢ ( 𝑤 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ↔ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝐵 𝐷 ) )
36 31 35 imbi12d ⊢ ( 𝑤 = 𝐵 → ( ( 𝑤 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ) ↔ ( 𝐵 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝐵 𝐷 ) ) )
37 36 imbi2d ⊢ ( 𝑤 = 𝐵 → ( ( 𝜑 → ( 𝑤 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑤 𝐷 ) ) ↔ ( 𝜑 → ( 𝐵 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝐵 𝐷 ) ) ) )
38 0cn ⊢ 0 ∈ ℂ
39 rlimconst ⊢ ( ( 𝐴 ⊆ ℝ ∧ 0 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 0 ) ⇝𝑟 0 )
40 1 38 39 sylancl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 0 ) ⇝𝑟 0 )
41 40 a1d ⊢ ( 𝜑 → ( ∅ ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ 0 ) ⇝𝑟 0 ) )
42 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
43 sstr ⊢ ( ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) → 𝑦 ⊆ 𝐵 )
44 42 43 mpan ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → 𝑦 ⊆ 𝐵 )
45 44 imim1i ⊢ ( ( 𝑦 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) )
46 sumex ⊢ Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 ∈ V
47 46 a1i ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) ∧ 𝑤 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 ∈ V )
48 simprr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 )
49 48 unssbd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → { 𝑧 } ⊆ 𝐵 )
50 vex ⊢ 𝑧 ∈ V
51 50 snss ⊢ ( 𝑧 ∈ 𝐵 ↔ { 𝑧 } ⊆ 𝐵 )
52 49 51 sylibr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ 𝐵 )
54 3 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
55 54 4 rlimmptrcl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
56 55 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
57 56 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
58 57 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
59 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐶
60 59 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ
61 csbeq1a ⊢ ( 𝑘 = 𝑧 → 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
62 61 eleq1d ⊢ ( 𝑘 = 𝑧 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
63 60 62 rspc ⊢ ( 𝑧 ∈ 𝐵 → ( ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ → ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
64 53 58 63 sylc ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ )
65 64 ralrimiva ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ )
67 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶
68 67 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ
69 csbeq1a ⊢ ( 𝑥 = 𝑤 → ⦋ 𝑧 / 𝑘 ⦌ 𝐶 = ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
70 69 eleq1d ⊢ ( 𝑥 = 𝑤 → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ ↔ ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
71 68 70 rspc ⊢ ( 𝑤 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ → ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
72 66 71 mpan9 ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) ∧ 𝑤 ∈ 𝐴 ) → ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ )
73 72 elexd ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) ∧ 𝑤 ∈ 𝐴 ) → ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V )
74 nfcv ⊢ Ⅎ 𝑤 Σ 𝑘 ∈ 𝑦 𝐶
75 nfcv ⊢ Ⅎ 𝑥 𝑦
76 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐶
77 75 76 nfsum ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶
78 csbeq1a ⊢ ( 𝑥 = 𝑤 → 𝐶 = ⦋ 𝑤 / 𝑥 ⦌ 𝐶 )
79 78 sumeq2sdv ⊢ ( 𝑥 = 𝑤 → Σ 𝑘 ∈ 𝑦 𝐶 = Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 )
80 74 77 79 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) = ( 𝑤 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 )
81 simpr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 )
82 80 81 eqbrtrrid ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( 𝑤 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 )
83 nfcv ⊢ Ⅎ 𝑤 ⦋ 𝑧 / 𝑘 ⦌ 𝐶
84 83 67 69 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) = ( 𝑤 ∈ 𝐴 ↦ ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
85 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )
86 85 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )
87 nfcv ⊢ Ⅎ 𝑘 𝐴
88 87 59 nfmpt ⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
89 nfcv ⊢ Ⅎ 𝑘 ⇝𝑟
90 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐷
91 88 89 90 nfbr ⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ⇝𝑟 ⦋ 𝑧 / 𝑘 ⦌ 𝐷
92 61 mpteq2dv ⊢ ( 𝑘 = 𝑧 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
93 csbeq1a ⊢ ( 𝑘 = 𝑧 → 𝐷 = ⦋ 𝑧 / 𝑘 ⦌ 𝐷 )
94 92 93 breq12d ⊢ ( 𝑘 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 ↔ ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ⇝𝑟 ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ) )
95 91 94 rspc ⊢ ( 𝑧 ∈ 𝐵 → ( ∀ 𝑘 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ⇝𝑟 ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ) )
96 52 86 95 sylc ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ⇝𝑟 ⦋ 𝑧 / 𝑘 ⦌ 𝐷 )
97 96 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ⇝𝑟 ⦋ 𝑧 / 𝑘 ⦌ 𝐷 )
98 84 97 eqbrtrrid ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( 𝑤 ∈ 𝐴 ↦ ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ⇝𝑟 ⦋ 𝑧 / 𝑘 ⦌ 𝐷 )
99 47 73 82 98 rlimadd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( 𝑤 ∈ 𝐴 ↦ ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 + ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) ⇝𝑟 ( Σ 𝑘 ∈ 𝑦 𝐷 + ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ) )
100 simprl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ¬ 𝑧 ∈ 𝑦 )
101 disjsn ⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
102 100 101 sylibr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
103 102 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
104 eqidd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∪ { 𝑧 } ) = ( 𝑦 ∪ { 𝑧 } ) )
105 2 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → 𝐵 ∈ Fin )
106 105 48 ssfid ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
107 106 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
108 48 sselda ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑘 ∈ 𝐵 )
109 108 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑘 ∈ 𝐵 )
110 109 57 syldan ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝐶 ∈ ℂ )
111 103 104 107 110 fsumsplit ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 = ( Σ 𝑘 ∈ 𝑦 𝐶 + Σ 𝑘 ∈ { 𝑧 } 𝐶 ) )
112 csbeq1a ⊢ ( 𝑘 = 𝑤 → 𝐶 = ⦋ 𝑤 / 𝑘 ⦌ 𝐶 )
113 nfcv ⊢ Ⅎ 𝑤 𝐶
114 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑤 / 𝑘 ⦌ 𝐶
115 112 113 114 cbvsum ⊢ Σ 𝑘 ∈ { 𝑧 } 𝐶 = Σ 𝑤 ∈ { 𝑧 } ⦋ 𝑤 / 𝑘 ⦌ 𝐶
116 csbeq1 ⊢ ( 𝑤 = 𝑧 → ⦋ 𝑤 / 𝑘 ⦌ 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
117 116 sumsn ⊢ ( ( 𝑧 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ ) → Σ 𝑤 ∈ { 𝑧 } ⦋ 𝑤 / 𝑘 ⦌ 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
118 53 64 117 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑤 ∈ { 𝑧 } ⦋ 𝑤 / 𝑘 ⦌ 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
119 115 118 eqtrid ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ { 𝑧 } 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
120 119 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( Σ 𝑘 ∈ 𝑦 𝐶 + Σ 𝑘 ∈ { 𝑧 } 𝐶 ) = ( Σ 𝑘 ∈ 𝑦 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
121 111 120 eqtrd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 = ( Σ 𝑘 ∈ 𝑦 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
122 121 mpteq2dva ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( Σ 𝑘 ∈ 𝑦 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) )
123 122 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( Σ 𝑘 ∈ 𝑦 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) )
124 nfcv ⊢ Ⅎ 𝑤 ( Σ 𝑘 ∈ 𝑦 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
125 nfcv ⊢ Ⅎ 𝑥 +
126 77 125 67 nfov ⊢ Ⅎ 𝑥 ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 + ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
127 79 69 oveq12d ⊢ ( 𝑥 = 𝑤 → ( Σ 𝑘 ∈ 𝑦 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) = ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 + ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
128 124 126 127 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( Σ 𝑘 ∈ 𝑦 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) = ( 𝑤 ∈ 𝐴 ↦ ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 + ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
129 123 128 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) = ( 𝑤 ∈ 𝐴 ↦ ( Σ 𝑘 ∈ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝐶 + ⦋ 𝑤 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) )
130 eqidd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑦 ∪ { 𝑧 } ) = ( 𝑦 ∪ { 𝑧 } ) )
131 rlimcl ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ )
132 4 131 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐷 ∈ ℂ )
133 132 adantlr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) → 𝐷 ∈ ℂ )
134 108 133 syldan ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝐷 ∈ ℂ )
135 102 130 106 134 fsumsplit ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 = ( Σ 𝑘 ∈ 𝑦 𝐷 + Σ 𝑘 ∈ { 𝑧 } 𝐷 ) )
136 csbeq1a ⊢ ( 𝑘 = 𝑤 → 𝐷 = ⦋ 𝑤 / 𝑘 ⦌ 𝐷 )
137 nfcv ⊢ Ⅎ 𝑤 𝐷
138 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑤 / 𝑘 ⦌ 𝐷
139 136 137 138 cbvsum ⊢ Σ 𝑘 ∈ { 𝑧 } 𝐷 = Σ 𝑤 ∈ { 𝑧 } ⦋ 𝑤 / 𝑘 ⦌ 𝐷
140 133 ralrimiva ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 𝐷 ∈ ℂ )
141 90 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ∈ ℂ
142 93 eleq1d ⊢ ( 𝑘 = 𝑧 → ( 𝐷 ∈ ℂ ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ∈ ℂ ) )
143 141 142 rspc ⊢ ( 𝑧 ∈ 𝐵 → ( ∀ 𝑘 ∈ 𝐵 𝐷 ∈ ℂ → ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ∈ ℂ ) )
144 52 140 143 sylc ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ∈ ℂ )
145 csbeq1 ⊢ ( 𝑤 = 𝑧 → ⦋ 𝑤 / 𝑘 ⦌ 𝐷 = ⦋ 𝑧 / 𝑘 ⦌ 𝐷 )
146 145 sumsn ⊢ ( ( 𝑧 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ∈ ℂ ) → Σ 𝑤 ∈ { 𝑧 } ⦋ 𝑤 / 𝑘 ⦌ 𝐷 = ⦋ 𝑧 / 𝑘 ⦌ 𝐷 )
147 52 144 146 syl2anc ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → Σ 𝑤 ∈ { 𝑧 } ⦋ 𝑤 / 𝑘 ⦌ 𝐷 = ⦋ 𝑧 / 𝑘 ⦌ 𝐷 )
148 139 147 eqtrid ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → Σ 𝑘 ∈ { 𝑧 } 𝐷 = ⦋ 𝑧 / 𝑘 ⦌ 𝐷 )
149 148 oveq2d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( Σ 𝑘 ∈ 𝑦 𝐷 + Σ 𝑘 ∈ { 𝑧 } 𝐷 ) = ( Σ 𝑘 ∈ 𝑦 𝐷 + ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ) )
150 135 149 eqtrd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 = ( Σ 𝑘 ∈ 𝑦 𝐷 + ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ) )
151 150 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 = ( Σ 𝑘 ∈ 𝑦 𝐷 + ⦋ 𝑧 / 𝑘 ⦌ 𝐷 ) )
152 99 129 151 3brtr4d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 )
153 152 ex ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) )
154 153 expr ⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) ) )
155 154 a2d ⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) ) )
156 45 155 syl5 ⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝑦 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) ) )
157 156 expcom ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝜑 → ( ( 𝑦 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) ) ) )
158 157 a2d ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝜑 → ( 𝑦 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) ) → ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) ) ) )
159 158 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝜑 → ( 𝑦 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑦 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝑦 𝐷 ) ) → ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐷 ) ) ) )
160 16 23 30 37 41 159 findcard2s ⊢ ( 𝐵 ∈ Fin → ( 𝜑 → ( 𝐵 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝐵 𝐷 ) ) )
161 2 160 mpcom ⊢ ( 𝜑 → ( 𝐵 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝐵 𝐷 ) )
162 5 161 mpi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ⇝𝑟 Σ 𝑘 ∈ 𝐵 𝐷 )