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	biimpi	$$⊢A\subseteq O\to A\cup \left(O\setminus A\right)=O$$
5	4	adantl	$$⊢\left(O\in V\wedge A\subseteq O\right)\to A\cup \left(O\setminus A\right)=O$$
6	5	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)$$
7	1 2 6	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)$$
8		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)$$
9	7 8	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)$$
10		iftrue	$$⊢x\in A\to if\left(x\in A,1,0\right)=1$$
11	10	sneqd	$$⊢x\in A\to \left\{if\left(x\in A,1,0\right)\right\}=\left\{1\right\}$$
12	11	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\}$$
13	12	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)$$
14		iunxpconst	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times \left\{1\right\}\right)=A\times \left\{1\right\}$$
15	13 14	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\}$$
16		eldifn	$$⊢x\in \left(O\setminus A\right)\to \neg x\in A$$
17		iffalse	$$⊢\neg x\in A\to if\left(x\in A,1,0\right)=0$$
18	17	sneqd	$$⊢\neg x\in A\to \left\{if\left(x\in A,1,0\right)\right\}=\left\{0\right\}$$
19	16 18	syl	$$⊢x\in \left(O\setminus A\right)\to \left\{if\left(x\in A,1,0\right)\right\}=\left\{0\right\}$$
20	19	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\}$$
21	20	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)$$
22		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\}$$
23	21 22	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\}$$
24	15 23	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)$$
25	9 24	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)$$