Theorem 0aryfvalel

Description: A nullary (endo)function on a set X is a singleton of an ordered pair with the empty set as first component. A nullary function represents a constant: ( F(/) ) = C with C e. X , see also 0aryfvalelfv . Instead of ( F(/) ) , nullary functions are usually written as F ( ) in literature. (Contributed by AV, 15-May-2024)

	Ref	Expression
Assertion	0aryfvalel	|- ( X e. V -> ( F e. ( 0 -aryF X ) <-> E. x e. X F = { <. (/) , x >. } ) )

Proof

Step	Hyp	Ref	Expression
1		0nn0	|- 0 e. NN0
2		fzo0	|- ( 0 ..^ 0 ) = (/)
3	2	eqcomi	|- (/) = ( 0 ..^ 0 )
4	3	naryfvalel	|- ( ( 0 e. NN0 /\ X e. V ) -> ( F e. ( 0 -aryF X ) <-> F : ( X ^m (/) ) --> X ) )
5	1 4	mpan	|- ( X e. V -> ( F e. ( 0 -aryF X ) <-> F : ( X ^m (/) ) --> X ) )
6		mapdm0	|- ( X e. V -> ( X ^m (/) ) = { (/) } )
7	6	feq2d	|- ( X e. V -> ( F : ( X ^m (/) ) --> X <-> F : { (/) } --> X ) )
8		0ex	|- (/) e. _V
9	8	fsn2	|- ( F : { (/) } --> X <-> ( ( F ` (/) ) e. X /\ F = { <. (/) , ( F ` (/) ) >. } ) )
10		opeq2	|- ( x = ( F ` (/) ) -> <. (/) , x >. = <. (/) , ( F ` (/) ) >. )
11	10	sneqd	|- ( x = ( F ` (/) ) -> { <. (/) , x >. } = { <. (/) , ( F ` (/) ) >. } )
12	11	rspceeqv	|- ( ( ( F ` (/) ) e. X /\ F = { <. (/) , ( F ` (/) ) >. } ) -> E. x e. X F = { <. (/) , x >. } )
13	9 12	sylbi	|- ( F : { (/) } --> X -> E. x e. X F = { <. (/) , x >. } )
14	8	a1i	|- ( x e. X -> (/) e. _V )
15		id	|- ( x e. X -> x e. X )
16	14 15	fsnd	|- ( x e. X -> { <. (/) , x >. } : { (/) } --> X )
17		feq1	|- ( F = { <. (/) , x >. } -> ( F : { (/) } --> X <-> { <. (/) , x >. } : { (/) } --> X ) )
18	16 17	syl5ibrcom	|- ( x e. X -> ( F = { <. (/) , x >. } -> F : { (/) } --> X ) )
19	18	rexlimiv	|- ( E. x e. X F = { <. (/) , x >. } -> F : { (/) } --> X )
20	13 19	impbii	|- ( F : { (/) } --> X <-> E. x e. X F = { <. (/) , x >. } )
21	20	a1i	|- ( X e. V -> ( F : { (/) } --> X <-> E. x e. X F = { <. (/) , x >. } ) )
22	5 7 21	3bitrd	|- ( X e. V -> ( F e. ( 0 -aryF X ) <-> E. x e. X F = { <. (/) , x >. } ) )