Step |
Hyp |
Ref |
Expression |
1 |
|
ovnsplit.x |
⊢ ( 𝜑 → 𝑋 ∈ Fin ) |
2 |
|
ovnsplit.a |
⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) ) |
3 |
|
inundif |
⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 |
4 |
3
|
eqcomi |
⊢ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) |
5 |
4
|
fveq2i |
⊢ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) |
6 |
5
|
a1i |
⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ) |
7 |
2
|
ssinss1d |
⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ ( ℝ ↑m 𝑋 ) ) |
8 |
2
|
ssdifssd |
⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ ( ℝ ↑m 𝑋 ) ) |
9 |
1 7 8
|
ovnsubadd2 |
⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ 𝐵 ) ) ) ) |
10 |
6 9
|
eqbrtrd |
⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ 𝐵 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ 𝐵 ) ) ) ) |