indconst0

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

		Ref	Expression
	Assertion	indconst0	$⊢ O \in V \to 𝟙_{O} (\emptyset) = O \times \{0\}$

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

Metamath Proof Explorer