Theorem i1f1lem

Description: Lemma for i1f1 and itg11 . (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Hypothesis	i1f1.1	$$⊢F=\left(x\in ℝ⟼if\left(x\in A,1,0\right)\right)$$
Assertion	i1f1lem	$$⊢\left(F:ℝ⟶\left\{0,1\right\}\wedge \left(A\in \mathrm{dom}vol\to F^{-1}\left[\left\{1\right\}\right]=A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		i1f1.1	$$⊢F=\left(x\in ℝ⟼if\left(x\in A,1,0\right)\right)$$
2		1elpr01	$$⊢1\in \left\{0,1\right\}$$
3		0elpr01	$$⊢0\in \left\{0,1\right\}$$
4	2 3	ifcli	$$⊢if\left(x\in A,1,0\right)\in \left\{0,1\right\}$$
5	4	rgenw	$$⊢\forall x\in ℝif\left(x\in A,1,0\right)\in \left\{0,1\right\}$$
6	1	fmpt	$$⊢\forall x\in ℝif\left(x\in A,1,0\right)\in \left\{0,1\right\}\leftrightarrow F:ℝ⟶\left\{0,1\right\}$$
7	5 6	mpbi	$$⊢F:ℝ⟶\left\{0,1\right\}$$
8	4	a1i	$$⊢\left(A\in \mathrm{dom}vol\wedge x\in ℝ\right)\to if\left(x\in A,1,0\right)\in \left\{0,1\right\}$$
9	8 1	fmptd	$$⊢A\in \mathrm{dom}vol\to F:ℝ⟶\left\{0,1\right\}$$
10		ffn	$$⊢F:ℝ⟶\left\{0,1\right\}\to FFnℝ$$
11		elpreima	$$⊢FFnℝ\to \left(y\in F^{-1}\left[\left\{1\right\}\right]\leftrightarrow \left(y\in ℝ\wedge F\left(y\right)\in \left\{1\right\}\right)\right)$$
12	9 10 11	3syl	$$⊢A\in \mathrm{dom}vol\to \left(y\in F^{-1}\left[\left\{1\right\}\right]\leftrightarrow \left(y\in ℝ\wedge F\left(y\right)\in \left\{1\right\}\right)\right)$$
13		fvex	$$⊢F\left(y\right)\in \mathrm{V}$$
14	13	elsn	$$⊢F\left(y\right)\in \left\{1\right\}\leftrightarrow F\left(y\right)=1$$
15		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
16	15	ifbid	$$⊢x=y\to if\left(x\in A,1,0\right)=if\left(y\in A,1,0\right)$$
17		1ex	$$⊢1\in \mathrm{V}$$
18		c0ex	$$⊢0\in \mathrm{V}$$
19	17 18	ifex	$$⊢if\left(y\in A,1,0\right)\in \mathrm{V}$$
20	16 1 19	fvmpt	$$⊢y\in ℝ\to F\left(y\right)=if\left(y\in A,1,0\right)$$
21	20	eqeq1d	$$⊢y\in ℝ\to \left(F\left(y\right)=1\leftrightarrow if\left(y\in A,1,0\right)=1\right)$$
22		0ne1	$$⊢0\ne 1$$
23		iffalse	$$⊢\neg y\in A\to if\left(y\in A,1,0\right)=0$$
24	23	eqeq1d	$$⊢\neg y\in A\to \left(if\left(y\in A,1,0\right)=1\leftrightarrow 0=1\right)$$
25	24	necon3bbid	$$⊢\neg y\in A\to \left(\neg if\left(y\in A,1,0\right)=1\leftrightarrow 0\ne 1\right)$$
26	22 25	mpbiri	$$⊢\neg y\in A\to \neg if\left(y\in A,1,0\right)=1$$
27	26	con4i	$$⊢if\left(y\in A,1,0\right)=1\to y\in A$$
28		iftrue	$$⊢y\in A\to if\left(y\in A,1,0\right)=1$$
29	27 28	impbii	$$⊢if\left(y\in A,1,0\right)=1\leftrightarrow y\in A$$
30	21 29	bitrdi	$$⊢y\in ℝ\to \left(F\left(y\right)=1\leftrightarrow y\in A\right)$$
31	14 30	bitrid	$$⊢y\in ℝ\to \left(F\left(y\right)\in \left\{1\right\}\leftrightarrow y\in A\right)$$
32	31	pm5.32i	$$⊢\left(y\in ℝ\wedge F\left(y\right)\in \left\{1\right\}\right)\leftrightarrow \left(y\in ℝ\wedge y\in A\right)$$
33	12 32	bitrdi	$$⊢A\in \mathrm{dom}vol\to \left(y\in F^{-1}\left[\left\{1\right\}\right]\leftrightarrow \left(y\in ℝ\wedge y\in A\right)\right)$$
34		mblss	$$⊢A\in \mathrm{dom}vol\to A\subseteq ℝ$$
35	34	sseld	$$⊢A\in \mathrm{dom}vol\to \left(y\in A\to y\in ℝ\right)$$
36	35	pm4.71rd	$$⊢A\in \mathrm{dom}vol\to \left(y\in A\leftrightarrow \left(y\in ℝ\wedge y\in A\right)\right)$$
37	33 36	bitr4d	$$⊢A\in \mathrm{dom}vol\to \left(y\in F^{-1}\left[\left\{1\right\}\right]\leftrightarrow y\in A\right)$$
38	37	eqrdv	$$⊢A\in \mathrm{dom}vol\to F^{-1}\left[\left\{1\right\}\right]=A$$
39	7 38	pm3.2i	$$⊢\left(F:ℝ⟶\left\{0,1\right\}\wedge \left(A\in \mathrm{dom}vol\to F^{-1}\left[\left\{1\right\}\right]=A\right)\right)$$