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 e. _V
Assertion	fvconstdomi	|- ( ( A X. { B } ) ` X ) ~<_ B

Proof

Step	Hyp	Ref	Expression
1		fvconstdomi.1	|- B e. _V
2		dmxpss	|- dom ( A X. { B } ) C_ A
3	2	sseli	|- ( X e. dom ( A X. { B } ) -> X e. A )
4	1	fvconst2	|- ( X e. A -> ( ( A X. { B } ) ` X ) = B )
5	3 4	syl	|- ( X e. dom ( A X. { B } ) -> ( ( A X. { B } ) ` X ) = B )
6		domrefg	|- ( B e. _V -> B ~<_ B )
7	1 6	ax-mp	|- B ~<_ B
8	5 7	eqbrtrdi	|- ( X e. dom ( A X. { B } ) -> ( ( A X. { B } ) ` X ) ~<_ B )
9		ndmfv	|- ( -. X e. dom ( A X. { B } ) -> ( ( A X. { B } ) ` X ) = (/) )
10	1	0dom	|- (/) ~<_ B
11	9 10	eqbrtrdi	|- ( -. X e. dom ( A X. { B } ) -> ( ( A X. { B } ) ` X ) ~<_ B )
12	8 11	pm2.61i	|- ( ( A X. { B } ) ` X ) ~<_ B