Theorem i1fima2sn

Description: Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014)

	Ref	Expression
Assertion	i1fima2sn	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge A\in \left(B\setminus \left\{0\right\}\right)\right)\to vol\left(F^{-1}\left[\left\{A\right\}\right]\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eldifn	$$⊢A\in \left(B\setminus \left\{0\right\}\right)\to \neg A\in \left\{0\right\}$$
2		elsni	$$⊢0\in \left\{A\right\}\to 0=A$$
3		snidg	$$⊢0\in \left\{A\right\}\to 0\in \left\{0\right\}$$
4	2 3	eqeltrrd	$$⊢0\in \left\{A\right\}\to A\in \left\{0\right\}$$
5	1 4	nsyl	$$⊢A\in \left(B\setminus \left\{0\right\}\right)\to \neg 0\in \left\{A\right\}$$
6		i1fima2	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge \neg 0\in \left\{A\right\}\right)\to vol\left(F^{-1}\left[\left\{A\right\}\right]\right)\in ℝ$$
7	5 6	sylan2	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge A\in \left(B\setminus \left\{0\right\}\right)\right)\to vol\left(F^{-1}\left[\left\{A\right\}\right]\right)\in ℝ$$