Theorem cnbdibl

Description: A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cnbdibl.a	|- ( ph -> A e. dom vol )
	cnbdibl.va	|- ( ph -> ( vol ` A ) e. RR )
	cnbdibl.f	|- ( ph -> F e. ( A -cn-> CC ) )
	cnbdibl.bd	|- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )
Assertion	cnbdibl	|- ( ph -> F e. L^1 )

Proof

Step	Hyp	Ref	Expression
1		cnbdibl.a	|- ( ph -> A e. dom vol )
2		cnbdibl.va	|- ( ph -> ( vol ` A ) e. RR )
3		cnbdibl.f	|- ( ph -> F e. ( A -cn-> CC ) )
4		cnbdibl.bd	|- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )
5		cnmbf	|- ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) -> F e. MblFn )
6	1 3 5	syl2anc	|- ( ph -> F e. MblFn )
7		cncff	|- ( F e. ( A -cn-> CC ) -> F : A --> CC )
8		fdm	|- ( F : A --> CC -> dom F = A )
9	3 7 8	3syl	|- ( ph -> dom F = A )
10	9	fveq2d	|- ( ph -> ( vol ` dom F ) = ( vol ` A ) )
11	10 2	eqeltrd	|- ( ph -> ( vol ` dom F ) e. RR )
12		bddibl	|- ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> F e. L^1 )
13	6 11 4 12	syl3anc	|- ( ph -> F e. L^1 )