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 \mathrm{V}$$
	fvconst0ci.2	$$⊢Y=\left(A\times \left\{B\right\}\right)\left(X\right)$$
Assertion	fvconst0ci	$$⊢\left(Y=\varnothing \vee Y=B\right)$$

Proof

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