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