Metamath Proof Explorer

Theorem 0aryfvalelfv

Description: The value of a nullary (endo)function on a set X . (Contributed by AV, 19-May-2024)

Ref Expression
Assertion 0aryfvalelfv 
|- ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 0 ..^ 0 ) = ( 0 ..^ 0 )
2 1 naryrcl 
 |-  ( F e. ( 0 -aryF X ) -> ( 0 e. NN0 /\ X e. _V ) )
3 0aryfvalel 
 |-  ( X e. _V -> ( F e. ( 0 -aryF X ) <-> E. x e. X F = { <. (/) , x >. } ) )
4 0ex 
 |-  (/) e. _V
5 fvsng 
 |-  ( ( (/) e. _V /\ x e. X ) -> ( { <. (/) , x >. } ` (/) ) = x )
6 4 5 mpan 
 |-  ( x e. X -> ( { <. (/) , x >. } ` (/) ) = x )
7 fveq1 
 |-  ( F = { <. (/) , x >. } -> ( F ` (/) ) = ( { <. (/) , x >. } ` (/) ) )
8 7 eqeq1d 
 |-  ( F = { <. (/) , x >. } -> ( ( F ` (/) ) = x <-> ( { <. (/) , x >. } ` (/) ) = x ) )
9 6 8 syl5ibrcom 
 |-  ( x e. X -> ( F = { <. (/) , x >. } -> ( F ` (/) ) = x ) )
10 9 reximia 
 |-  ( E. x e. X F = { <. (/) , x >. } -> E. x e. X ( F ` (/) ) = x )
11 3 10 biimtrdi 
 |-  ( X e. _V -> ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x ) )
12 11 adantl 
 |-  ( ( 0 e. NN0 /\ X e. _V ) -> ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x ) )
13 2 12 mpcom 
 |-  ( F e. ( 0 -aryF X ) -> E. x e. X ( F ` (/) ) = x )