This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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