Theorem fvconstdomi

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

	Ref	Expression
Hypothesis	fvconstdomi.1	$$⊢B\in \mathrm{V}$$
Assertion	fvconstdomi	$$⊢\left(A\times \left\{B\right\}\right)\left(X\right)\preccurlyeq B$$

Proof

Step	Hyp	Ref	Expression
1		fvconstdomi.1	$$⊢B\in \mathrm{V}$$
2		dmxpss	$$⊢\mathrm{dom}\left(A\times \left\{B\right\}\right)\subseteq A$$
3	2	sseli	$$⊢X\in \mathrm{dom}\left(A\times \left\{B\right\}\right)\to X\in A$$
4	1	fvconst2	$$⊢X\in A\to \left(A\times \left\{B\right\}\right)\left(X\right)=B$$
5	3 4	syl	$$⊢X\in \mathrm{dom}\left(A\times \left\{B\right\}\right)\to \left(A\times \left\{B\right\}\right)\left(X\right)=B$$
6		domrefg	$$⊢B\in \mathrm{V}\to B\preccurlyeq B$$
7	1 6	ax-mp	$$⊢B\preccurlyeq B$$
8	5 7	eqbrtrdi	$$⊢X\in \mathrm{dom}\left(A\times \left\{B\right\}\right)\to \left(A\times \left\{B\right\}\right)\left(X\right)\preccurlyeq B$$
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	1	0dom	$$⊢\varnothing \preccurlyeq B$$
11	9 10	eqbrtrdi	$$⊢\neg X\in \mathrm{dom}\left(A\times \left\{B\right\}\right)\to \left(A\times \left\{B\right\}\right)\left(X\right)\preccurlyeq B$$
12	8 11	pm2.61i	$$⊢\left(A\times \left\{B\right\}\right)\left(X\right)\preccurlyeq B$$