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		1ex	$$⊢1\in \mathrm{V}$$
3	2	prid2	$$⊢1\in \left\{0,1\right\}$$
4		c0ex	$$⊢0\in \mathrm{V}$$
5	4	prid1	$$⊢0\in \left\{0,1\right\}$$
6	3 5	ifcli	$$⊢if\left(x\in A,1,0\right)\in \left\{0,1\right\}$$
7	6	rgenw	$$⊢\forall x\in ℝif\left(x\in A,1,0\right)\in \left\{0,1\right\}$$
8	1	fmpt	$$⊢\forall x\in ℝif\left(x\in A,1,0\right)\in \left\{0,1\right\}\leftrightarrow F:ℝ⟶\left\{0,1\right\}$$
9	7 8	mpbi	$$⊢F:ℝ⟶\left\{0,1\right\}$$
10	6	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\}$$
11	10 1	fmptd	$$⊢A\in \mathrm{dom}vol\to F:ℝ⟶\left\{0,1\right\}$$
12		ffn	$$⊢F:ℝ⟶\left\{0,1\right\}\to FFnℝ$$
13		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)$$
14	11 12 13	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)$$
15		fvex	$$⊢F\left(y\right)\in \mathrm{V}$$
16	15	elsn	$$⊢F\left(y\right)\in \left\{1\right\}\leftrightarrow F\left(y\right)=1$$
17		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
18	17	ifbid	$$⊢x=y\to if\left(x\in A,1,0\right)=if\left(y\in A,1,0\right)$$
19	2 4	ifex	$$⊢if\left(y\in A,1,0\right)\in \mathrm{V}$$
20	18 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	16 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	14 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	9 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)$$