This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvconst0ci

Description: A constant function's value is either the constant or the empty set. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024)

		Ref	Expression
	Hypotheses	fvconst0ci.1	$⊢ B \in V$
		fvconst0ci.2	$⊢ Y = (A \times \{B\}) (X)$
	Assertion	fvconst0ci	$⊢ (Y = \emptyset \lor Y = B)$

Proof

Step	Hyp	Ref	Expression
1		fvconst0ci.1	$⊢ B \in V$
2		fvconst0ci.2	$⊢ Y = (A \times \{B\}) (X)$
3		dmxpss	$⊢ dom (A \times \{B\}) \subseteq A$
4	3	sseli	$⊢ X \in dom (A \times \{B\}) \to X \in A$
5	1	fvconst2	$⊢ X \in A \to (A \times \{B\}) (X) = B$
6	4 5	syl	$⊢ X \in dom (A \times \{B\}) \to (A \times \{B\}) (X) = B$
7	2 6	eqtrid	$⊢ X \in dom (A \times \{B\}) \to Y = B$
8	7	olcd	$⊢ X \in dom (A \times \{B\}) \to (Y = \emptyset \lor Y = B)$
9		ndmfv	$⊢ \neg X \in dom (A \times \{B\}) \to (A \times \{B\}) (X) = \emptyset$
10	2 9	eqtrid	$⊢ \neg X \in dom (A \times \{B\}) \to Y = \emptyset$
11	10	orcd	$⊢ \neg X \in dom (A \times \{B\}) \to (Y = \emptyset \lor Y = B)$
12	8 11	pm2.61i	$⊢ (Y = \emptyset \lor Y = B)$