Metamath Proof Explorer

Theorem ovnsubadd2lem

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovnsubadd2lem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
ovnsubadd2lem.a ⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
ovnsubadd2lem.b ⊢ ( 𝜑 → 𝐵 ⊆ ( ℝ ↑m 𝑋 ) )
ovnsubadd2lem.c ⊢ 𝐶 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) )
Assertion ovnsubadd2lem ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ovnsubadd2lem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ovnsubadd2lem.a ⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3 ovnsubadd2lem.b ⊢ ( 𝜑 → 𝐵 ⊆ ( ℝ ↑m 𝑋 ) )
4 ovnsubadd2lem.c ⊢ 𝐶 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) )
5 iftrue ⊢ ( 𝑛 = 1 → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = 𝐴 )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = 𝐴 )
7 ovexd ⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) ∈ V )
8 7 2 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
9 8 2 elpwd ⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
11 6 10 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
12 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑛 = 1 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
13 simpl ⊢ ( ( ¬ 𝑛 = 1 ∧ 𝑛 = 2 ) → ¬ 𝑛 = 1 )
14 13 iffalsed ⊢ ( ( ¬ 𝑛 = 1 ∧ 𝑛 = 2 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = if ( 𝑛 = 2 , 𝐵 , ∅ ) )
15 simpr ⊢ ( ( ¬ 𝑛 = 1 ∧ 𝑛 = 2 ) → 𝑛 = 2 )
16 15 iftrued ⊢ ( ( ¬ 𝑛 = 1 ∧ 𝑛 = 2 ) → if ( 𝑛 = 2 , 𝐵 , ∅ ) = 𝐵 )
17 14 16 eqtrd ⊢ ( ( ¬ 𝑛 = 1 ∧ 𝑛 = 2 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = 𝐵 )
18 17 adantll ⊢ ( ( ( 𝜑 ∧ ¬ 𝑛 = 1 ) ∧ 𝑛 = 2 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = 𝐵 )
19 7 3 ssexd ⊢ ( 𝜑 → 𝐵 ∈ V )
20 19 3 elpwd ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑛 = 1 ) ∧ 𝑛 = 2 ) → 𝐵 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
22 18 21 eqeltrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑛 = 1 ) ∧ 𝑛 = 2 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
23 22 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ 𝑛 = 1 ) ∧ 𝑛 = 2 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
24 simpl ⊢ ( ( ¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2 ) → ¬ 𝑛 = 1 )
25 24 iffalsed ⊢ ( ( ¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = if ( 𝑛 = 2 , 𝐵 , ∅ ) )
26 simpr ⊢ ( ( ¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2 ) → ¬ 𝑛 = 2 )
27 26 iffalsed ⊢ ( ( ¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2 ) → if ( 𝑛 = 2 , 𝐵 , ∅ ) = ∅ )
28 25 27 eqtrd ⊢ ( ( ¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = ∅ )
29 0elpw ⊢ ∅ ∈ 𝒫 ( ℝ ↑m 𝑋 )
30 29 a1i ⊢ ( ( ¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2 ) → ∅ ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
31 28 30 eqeltrd ⊢ ( ( ¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
32 31 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ 𝑛 = 1 ) ∧ ¬ 𝑛 = 2 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
33 23 32 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ 𝑛 = 1 ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
34 12 33 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
35 34 4 fmptd ⊢ ( 𝜑 → 𝐶 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
36 1 35 ovnsubadd ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐶 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) ) ) )
37 eldifi ⊢ ( 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) → 𝑛 ∈ ℕ )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ) → 𝑛 ∈ ℕ )
39 eldifn ⊢ ( 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) → ¬ 𝑛 ∈ { 1 , 2 } )
40 vex ⊢ 𝑛 ∈ V
41 40 a1i ⊢ ( ¬ 𝑛 ∈ { 1 , 2 } → 𝑛 ∈ V )
42 id ⊢ ( ¬ 𝑛 ∈ { 1 , 2 } → ¬ 𝑛 ∈ { 1 , 2 } )
43 41 42 nelpr1 ⊢ ( ¬ 𝑛 ∈ { 1 , 2 } → 𝑛 ≠ 1 )
44 43 neneqd ⊢ ( ¬ 𝑛 ∈ { 1 , 2 } → ¬ 𝑛 = 1 )
45 39 44 syl ⊢ ( 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) → ¬ 𝑛 = 1 )
46 41 42 nelpr2 ⊢ ( ¬ 𝑛 ∈ { 1 , 2 } → 𝑛 ≠ 2 )
47 46 neneqd ⊢ ( ¬ 𝑛 ∈ { 1 , 2 } → ¬ 𝑛 = 2 )
48 39 47 syl ⊢ ( 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) → ¬ 𝑛 = 2 )
49 45 48 28 syl2anc ⊢ ( 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = ∅ )
50 0ex ⊢ ∅ ∈ V
51 50 a1i ⊢ ( 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) → ∅ ∈ V )
52 49 51 eqeltrd ⊢ ( 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ V )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ V )
54 4 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) ∈ V ) → ( 𝐶 ‘ 𝑛 ) = if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) )
55 38 53 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ) → ( 𝐶 ‘ 𝑛 ) = if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) )
56 49 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ) → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = ∅ )
57 55 56 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ) → ( 𝐶 ‘ 𝑛 ) = ∅ )
58 57 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ( 𝐶 ‘ 𝑛 ) = ∅ )
59 nfcv ⊢ Ⅎ 𝑛 ( ℕ ∖ { 1 , 2 } )
60 59 iunxdif3 ⊢ ( ∀ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ( 𝐶 ‘ 𝑛 ) = ∅ → ∪ 𝑛 ∈ ( ℕ ∖ ( ℕ ∖ { 1 , 2 } ) ) ( 𝐶 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝐶 ‘ 𝑛 ) )
61 58 60 syl ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( ℕ ∖ ( ℕ ∖ { 1 , 2 } ) ) ( 𝐶 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝐶 ‘ 𝑛 ) )
62 61 eqcomd ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐶 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( ℕ ∖ ( ℕ ∖ { 1 , 2 } ) ) ( 𝐶 ‘ 𝑛 ) )
63 1nn ⊢ 1 ∈ ℕ
64 2nn ⊢ 2 ∈ ℕ
65 63 64 pm3.2i ⊢ ( 1 ∈ ℕ ∧ 2 ∈ ℕ )
66 prssi ⊢ ( ( 1 ∈ ℕ ∧ 2 ∈ ℕ ) → { 1 , 2 } ⊆ ℕ )
67 65 66 ax-mp ⊢ { 1 , 2 } ⊆ ℕ
68 dfss4 ⊢ ( { 1 , 2 } ⊆ ℕ ↔ ( ℕ ∖ ( ℕ ∖ { 1 , 2 } ) ) = { 1 , 2 } )
69 67 68 mpbi ⊢ ( ℕ ∖ ( ℕ ∖ { 1 , 2 } ) ) = { 1 , 2 }
70 iuneq1 ⊢ ( ( ℕ ∖ ( ℕ ∖ { 1 , 2 } ) ) = { 1 , 2 } → ∪ 𝑛 ∈ ( ℕ ∖ ( ℕ ∖ { 1 , 2 } ) ) ( 𝐶 ‘ 𝑛 ) = ∪ 𝑛 ∈ { 1 , 2 } ( 𝐶 ‘ 𝑛 ) )
71 69 70 ax-mp ⊢ ∪ 𝑛 ∈ ( ℕ ∖ ( ℕ ∖ { 1 , 2 } ) ) ( 𝐶 ‘ 𝑛 ) = ∪ 𝑛 ∈ { 1 , 2 } ( 𝐶 ‘ 𝑛 )
72 71 a1i ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( ℕ ∖ ( ℕ ∖ { 1 , 2 } ) ) ( 𝐶 ‘ 𝑛 ) = ∪ 𝑛 ∈ { 1 , 2 } ( 𝐶 ‘ 𝑛 ) )
73 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐶 ‘ 𝑛 ) = ( 𝐶 ‘ 1 ) )
74 fveq2 ⊢ ( 𝑛 = 2 → ( 𝐶 ‘ 𝑛 ) = ( 𝐶 ‘ 2 ) )
75 73 74 iunxprg ⊢ ( ( 1 ∈ ℕ ∧ 2 ∈ ℕ ) → ∪ 𝑛 ∈ { 1 , 2 } ( 𝐶 ‘ 𝑛 ) = ( ( 𝐶 ‘ 1 ) ∪ ( 𝐶 ‘ 2 ) ) )
76 63 64 75 mp2an ⊢ ∪ 𝑛 ∈ { 1 , 2 } ( 𝐶 ‘ 𝑛 ) = ( ( 𝐶 ‘ 1 ) ∪ ( 𝐶 ‘ 2 ) )
77 76 a1i ⊢ ( 𝜑 → ∪ 𝑛 ∈ { 1 , 2 } ( 𝐶 ‘ 𝑛 ) = ( ( 𝐶 ‘ 1 ) ∪ ( 𝐶 ‘ 2 ) ) )
78 63 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
79 4 5 78 8 fvmptd3 ⊢ ( 𝜑 → ( 𝐶 ‘ 1 ) = 𝐴 )
80 id ⊢ ( 𝑛 = 2 → 𝑛 = 2 )
81 1ne2 ⊢ 1 ≠ 2
82 81 necomi ⊢ 2 ≠ 1
83 82 a1i ⊢ ( 𝑛 = 2 → 2 ≠ 1 )
84 80 83 eqnetrd ⊢ ( 𝑛 = 2 → 𝑛 ≠ 1 )
85 84 neneqd ⊢ ( 𝑛 = 2 → ¬ 𝑛 = 1 )
86 85 iffalsed ⊢ ( 𝑛 = 2 → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = if ( 𝑛 = 2 , 𝐵 , ∅ ) )
87 iftrue ⊢ ( 𝑛 = 2 → if ( 𝑛 = 2 , 𝐵 , ∅ ) = 𝐵 )
88 86 87 eqtrd ⊢ ( 𝑛 = 2 → if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) = 𝐵 )
89 64 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
90 4 88 89 19 fvmptd3 ⊢ ( 𝜑 → ( 𝐶 ‘ 2 ) = 𝐵 )
91 79 90 uneq12d ⊢ ( 𝜑 → ( ( 𝐶 ‘ 1 ) ∪ ( 𝐶 ‘ 2 ) ) = ( 𝐴 ∪ 𝐵 ) )
92 eqidd ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )
93 77 91 92 3eqtrd ⊢ ( 𝜑 → ∪ 𝑛 ∈ { 1 , 2 } ( 𝐶 ‘ 𝑛 ) = ( 𝐴 ∪ 𝐵 ) )
94 62 72 93 3eqtrd ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐶 ‘ 𝑛 ) = ( 𝐴 ∪ 𝐵 ) )
95 94 fveq2d ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐶 ‘ 𝑛 ) ) = ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∪ 𝐵 ) ) )
96 nfv ⊢ Ⅎ 𝑛 𝜑
97 nnex ⊢ ℕ ∈ V
98 97 a1i ⊢ ( 𝜑 → ℕ ∈ V )
99 67 a1i ⊢ ( 𝜑 → { 1 , 2 } ⊆ ℕ )
100 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 1 , 2 } ) → 𝑋 ∈ Fin )
101 simpl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 1 , 2 } ) → 𝜑 )
102 99 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 1 , 2 } ) → 𝑛 ∈ ℕ )
103 35 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
104 elpwi ⊢ ( ( 𝐶 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) → ( 𝐶 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
105 103 104 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
106 101 102 105 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 1 , 2 } ) → ( 𝐶 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
107 100 106 ovncl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 1 , 2 } ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
108 57 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) = ( ( voln* ‘ 𝑋 ) ‘ ∅ ) )
109 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ) → 𝑋 ∈ Fin )
110 109 ovn0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∅ ) = 0 )
111 108 110 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ { 1 , 2 } ) ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) = 0 )
112 96 98 99 107 111 sge0ss ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ { 1 , 2 } ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) ) ) )
113 112 eqcomd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ { 1 , 2 } ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) ) ) )
114 79 2 eqsstrd ⊢ ( 𝜑 → ( 𝐶 ‘ 1 ) ⊆ ( ℝ ↑m 𝑋 ) )
115 1 114 ovncl ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 1 ) ) ∈ ( 0 [,] +∞ ) )
116 90 3 eqsstrd ⊢ ( 𝜑 → ( 𝐶 ‘ 2 ) ⊆ ( ℝ ↑m 𝑋 ) )
117 1 116 ovncl ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 2 ) ) ∈ ( 0 [,] +∞ ) )
118 2fveq3 ⊢ ( 𝑛 = 1 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) = ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 1 ) ) )
119 2fveq3 ⊢ ( 𝑛 = 2 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) = ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 2 ) ) )
120 81 a1i ⊢ ( 𝜑 → 1 ≠ 2 )
121 78 89 115 117 118 119 120 sge0pr ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ { 1 , 2 } ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) ) ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 1 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 2 ) ) ) )
122 79 fveq2d ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 1 ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
123 90 fveq2d ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 2 ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) )
124 122 123 oveq12d ⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 1 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 2 ) ) ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) ) )
125 113 121 124 3eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) ) ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) ) )
126 95 125 breq12d ⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐶 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐶 ‘ 𝑛 ) ) ) ) ↔ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) ) ) )
127 36 126 mpbid ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) ) )