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 syl5eq ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ { 𝑧 } 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
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) )