Metamath Proof Explorer


Theorem fsumo1

Description: The finite sum of eventually bounded functions (where the index set B does not depend on x ) is eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016) (Proof shortened by Mario Carneiro, 22-May-2016)

Ref Expression
Hypotheses fsumo1.1 ( 𝜑𝐴 ⊆ ℝ )
fsumo1.2 ( 𝜑𝐵 ∈ Fin )
fsumo1.3 ( ( 𝜑 ∧ ( 𝑥𝐴𝑘𝐵 ) ) → 𝐶𝑉 )
fsumo1.4 ( ( 𝜑𝑘𝐵 ) → ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) )
Assertion fsumo1 ( 𝜑 → ( 𝑥𝐴 ↦ Σ 𝑘𝐵 𝐶 ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 fsumo1.1 ( 𝜑𝐴 ⊆ ℝ )
2 fsumo1.2 ( 𝜑𝐵 ∈ Fin )
3 fsumo1.3 ( ( 𝜑 ∧ ( 𝑥𝐴𝑘𝐵 ) ) → 𝐶𝑉 )
4 fsumo1.4 ( ( 𝜑𝑘𝐵 ) → ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) )
5 ssid 𝐵𝐵
6 sseq1 ( 𝑤 = ∅ → ( 𝑤𝐵 ↔ ∅ ⊆ 𝐵 ) )
7 sumeq1 ( 𝑤 = ∅ → Σ 𝑘𝑤 𝐶 = Σ 𝑘 ∈ ∅ 𝐶 )
8 sum0 Σ 𝑘 ∈ ∅ 𝐶 = 0
9 7 8 eqtrdi ( 𝑤 = ∅ → Σ 𝑘𝑤 𝐶 = 0 )
10 9 mpteq2dv ( 𝑤 = ∅ → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) = ( 𝑥𝐴 ↦ 0 ) )
11 10 eleq1d ( 𝑤 = ∅ → ( ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ↔ ( 𝑥𝐴 ↦ 0 ) ∈ 𝑂(1) ) )
12 6 11 imbi12d ( 𝑤 = ∅ → ( ( 𝑤𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ) ↔ ( ∅ ⊆ 𝐵 → ( 𝑥𝐴 ↦ 0 ) ∈ 𝑂(1) ) ) )
13 12 imbi2d ( 𝑤 = ∅ → ( ( 𝜑 → ( 𝑤𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐵 → ( 𝑥𝐴 ↦ 0 ) ∈ 𝑂(1) ) ) ) )
14 sseq1 ( 𝑤 = 𝑦 → ( 𝑤𝐵𝑦𝐵 ) )
15 sumeq1 ( 𝑤 = 𝑦 → Σ 𝑘𝑤 𝐶 = Σ 𝑘𝑦 𝐶 )
16 15 mpteq2dv ( 𝑤 = 𝑦 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) = ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) )
17 16 eleq1d ( 𝑤 = 𝑦 → ( ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ↔ ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) )
18 14 17 imbi12d ( 𝑤 = 𝑦 → ( ( 𝑤𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ) ↔ ( 𝑦𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) ) )
19 18 imbi2d ( 𝑤 = 𝑦 → ( ( 𝜑 → ( 𝑤𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ) ) ↔ ( 𝜑 → ( 𝑦𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) ) ) )
20 sseq1 ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑤𝐵 ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) )
21 sumeq1 ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑘𝑤 𝐶 = Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 )
22 21 mpteq2dv ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) = ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) )
23 22 eleq1d ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ↔ ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) )
24 20 23 imbi12d ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑤𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ) ↔ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) ) )
25 24 imbi2d ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝜑 → ( 𝑤𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ) ) ↔ ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) ) ) )
26 sseq1 ( 𝑤 = 𝐵 → ( 𝑤𝐵𝐵𝐵 ) )
27 sumeq1 ( 𝑤 = 𝐵 → Σ 𝑘𝑤 𝐶 = Σ 𝑘𝐵 𝐶 )
28 27 mpteq2dv ( 𝑤 = 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) = ( 𝑥𝐴 ↦ Σ 𝑘𝐵 𝐶 ) )
29 28 eleq1d ( 𝑤 = 𝐵 → ( ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ↔ ( 𝑥𝐴 ↦ Σ 𝑘𝐵 𝐶 ) ∈ 𝑂(1) ) )
30 26 29 imbi12d ( 𝑤 = 𝐵 → ( ( 𝑤𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ) ↔ ( 𝐵𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝐵 𝐶 ) ∈ 𝑂(1) ) ) )
31 30 imbi2d ( 𝑤 = 𝐵 → ( ( 𝜑 → ( 𝑤𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑤 𝐶 ) ∈ 𝑂(1) ) ) ↔ ( 𝜑 → ( 𝐵𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝐵 𝐶 ) ∈ 𝑂(1) ) ) ) )
32 0cn 0 ∈ ℂ
33 o1const ( ( 𝐴 ⊆ ℝ ∧ 0 ∈ ℂ ) → ( 𝑥𝐴 ↦ 0 ) ∈ 𝑂(1) )
34 1 32 33 sylancl ( 𝜑 → ( 𝑥𝐴 ↦ 0 ) ∈ 𝑂(1) )
35 34 a1d ( 𝜑 → ( ∅ ⊆ 𝐵 → ( 𝑥𝐴 ↦ 0 ) ∈ 𝑂(1) ) )
36 ssun1 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
37 sstr ( ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) → 𝑦𝐵 )
38 36 37 mpan ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵𝑦𝐵 )
39 38 imim1i ( ( 𝑦𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) )
40 simprl ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ¬ 𝑧𝑦 )
41 disjsn ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧𝑦 )
42 40 41 sylibr ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
43 42 adantr ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
44 eqidd ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → ( 𝑦 ∪ { 𝑧 } ) = ( 𝑦 ∪ { 𝑧 } ) )
45 2 adantr ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → 𝐵 ∈ Fin )
46 simprr ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 )
47 45 46 ssfid ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
48 47 adantr ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
49 46 sselda ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑘𝐵 )
50 49 adantlr ( ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑘𝐵 )
51 3 anass1rs ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) → 𝐶𝑉 )
52 51 4 o1mptrcl ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑥𝐴 ) → 𝐶 ∈ ℂ )
53 52 an32s ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑘𝐵 ) → 𝐶 ∈ ℂ )
54 53 adantllr ( ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑘𝐵 ) → 𝐶 ∈ ℂ )
55 50 54 syldan ( ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) ∧ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝐶 ∈ ℂ )
56 43 44 48 55 fsumsplit ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 = ( Σ 𝑘𝑦 𝐶 + Σ 𝑘 ∈ { 𝑧 } 𝐶 ) )
57 nfcv 𝑤 𝐶
58 nfcsb1v 𝑘 𝑤 / 𝑘 𝐶
59 csbeq1a ( 𝑘 = 𝑤𝐶 = 𝑤 / 𝑘 𝐶 )
60 57 58 59 cbvsumi Σ 𝑘 ∈ { 𝑧 } 𝐶 = Σ 𝑤 ∈ { 𝑧 } 𝑤 / 𝑘 𝐶
61 46 unssbd ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → { 𝑧 } ⊆ 𝐵 )
62 vex 𝑧 ∈ V
63 62 snss ( 𝑧𝐵 ↔ { 𝑧 } ⊆ 𝐵 )
64 61 63 sylibr ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → 𝑧𝐵 )
65 64 adantr ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → 𝑧𝐵 )
66 54 ralrimiva ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → ∀ 𝑘𝐵 𝐶 ∈ ℂ )
67 nfcsb1v 𝑘 𝑧 / 𝑘 𝐶
68 67 nfel1 𝑘 𝑧 / 𝑘 𝐶 ∈ ℂ
69 csbeq1a ( 𝑘 = 𝑧𝐶 = 𝑧 / 𝑘 𝐶 )
70 69 eleq1d ( 𝑘 = 𝑧 → ( 𝐶 ∈ ℂ ↔ 𝑧 / 𝑘 𝐶 ∈ ℂ ) )
71 68 70 rspc ( 𝑧𝐵 → ( ∀ 𝑘𝐵 𝐶 ∈ ℂ → 𝑧 / 𝑘 𝐶 ∈ ℂ ) )
72 65 66 71 sylc ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → 𝑧 / 𝑘 𝐶 ∈ ℂ )
73 csbeq1 ( 𝑤 = 𝑧 𝑤 / 𝑘 𝐶 = 𝑧 / 𝑘 𝐶 )
74 73 sumsn ( ( 𝑧𝐵 𝑧 / 𝑘 𝐶 ∈ ℂ ) → Σ 𝑤 ∈ { 𝑧 } 𝑤 / 𝑘 𝐶 = 𝑧 / 𝑘 𝐶 )
75 65 72 74 syl2anc ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → Σ 𝑤 ∈ { 𝑧 } 𝑤 / 𝑘 𝐶 = 𝑧 / 𝑘 𝐶 )
76 60 75 eqtrid ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → Σ 𝑘 ∈ { 𝑧 } 𝐶 = 𝑧 / 𝑘 𝐶 )
77 76 oveq2d ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → ( Σ 𝑘𝑦 𝐶 + Σ 𝑘 ∈ { 𝑧 } 𝐶 ) = ( Σ 𝑘𝑦 𝐶 + 𝑧 / 𝑘 𝐶 ) )
78 56 77 eqtrd ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 = ( Σ 𝑘𝑦 𝐶 + 𝑧 / 𝑘 𝐶 ) )
79 78 mpteq2dva ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) = ( 𝑥𝐴 ↦ ( Σ 𝑘𝑦 𝐶 + 𝑧 / 𝑘 𝐶 ) ) )
80 1 adantr ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → 𝐴 ⊆ ℝ )
81 reex ℝ ∈ V
82 81 ssex ( 𝐴 ⊆ ℝ → 𝐴 ∈ V )
83 80 82 syl ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → 𝐴 ∈ V )
84 sumex Σ 𝑘𝑦 𝐶 ∈ V
85 84 a1i ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥𝐴 ) → Σ 𝑘𝑦 𝐶 ∈ V )
86 eqidd ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) = ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) )
87 eqidd ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) = ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) )
88 83 85 72 86 87 offval2 ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∘f + ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ) = ( 𝑥𝐴 ↦ ( Σ 𝑘𝑦 𝐶 + 𝑧 / 𝑘 𝐶 ) ) )
89 79 88 eqtr4d ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) = ( ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∘f + ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ) )
90 89 adantr ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) = ( ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∘f + ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ) )
91 id ( ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) )
92 4 ralrimiva ( 𝜑 → ∀ 𝑘𝐵 ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) )
93 92 adantr ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ∀ 𝑘𝐵 ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) )
94 nfcv 𝑘 𝐴
95 94 67 nfmpt 𝑘 ( 𝑥𝐴 𝑧 / 𝑘 𝐶 )
96 95 nfel1 𝑘 ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ∈ 𝑂(1)
97 69 mpteq2dv ( 𝑘 = 𝑧 → ( 𝑥𝐴𝐶 ) = ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) )
98 97 eleq1d ( 𝑘 = 𝑧 → ( ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) ↔ ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ∈ 𝑂(1) ) )
99 96 98 rspc ( 𝑧𝐵 → ( ∀ 𝑘𝐵 ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) → ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ∈ 𝑂(1) ) )
100 64 93 99 sylc ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ∈ 𝑂(1) )
101 o1add ( ( ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ∧ ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ∈ 𝑂(1) ) → ( ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∘f + ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ) ∈ 𝑂(1) )
102 91 100 101 syl2anr ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) → ( ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∘f + ( 𝑥𝐴 𝑧 / 𝑘 𝐶 ) ) ∈ 𝑂(1) )
103 90 102 eqeltrd ( ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) )
104 103 ex ( ( 𝜑 ∧ ( ¬ 𝑧𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) )
105 104 expr ( ( 𝜑 ∧ ¬ 𝑧𝑦 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) ) )
106 105 a2d ( ( 𝜑 ∧ ¬ 𝑧𝑦 ) → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) ) )
107 39 106 syl5 ( ( 𝜑 ∧ ¬ 𝑧𝑦 ) → ( ( 𝑦𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) ) )
108 107 expcom ( ¬ 𝑧𝑦 → ( 𝜑 → ( ( 𝑦𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) ) ) )
109 108 a2d ( ¬ 𝑧𝑦 → ( ( 𝜑 → ( 𝑦𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) ) → ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) ) ) )
110 109 adantl ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) → ( ( 𝜑 → ( 𝑦𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝑦 𝐶 ) ∈ 𝑂(1) ) ) → ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝑂(1) ) ) ) )
111 13 19 25 31 35 110 findcard2s ( 𝐵 ∈ Fin → ( 𝜑 → ( 𝐵𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝐵 𝐶 ) ∈ 𝑂(1) ) ) )
112 2 111 mpcom ( 𝜑 → ( 𝐵𝐵 → ( 𝑥𝐴 ↦ Σ 𝑘𝐵 𝐶 ) ∈ 𝑂(1) ) )
113 5 112 mpi ( 𝜑 → ( 𝑥𝐴 ↦ Σ 𝑘𝐵 𝐶 ) ∈ 𝑂(1) )