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	|- ( ph -> X e. Fin )
	ovnsubadd2.a	|- ( ph -> A C_ ( RR ^m X ) )
	ovnsubadd2.b	|- ( ph -> B C_ ( RR ^m X ) )
Assertion	ovnsubadd2	|- ( ph -> ( ( voln* ` X ) ` ( A u. B ) ) <_ ( ( ( voln* ` X ) ` A ) +e ( ( voln* ` X ) ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovnsubadd2.x	|- ( ph -> X e. Fin )
2		ovnsubadd2.a	|- ( ph -> A C_ ( RR ^m X ) )
3		ovnsubadd2.b	|- ( ph -> B C_ ( RR ^m X ) )
4		eqeq1	|- ( m = n -> ( m = 1 <-> n = 1 ) )
5		eqeq1	|- ( m = n -> ( m = 2 <-> n = 2 ) )
6	5	ifbid	|- ( m = n -> if ( m = 2 , B , (/) ) = if ( n = 2 , B , (/) ) )
7	4 6	ifbieq2d	|- ( m = n -> if ( m = 1 , A , if ( m = 2 , B , (/) ) ) = if ( n = 1 , A , if ( n = 2 , B , (/) ) ) )
8	7	cbvmptv	|- ( m e. NN |-> if ( m = 1 , A , if ( m = 2 , B , (/) ) ) ) = ( n e. NN |-> if ( n = 1 , A , if ( n = 2 , B , (/) ) ) )
9	1 2 3 8	ovnsubadd2lem	|- ( ph -> ( ( voln* ` X ) ` ( A u. B ) ) <_ ( ( ( voln* ` X ) ` A ) +e ( ( voln* ` X ) ` B ) ) )