Theorem indconst1

Description: Indicator of the whole set. (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Assertion	indconst1	$$⊢O\in V\to {𝟙}_O\left(O\right)=O\times \left\{1\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢O\subseteq O$$
2		indval2	$$⊢\left(O\in V\wedge O\subseteq O\right)\to {𝟙}_O\left(O\right)=\left(O\times \left\{1\right\}\right)\cup \left(\left(O\setminus O\right)\times \left\{0\right\}\right)$$
3	1 2	mpan2	$$⊢O\in V\to {𝟙}_O\left(O\right)=\left(O\times \left\{1\right\}\right)\cup \left(\left(O\setminus O\right)\times \left\{0\right\}\right)$$
4		difid	$$⊢O\setminus O=\varnothing$$
5	4	xpeq1i	$$⊢\left(O\setminus O\right)\times \left\{0\right\}=\varnothing \times \left\{0\right\}$$
6		0xp	$$⊢\varnothing \times \left\{0\right\}=\varnothing$$
7	5 6	eqtri	$$⊢\left(O\setminus O\right)\times \left\{0\right\}=\varnothing$$
8	7	a1i	$$⊢O\in V\to \left(O\setminus O\right)\times \left\{0\right\}=\varnothing$$
9	8	uneq2d	$$⊢O\in V\to \left(O\times \left\{1\right\}\right)\cup \left(\left(O\setminus O\right)\times \left\{0\right\}\right)=\left(O\times \left\{1\right\}\right)\cup \varnothing$$
10		un0	$$⊢\left(O\times \left\{1\right\}\right)\cup \varnothing =O\times \left\{1\right\}$$
11	10	a1i	$$⊢O\in V\to \left(O\times \left\{1\right\}\right)\cup \varnothing =O\times \left\{1\right\}$$
12	3 9 11	3eqtrd	$$⊢O\in V\to {𝟙}_O\left(O\right)=O\times \left\{1\right\}$$