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 e. _V
	fvconst0ci.2	|- Y = ( ( A X. { B } ) ` X )
Assertion	fvconst0ci	|- ( Y = (/) \/ Y = B )

Proof

Step	Hyp	Ref	Expression
1		fvconst0ci.1	|- B e. _V
2		fvconst0ci.2	|- Y = ( ( A X. { B } ) ` X )
3		dmxpss	|- dom ( A X. { B } ) C_ A
4	3	sseli	|- ( X e. dom ( A X. { B } ) -> X e. A )
5	1	fvconst2	|- ( X e. A -> ( ( A X. { B } ) ` X ) = B )
6	4 5	syl	|- ( X e. dom ( A X. { B } ) -> ( ( A X. { B } ) ` X ) = B )
7	2 6	eqtrid	|- ( X e. dom ( A X. { B } ) -> Y = B )
8	7	olcd	|- ( X e. dom ( A X. { B } ) -> ( Y = (/) \/ Y = B ) )
9		ndmfv	|- ( -. X e. dom ( A X. { B } ) -> ( ( A X. { B } ) ` X ) = (/) )
10	2 9	eqtrid	|- ( -. X e. dom ( A X. { B } ) -> Y = (/) )
11	10	orcd	|- ( -. X e. dom ( A X. { B } ) -> ( Y = (/) \/ Y = B ) )
12	8 11	pm2.61i	|- ( Y = (/) \/ Y = B )