Theorem ovnsubadd2

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	ovnsubadd2.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnsubadd2.a	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
	ovnsubadd2.b	⊢ ( 𝜑 → 𝐵 ⊆ ( ℝ ↑m 𝑋 ) )
Assertion	ovnsubadd2	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovnsubadd2.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnsubadd2.a	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3		ovnsubadd2.b	⊢ ( 𝜑 → 𝐵 ⊆ ( ℝ ↑m 𝑋 ) )
4		eqeq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 = 1 ↔ 𝑛 = 1 ) )
5		eqeq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 = 2 ↔ 𝑛 = 2 ) )
6	5	ifbid	⊢ ( 𝑚 = 𝑛 → if ( 𝑚 = 2 , 𝐵 , ∅ ) = if ( 𝑛 = 2 , 𝐵 , ∅ ) )
7	4 6	ifbieq2d	⊢ ( 𝑚 = 𝑛 → if ( 𝑚 = 1 , 𝐴 , if ( 𝑚 = 2 , 𝐵 , ∅ ) ) = if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) )
8	7	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ if ( 𝑚 = 1 , 𝐴 , if ( 𝑚 = 2 , 𝐵 , ∅ ) ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 = 1 , 𝐴 , if ( 𝑛 = 2 , 𝐵 , ∅ ) ) )
9	1 2 3 8	ovnsubadd2lem	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) ) )