Metamath Proof Explorer


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 Could not format assertion : No typesetting found for |- ( X e. V -> ( F e. ( 0 -aryF X ) <-> E. x e. X F = { <. (/) , x >. } ) ) with typecode |-

Proof

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