indconst1

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

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

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

Metamath Proof Explorer