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 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 )