Theorem indconst0

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

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

Proof

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