Theorem indval2

Description: Alternate value of the indicator function generator. (Contributed by Thierry Arnoux, 2-Feb-2017)

	Ref	Expression
Assertion	indval2	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)=\left(A\times \left\{1\right\}\right)\cup \left(\left(O\setminus A\right)\times \left\{0\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfmpt3	$$⊢\left(x\in O⟼if\left(x\in A,1,0\right)\right)=\bigcup _{x\in O}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)$$
2		indval	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)=\left(x\in O⟼if\left(x\in A,1,0\right)\right)$$
3		undif	$$⊢A\subseteq O\leftrightarrow A\cup \left(O\setminus A\right)=O$$
4	3	bilani	$$⊢\left(O\in V\wedge A\subseteq O\right)\to A\cup \left(O\setminus A\right)=O$$
5	4	iuneq1d	$$⊢\left(O\in V\wedge A\subseteq O\right)\to \bigcup _{x\in A\cup \left(O\setminus A\right)}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)=\bigcup _{x\in O}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)$$
6	1 2 5	3eqtr4a	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)=\bigcup _{x\in A\cup \left(O\setminus A\right)}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)$$
7		iunxun	$$⊢\bigcup _{x\in A\cup \left(O\setminus A\right)}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)=\bigcup _{x\in A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)\cup \bigcup _{x\in O\setminus A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)$$
8	6 7	eqtrdi	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)=\bigcup _{x\in A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)\cup \bigcup _{x\in O\setminus A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)$$
9		iftrue	$$⊢x\in A\to if\left(x\in A,1,0\right)=1$$
10	9	sneqd	$$⊢x\in A\to \left\{if\left(x\in A,1,0\right)\right\}=\left\{1\right\}$$
11	10	xpeq2d	$$⊢x\in A\to \left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}=\left\{x\right\}\times \left\{1\right\}$$
12	11	iuneq2i	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)=\bigcup _{x\in A}\left(\left\{x\right\}\times \left\{1\right\}\right)$$
13		iunxpconst	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times \left\{1\right\}\right)=A\times \left\{1\right\}$$
14	12 13	eqtri	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)=A\times \left\{1\right\}$$
15		eldifn	$$⊢x\in \left(O\setminus A\right)\to \neg x\in A$$
16		iffalse	$$⊢\neg x\in A\to if\left(x\in A,1,0\right)=0$$
17	16	sneqd	$$⊢\neg x\in A\to \left\{if\left(x\in A,1,0\right)\right\}=\left\{0\right\}$$
18	15 17	syl	$$⊢x\in \left(O\setminus A\right)\to \left\{if\left(x\in A,1,0\right)\right\}=\left\{0\right\}$$
19	18	xpeq2d	$$⊢x\in \left(O\setminus A\right)\to \left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}=\left\{x\right\}\times \left\{0\right\}$$
20	19	iuneq2i	$$⊢\bigcup _{x\in O\setminus A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)=\bigcup _{x\in O\setminus A}\left(\left\{x\right\}\times \left\{0\right\}\right)$$
21		iunxpconst	$$⊢\bigcup _{x\in O\setminus A}\left(\left\{x\right\}\times \left\{0\right\}\right)=\left(O\setminus A\right)\times \left\{0\right\}$$
22	20 21	eqtri	$$⊢\bigcup _{x\in O\setminus A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)=\left(O\setminus A\right)\times \left\{0\right\}$$
23	14 22	uneq12i	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)\cup \bigcup _{x\in O\setminus A}\left(\left\{x\right\}\times \left\{if\left(x\in A,1,0\right)\right\}\right)=\left(A\times \left\{1\right\}\right)\cup \left(\left(O\setminus A\right)\times \left\{0\right\}\right)$$
24	8 23	eqtrdi	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)=\left(A\times \left\{1\right\}\right)\cup \left(\left(O\setminus A\right)\times \left\{0\right\}\right)$$